set a9 = the Element of C1;
set b9 = the Element of C2;
the Element of C1 U+ the Element of C2 in C1 "/\" C2 ;
hence not C1 "/\" C2 is empty ; :: thesis: ( C1 "/\" C2 is subset-closed & C1 "/\" C2 is binary_complete )
hereby :: according to CLASSES1:def 1 :: thesis: C1 "/\" C2 is binary_complete
let a, b be set ; :: thesis: ( a in C1 "/\" C2 & b c= a implies b in C1 "/\" C2 )
assume a in C1 "/\" C2 ; :: thesis: ( b c= a implies b in C1 "/\" C2 )
then consider aa being Element of C1, bb being Element of C2 such that
A1: a = aa U+ bb ;
assume b c= a ; :: thesis: b in C1 "/\" C2
then consider x1, y1 being set such that
A2: b = x1 U+ y1 and
A3: ( x1 c= aa & y1 c= bb ) by A1, Th79;
( x1 in C1 & y1 in C2 ) by A3, CLASSES1:def 1;
hence b in C1 "/\" C2 by A2; :: 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 )
assume A4: for a, b being set st a in A & b in A holds
a \/ b in C1 "/\" C2 ; :: thesis: union A in C1 "/\" C2
set A2 = { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ;
now :: thesis: for x, y being set st x in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } & y in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } holds
x \/ y in C2
let x, y be set ; :: thesis: ( x in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } & y in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } implies x \/ y in C2 )
assume x in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ; :: thesis: ( y in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } implies x \/ y in C2 )
then consider ax being Element of C2 such that
A5: x = ax and
A6: ex b being Element of C1 st b U+ ax in A ;
consider bx being Element of C1 such that
A7: bx U+ ax in A by A6;
assume y in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ; :: thesis: x \/ y in C2
then consider ay being Element of C2 such that
A8: y = ay and
A9: ex b being Element of C1 st b U+ ay in A ;
consider by1 being Element of C1 such that
A10: by1 U+ ay in A by A9;
(bx U+ ax) \/ (by1 U+ ay) in C1 "/\" C2 by A4, A7, A10;
then (bx \/ by1) U+ (ax \/ ay) in C1 "/\" C2 by Th81;
hence x \/ y in C2 by A5, A8, Th84; :: thesis: verum
end;
then A11: union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } in C2 by Def1;
set A1 = { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ;
A12: (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) = union A
proof
hereby :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: union A c= (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } )
let x be object ; :: thesis: ( x in (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) implies b1 in union A )
assume A13: x in (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) ; :: thesis: b1 in union A
then A14: x = [(x `1),(x `2)] by Th75;
per cases ( ( x `2 = 1 & x `1 in union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) or ( x `2 = 2 & x `1 in union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) ) by A13, Th75;
suppose A15: ( x `2 = 1 & x `1 in union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) ; :: thesis: b1 in union A
then consider a being set such that
A16: x `1 in a and
A17: a in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } by TARSKI:def 4;
consider ax being Element of C1 such that
A18: a = ax and
A19: ex b being Element of C2 st ax U+ b in A by A17;
consider bx being Element of C2 such that
A20: ax U+ bx in A by A19;
x in ax U+ bx by A14, A15, A16, A18, Th76;
hence x in union A by A20, TARSKI:def 4; :: thesis: verum
end;
suppose A21: ( x `2 = 2 & x `1 in union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) ; :: thesis: b1 in union A
then consider a being set such that
A22: x `1 in a and
A23: a in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } by TARSKI:def 4;
consider bx being Element of C2 such that
A24: a = bx and
A25: ex a being Element of C1 st a U+ bx in A by A23;
consider ax being Element of C1 such that
A26: ax U+ bx in A by A25;
x in ax U+ bx by A14, A21, A22, A24, Th77;
hence x in union A by A26, TARSKI:def 4; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union A or x in (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) )
assume x in union A ; :: thesis: x in (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } )
then consider a being set such that
A27: x in a and
A28: a in A by TARSKI:def 4;
a \/ a in C1 "/\" C2 by A4, A28;
then consider aa being Element of C1, bb being Element of C2 such that
A29: a = aa U+ bb ;
bb in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } by A28, A29;
then A30: bb c= union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } by ZFMISC_1:74;
aa in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } by A28, A29;
then aa c= union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } by ZFMISC_1:74;
then aa U+ bb c= (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) by A30, Th78;
hence x in (union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ) U+ (union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ) by A27, A29; :: thesis: verum
end;
now :: thesis: for x, y being set st x in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } & y in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } holds
x \/ y in C1
let x, y be set ; :: thesis: ( x in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } & y in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } implies x \/ y in C1 )
assume x in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ; :: thesis: ( y in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } implies x \/ y in C1 )
then consider ax being Element of C1 such that
A31: x = ax and
A32: ex b being Element of C2 st ax U+ b in A ;
consider bx being Element of C2 such that
A33: ax U+ bx in A by A32;
assume y in { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ; :: thesis: x \/ y in C1
then consider ay being Element of C1 such that
A34: y = ay and
A35: ex b being Element of C2 st ay U+ b in A ;
consider by1 being Element of C2 such that
A36: ay U+ by1 in A by A35;
(ax U+ bx) \/ (ay U+ by1) in C1 "/\" C2 by A4, A33, A36;
then (ax \/ ay) U+ (bx \/ by1) in C1 "/\" C2 by Th81;
hence x \/ y in C1 by A31, A34, Th84; :: thesis: verum
end;
then union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } in C1 by Def1;
hence union A in C1 "/\" C2 by A11, A12; :: thesis: verum