let A, B be Category; IdCat [:A,B:] = [:(IdCat A),(IdCat B):]
now ( [: the carrier of (IdCat A), the carrier of (IdCat B):] = the carrier of (IdCat [:A,B:]) & the carrier' of (IdCat [:A,B:]) = [: the carrier' of (IdCat A), the carrier' of (IdCat B):] & [: the Source of (IdCat A), the Source of (IdCat B):] = the Source of (IdCat [:A,B:]) & [: the Target of (IdCat A), the Target of (IdCat B):] = the Target of (IdCat [:A,B:]) & |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) )reconsider OA = the
carrier of
(IdCat A) as non
empty Subset of the
carrier of
A by CAT_2:def 4;
set AB =
{ (id c) where c is Object of [:A,B:] : verum } ;
set MA =
{ (id a) where a is Object of A : verum } ;
set MB =
{ (id b) where b is Object of B : verum } ;
A1:
{ (id c) where c is Object of [:A,B:] : verum } = [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :]
proof
thus
{ (id c) where c is Object of [:A,B:] : verum } c= [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :]
XBOOLE_0:def 10 [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] c= { (id c) where c is Object of [:A,B:] : verum } proof
let x be
object ;
TARSKI:def 3 ( not x in { (id c) where c is Object of [:A,B:] : verum } or x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] )
assume
x in { (id c) where c is Object of [:A,B:] : verum }
;
x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :]
then consider c being
Object of
[:A,B:] such that A2:
x = id c
;
consider c1 being
Object of
A,
c2 being
Object of
B such that A3:
c = [c1,c2]
by DOMAIN_1:1;
A4:
id c2 in { (id b) where b is Object of B : verum }
;
A5:
id c1 in { (id a) where a is Object of A : verum }
;
id c = [(id c1),(id c2)]
by A3, CAT_2:31;
hence
x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :]
by A2, A5, A4, ZFMISC_1:87;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :] or x in { (id c) where c is Object of [:A,B:] : verum } )
assume
x in [: { (id a) where a is Object of A : verum } , { (id b) where b is Object of B : verum } :]
;
x in { (id c) where c is Object of [:A,B:] : verum }
then consider x1,
x2 being
object such that A6:
x1 in { (id a) where a is Object of A : verum }
and A7:
x2 in { (id b) where b is Object of B : verum }
and A8:
x = [x1,x2]
by ZFMISC_1:84;
consider a being
Object of
A such that A9:
x1 = id a
by A6;
consider b being
Object of
B such that A10:
x2 = id b
by A7;
id [a,b] = [(id a),(id b)]
by CAT_2:31;
hence
x in { (id c) where c is Object of [:A,B:] : verum }
by A8, A9, A10;
verum
end; reconsider OB = the
carrier of
(IdCat B) as non
empty Subset of the
carrier of
B by CAT_2:def 4;
reconsider MB = the
carrier' of
(IdCat B) as non
empty Subset of the
carrier' of
B by CAT_2:7;
reconsider MA = the
carrier' of
(IdCat A) as non
empty Subset of the
carrier' of
A by CAT_2:7;
A11:
the
carrier of
(IdCat B) = the
carrier of
B
by Def20;
the
carrier of
(IdCat A) = the
carrier of
A
by Def20;
hence
[: the carrier of (IdCat A), the carrier of (IdCat B):] = the
carrier of
(IdCat [:A,B:])
by A11, Def20;
( the carrier' of (IdCat [:A,B:]) = [: the carrier' of (IdCat A), the carrier' of (IdCat B):] & [: the Source of (IdCat A), the Source of (IdCat B):] = the Source of (IdCat [:A,B:]) & [: the Target of (IdCat A), the Target of (IdCat B):] = the Target of (IdCat [:A,B:]) & |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) )A12:
the
Target of
(IdCat B) = the
Target of
B | the
carrier' of
(IdCat B)
by Th4;
A13:
the
Source of
(IdCat B) = the
Source of
B | the
carrier' of
(IdCat B)
by Th4;
A14:
the
carrier' of
(IdCat B) = { (id b) where b is Object of B : verum }
by Def20;
the
carrier' of
(IdCat A) = { (id a) where a is Object of A : verum }
by Def20;
hence A15:
the
carrier' of
(IdCat [:A,B:]) = [: the carrier' of (IdCat A), the carrier' of (IdCat B):]
by A1, A14, Def20;
( [: the Source of (IdCat A), the Source of (IdCat B):] = the Source of (IdCat [:A,B:]) & [: the Target of (IdCat A), the Target of (IdCat B):] = the Target of (IdCat [:A,B:]) & |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) )
the
Source of
(IdCat A) = the
Source of
A | the
carrier' of
(IdCat A)
by Th4;
hence [: the Source of (IdCat A), the Source of (IdCat B):] =
[: the Source of A, the Source of B:] | [:MA,MB:]
by A13, FUNCT_3:81
.=
the
Source of
(IdCat [:A,B:])
by A15, Th4
;
( [: the Target of (IdCat A), the Target of (IdCat B):] = the Target of (IdCat [:A,B:]) & |: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) )
the
Target of
(IdCat A) = the
Target of
A | the
carrier' of
(IdCat A)
by Th4;
hence [: the Target of (IdCat A), the Target of (IdCat B):] =
[: the Target of A, the Target of B:] | [:MA,MB:]
by A12, FUNCT_3:81
.=
the
Target of
(IdCat [:A,B:])
by A15, Th4
;
|: the Comp of (IdCat A), the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:])A16:
the
Comp of
(IdCat A) = the
Comp of
A || MA
by Th4;
the
Comp of
(IdCat B) = the
Comp of
B || MB
by Th4;
hence |: the Comp of (IdCat A), the Comp of (IdCat B):| =
|: the Comp of A, the Comp of B:| || [:MA,MB:]
by A16, FUNCT_4:126
.=
the
Comp of
(IdCat [:A,B:])
by A15, Th4
;
verum end;
hence
IdCat [:A,B:] = [:(IdCat A),(IdCat B):]
; verum