let A, B be Category; :: thesis: IdCat [:A,B:] = [:(IdCat A),(IdCat B):]
now
( the
carrier of
(IdCat A) = the
carrier of
A & the
carrier of
(IdCat B) = the
carrier of
B )
by Def20;
hence A1:
[:the carrier of (IdCat A),the carrier of (IdCat B):] = the
carrier of
(IdCat [:A,B:])
by Def20;
:: thesis: ( 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:]) )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 } ;
A2:
{ (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 } :]
:: according to XBOOLE_0:def 10 :: thesis: [:{ (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 ;
:: according to TARSKI:def 3 :: thesis: ( 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 }
;
:: thesis: 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 A3:
x = id c
;
consider c1 being
Object of
A,
c2 being
Object of
B such that A4:
c = [c1,c2]
by DOMAIN_1:9;
A5:
id c = [(id c1),(id c2)]
by A4, CAT_2:41;
(
id c1 in { (id a) where a is Object of A : verum } &
id c2 in { (id b) where b is Object of B : verum } )
;
hence
x in [:{ (id a) where a is Object of A : verum } ,{ (id b) where b is Object of B : verum } :]
by A3, A5, ZFMISC_1:106;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 } :]
;
:: thesis: 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 } &
x2 in { (id b) where b is Object of B : verum } )
and A7:
x = [x1,x2]
by ZFMISC_1:103;
consider a being
Object of
A such that A8:
x1 = id a
by A6;
consider b being
Object of
B such that A9:
x2 = id b
by A6;
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 A7, A8, A9;
:: thesis: verum
end;
( the
carrier' of
(IdCat A) = { (id a) where a is Object of A : verum } & the
carrier' of
(IdCat B) = { (id b) where b is Object of B : verum } )
by Def20;
hence A10:
the
carrier' of
(IdCat [:A,B:]) = [:the carrier' of (IdCat A),the carrier' of (IdCat B):]
by A2, Def20;
:: thesis: ( [: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:]) )reconsider MA = the
carrier' of
(IdCat A) as non
empty Subset of the
carrier' of
A by CAT_2:13;
reconsider MB = the
carrier' of
(IdCat B) as non
empty Subset of the
carrier' of
B by CAT_2:13;
( the
Source of
(IdCat A) = the
Source of
A | the
carrier' of
(IdCat A) & the
Source of
(IdCat B) = the
Source of
B | the
carrier' of
(IdCat B) )
by Th8;
hence [:the Source of (IdCat A),the Source of (IdCat B):] =
[:the Source of A,the Source of B:] | [:MA,MB:]
by Th1
.=
the
Source of
(IdCat [:A,B:])
by A10, Th8
;
:: thesis: ( [: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) & the
Target of
(IdCat B) = the
Target of
B | the
carrier' of
(IdCat B) )
by Th8;
hence [:the Target of (IdCat A),the Target of (IdCat B):] =
[:the Target of A,the Target of B:] | [:MA,MB:]
by Th1
.=
the
Target of
(IdCat [:A,B:])
by A10, Th8
;
:: thesis: ( |: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:]) )A11:
|:the Comp of A,the Comp of B:| || [:MA,MB:] = the
Comp of
(IdCat [:A,B:])
by A10, Th8;
( the
Comp of
(IdCat A) = the
Comp of
A || MA & the
Comp of
(IdCat B) = the
Comp of
B || MB )
by Th8;
hence
|:the Comp of (IdCat A),the Comp of (IdCat B):| = the
Comp of
(IdCat [:A,B:])
by A11, Th2;
:: thesis: [:the Id of (IdCat A),the Id of (IdCat B):] = the Id 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;
reconsider OB = the
carrier of
(IdCat B) as non
empty Subset of the
carrier of
B by CAT_2:def 4;
( the
Id of
(IdCat A) = the
Id of
A | the
carrier of
(IdCat A) & the
Id of
(IdCat B) = the
Id of
B | the
carrier of
(IdCat B) )
by Th8;
hence [:the Id of (IdCat A),the Id of (IdCat B):] =
[:the Id of A,the Id of B:] | [:OA,OB:]
by Th1
.=
the
Id of
(IdCat [:A,B:])
by A1, Th8
;
:: thesis: verum
hence
IdCat [:A,B:] = [:(IdCat A),(IdCat B):]
; :: thesis: verum