let A, B be Category; IdCat [:A,B:] = [:(IdCat A),(IdCat B):]
now 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
set ;
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:9;
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:41;
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:106;
verum
end;
let x be
set ;
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
set 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:103;
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:41;
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:13;
reconsider MA = the
carrier' of
(IdCat A) as non
empty Subset of the
carrier' of
A by CAT_2:13;
A11:
the
carrier of
(IdCat B) = the
carrier of
B
by Def20;
the
carrier of
(IdCat A) = the
carrier of
A
by Def20;
hence A12:
[: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:]) & [:the Id of (IdCat A),the Id of (IdCat B):] = the Id of (IdCat [:A,B:]) )A13:
the
Target of
(IdCat B) = the
Target of
B | the
carrier' of
(IdCat B)
by Th8;
A14:
the
Source of
(IdCat B) = the
Source of
B | the
carrier' of
(IdCat B)
by Th8;
A15:
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 A16:
the
carrier' of
(IdCat [:A,B:]) = [:the carrier' of (IdCat A),the carrier' of (IdCat B):]
by A1, A15, 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 Id of (IdCat A),the Id of (IdCat B):] = the Id of (IdCat [:A,B:]) )
the
Source of
(IdCat A) = the
Source of
A | the
carrier' of
(IdCat A)
by Th8;
hence [:the Source of (IdCat A),the Source of (IdCat B):] =
[:the Source of A,the Source of B:] | [:MA,MB:]
by A14, Th1
.=
the
Source of
(IdCat [:A,B:])
by A16, Th8
;
( [: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 Id of (IdCat A),the Id of (IdCat B):] = the Id of (IdCat [:A,B:]) )
the
Target of
(IdCat A) = the
Target of
A | the
carrier' of
(IdCat A)
by Th8;
hence [:the Target of (IdCat A),the Target of (IdCat B):] =
[:the Target of A,the Target of B:] | [:MA,MB:]
by A13, Th1
.=
the
Target of
(IdCat [:A,B:])
by A16, Th8
;
( |:the Comp of (IdCat A),the Comp of (IdCat B):| = the Comp of (IdCat [:A,B:]) & [:the Id of (IdCat A),the Id of (IdCat B):] = the Id of (IdCat [:A,B:]) )A17:
the
Comp of
(IdCat A) = the
Comp of
A || MA
by Th8;
A18:
the
Comp of
(IdCat B) = the
Comp of
B || MB
by Th8;
|:the Comp of A,the Comp of B:| || [:MA,MB:] = the
Comp of
(IdCat [:A,B:])
by A16, Th8;
hence
|:the Comp of (IdCat A),the Comp of (IdCat B):| = the
Comp of
(IdCat [:A,B:])
by A17, A18, Th2;
[:the Id of (IdCat A),the Id of (IdCat B):] = the Id of (IdCat [:A,B:])A19:
the
Id of
(IdCat B) = the
Id of
B | the
carrier of
(IdCat B)
by Th8;
the
Id of
(IdCat A) = the
Id of
A | the
carrier of
(IdCat A)
by Th8;
hence [:the Id of (IdCat A),the Id of (IdCat B):] =
[:the Id of A,the Id of B:] | [:OA,OB:]
by A19, Th1
.=
the
Id of
(IdCat [:A,B:])
by A12, Th8
;
verum end;
hence
IdCat [:A,B:] = [:(IdCat A),(IdCat B):]
; verum