set a9 = the Element of C1;
the Element of C1 U+ {} in C1 "\/" C2 by Th86;
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
A37: a = aa U+ bb and
A38: ( aa = {} or bb = {} ) by Th87;
assume b c= a ; :: thesis: b in C1 "\/" C2
then consider x1, y1 being set such that
A39: b = x1 U+ y1 and
A40: ( x1 c= aa & y1 c= bb ) by A37, Th79;
A41: ( x1 in C1 & y1 in C2 ) by A40, CLASSES1:def 1;
( x1 = {} or y1 = {} ) by A38, A40;
hence b in C1 "\/" C2 by A39, A41, Th86; :: 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 = { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } ;
set A2 = { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } ;
assume A42: 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 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
A43: x = ax and
A44: ex b being Element of C1 st b U+ ax in A ;
consider bx being Element of C1 such that
A45: bx U+ ax in A by A44;
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
A46: y = ay and
A47: ex b being Element of C1 st b U+ ay in A ;
consider by1 being Element of C1 such that
A48: by1 U+ ay in A by A47;
(bx U+ ax) \/ (by1 U+ ay) in C1 "\/" C2 by A42, A45, A48;
then (bx \/ by1) U+ (ax \/ ay) in C1 "\/" C2 by Th81;
then ( x \/ y in C2 or x \/ y = {} ) by A43, A46, Th86;
hence x \/ y in C2 by COH_SP:1; :: thesis: verum
end;
then A49: union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } in C2 by Def1;
A50: (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 A51: 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 A52: 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 A51, Th75;
suppose A53: ( 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
A54: x `1 in a and
A55: 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
A56: a = ax and
A57: ex b being Element of C2 st ax U+ b in A by A55;
consider bx being Element of C2 such that
A58: ax U+ bx in A by A57;
x in ax U+ bx by A52, A53, A54, A56, Th76;
hence x in union A by A58, TARSKI:def 4; :: thesis: verum
end;
suppose A59: ( 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
A60: x `1 in a and
A61: 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
A62: a = bx and
A63: ex a being Element of C1 st a U+ bx in A by A61;
consider ax being Element of C1 such that
A64: ax U+ bx in A by A63;
x in ax U+ bx by A52, A59, A60, A62, Th77;
hence x in union A by A64, 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
A65: x in a and
A66: a in A by TARSKI:def 4;
a \/ a in C1 "\/" C2 by A42, A66;
then consider aa being Element of C1, bb being Element of C2 such that
A67: a = aa U+ bb and
( aa = {} or bb = {} ) by Th87;
bb in { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } by A66, A67;
then A68: 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 A66, A67;
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 A68, 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 A65, A67; :: thesis: verum
end;
A69: now :: thesis: ( union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } <> {} implies not union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } <> {} )
assume union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } <> {} ; :: thesis: not union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } <> {}
then reconsider AA = union { a where a is Element of C1 : ex b being Element of C2 st a U+ b in A } as non empty set ;
set aa = the Element of AA;
consider x being set such that
A70: the Element of AA in x and
A71: x 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
A72: x = ax and
A73: ex b being Element of C2 st ax U+ b in A by A71;
consider bx being Element of C2 such that
A74: ax U+ bx in A by A73;
assume union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } <> {} ; :: thesis: contradiction
then reconsider AA = union { b where b is Element of C2 : ex a being Element of C1 st a U+ b in A } as non empty set ;
set bb = the Element of AA;
consider y being set such that
A75: the Element of AA in y and
A76: y 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 by1 being Element of C2 such that
A77: y = by1 and
A78: ex a being Element of C1 st a U+ by1 in A by A76;
consider ay being Element of C1 such that
A79: ay U+ by1 in A by A78;
(ax U+ bx) \/ (ay U+ by1) in C1 "\/" C2 by A42, A74, A79;
then (ax \/ ay) U+ (bx \/ by1) in C1 "\/" C2 by Th81;
hence contradiction by A70, A72, A75, A77, Th86; :: 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
A80: x = ax and
A81: ex b being Element of C2 st ax U+ b in A ;
consider bx being Element of C2 such that
A82: ax U+ bx in A by A81;
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
A83: y = ay and
A84: ex b being Element of C2 st ay U+ b in A ;
consider by1 being Element of C2 such that
A85: ay U+ by1 in A by A84;
(ax U+ bx) \/ (ay U+ by1) in C1 "\/" C2 by A42, A82, A85;
then (ax \/ ay) U+ (bx \/ by1) in C1 "\/" C2 by Th81;
then ( x \/ y in C1 or x \/ y = {} ) by A80, A83, Th86;
hence x \/ y in C1 by COH_SP:1; :: 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 A49, A69, A50, Th86; :: thesis: verum