thus C1 [*] C2 is subset-closed :: thesis: C1 [*] C2 is binary_complete
proof
let a, b be set ; :: according to CLASSES1:def 1 :: thesis: ( not a in C1 [*] C2 or not b c= a or b in C1 [*] C2 )
assume a in C1 [*] C2 ; :: thesis: ( not b c= a or b in C1 [*] C2 )
then consider a1 being Element of C1, a2 being Element of C2 such that
A1: a c= [:a1,a2:] by Th96;
assume b c= a ; :: thesis: b in C1 [*] C2
then b c= [:a1,a2:] by A1;
hence b in C1 [*] C2 by Th96; :: thesis: verum
end;
let A be set ; :: according to COHSP_1:def 1 :: thesis: ( ( for a, b being set st a in A & b in A holds
a \/ b in C1 [*] C2 ) implies union A in C1 [*] C2 )
set A1 = { (proj1 a) where a is Element of C1 [*] C2 : a in A } ;
set A2 = { (proj2 a) where a is Element of C1 [*] C2 : a in A } ;
assume A2: for a, b being set st a in A & b in A holds
a \/ b in C1 [*] C2 ; :: thesis: union A in C1 [*] C2
now :: thesis: for a1, b1 being set st a1 in { (proj2 a) where a is Element of C1 [*] C2 : a in A } & b1 in { (proj2 a) where a is Element of C1 [*] C2 : a in A } holds
a1 \/ b1 in C2
let a1, b1 be set ; :: thesis: ( a1 in { (proj2 a) where a is Element of C1 [*] C2 : a in A } & b1 in { (proj2 a) where a is Element of C1 [*] C2 : a in A } implies a1 \/ b1 in C2 )
assume a1 in { (proj2 a) where a is Element of C1 [*] C2 : a in A } ; :: thesis: ( b1 in { (proj2 a) where a is Element of C1 [*] C2 : a in A } implies a1 \/ b1 in C2 )
then consider a being Element of C1 [*] C2 such that
A3: a1 = proj2 a and
A4: a in A ;
assume b1 in { (proj2 a) where a is Element of C1 [*] C2 : a in A } ; :: thesis: a1 \/ b1 in C2
then consider b being Element of C1 [*] C2 such that
A5: b1 = proj2 b and
A6: b in A ;
a \/ b in C1 [*] C2 by A2, A4, A6;
then proj2 (a \/ b) in C2 by Th97;
hence a1 \/ b1 in C2 by A3, A5, XTUPLE_0:27; :: thesis: verum
end;
then A7: union { (proj2 a) where a is Element of C1 [*] C2 : a in A } in C2 by Def1;
A8: union A c= [:(union { (proj1 a) where a is Element of C1 [*] C2 : a in A } ),(union { (proj2 a) where a is Element of C1 [*] C2 : a in A } ):]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union A or x in [:(union { (proj1 a) where a is Element of C1 [*] C2 : a in A } ),(union { (proj2 a) where a is Element of C1 [*] C2 : a in A } ):] )
assume x in union A ; :: thesis: x in [:(union { (proj1 a) where a is Element of C1 [*] C2 : a in A } ),(union { (proj2 a) where a is Element of C1 [*] C2 : a in A } ):]
then consider a being set such that
A9: x in a and
A10: a in A by TARSKI:def 4;
A11: a \/ a in C1 [*] C2 by A2, A10;
then proj2 a in { (proj2 a) where a is Element of C1 [*] C2 : a in A } by A10;
then A12: proj2 a c= union { (proj2 a) where a is Element of C1 [*] C2 : a in A } by ZFMISC_1:74;
a c= [:(proj1 a),(proj2 a):] by A11, Th97;
then A13: x in [:(proj1 a),(proj2 a):] by A9;
proj1 a in { (proj1 a) where a is Element of C1 [*] C2 : a in A } by A10, A11;
then proj1 a c= union { (proj1 a) where a is Element of C1 [*] C2 : a in A } by ZFMISC_1:74;
then [:(proj1 a),(proj2 a):] c= [:(union { (proj1 a) where a is Element of C1 [*] C2 : a in A } ),(union { (proj2 a) where a is Element of C1 [*] C2 : a in A } ):] by A12, ZFMISC_1:96;
hence x in [:(union { (proj1 a) where a is Element of C1 [*] C2 : a in A } ),(union { (proj2 a) where a is Element of C1 [*] C2 : a in A } ):] by A13; :: thesis: verum
end;
now :: thesis: for a1, b1 being set st a1 in { (proj1 a) where a is Element of C1 [*] C2 : a in A } & b1 in { (proj1 a) where a is Element of C1 [*] C2 : a in A } holds
a1 \/ b1 in C1
let a1, b1 be set ; :: thesis: ( a1 in { (proj1 a) where a is Element of C1 [*] C2 : a in A } & b1 in { (proj1 a) where a is Element of C1 [*] C2 : a in A } implies a1 \/ b1 in C1 )
assume a1 in { (proj1 a) where a is Element of C1 [*] C2 : a in A } ; :: thesis: ( b1 in { (proj1 a) where a is Element of C1 [*] C2 : a in A } implies a1 \/ b1 in C1 )
then consider a being Element of C1 [*] C2 such that
A14: a1 = proj1 a and
A15: a in A ;
assume b1 in { (proj1 a) where a is Element of C1 [*] C2 : a in A } ; :: thesis: a1 \/ b1 in C1
then consider b being Element of C1 [*] C2 such that
A16: b1 = proj1 b and
A17: b in A ;
a \/ b in C1 [*] C2 by A2, A15, A17;
then proj1 (a \/ b) in C1 by Th97;
hence a1 \/ b1 in C1 by A14, A16, XTUPLE_0:23; :: thesis: verum
end;
then union { (proj1 a) where a is Element of C1 [*] C2 : a in A } in C1 by Def1;
hence union A in C1 [*] C2 by A7, A8, Th96; :: thesis: verum