let X be set ; :: thesis: for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for A, B, P being set st P = DisUnion S & A in P & B in P & A misses B holds
A \/ B in P
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X; :: thesis: for A, B, P being set st P = DisUnion S & A in P & B in P & A misses B holds
A \/ B in P
let A, B, P be set ; :: thesis: ( P = DisUnion S & A in P & B in P & A misses B implies A \/ B in P )
assume that
A1: P = DisUnion S and
A2: ( A in P & B in P & A misses B ) ; :: thesis: A \/ B in P
consider A1 being Subset of X such that
A3: ( A = A1 & ex g being disjoint_valued FinSequence of S st A1 = Union g ) by A1, A2;
consider g1 being disjoint_valued FinSequence of S such that
A4: A1 = Union g1 by A3;
consider B1 being Subset of X such that
A5: ( B = B1 & ex g being disjoint_valued FinSequence of S st B1 = Union g ) by A1, A2;
consider g2 being disjoint_valued FinSequence of S such that
A6: B1 = Union g2 by A5;
set F = g1 ^ g2;
now :: thesis: for n, m being object st n <> m holds
(g1 ^ g2) . n misses (g1 ^ g2) . m
let n, m be object ; :: thesis: ( n <> m implies (g1 ^ g2) . b1 misses (g1 ^ g2) . b2 )
assume A7: n <> m ; :: thesis: (g1 ^ g2) . b1 misses (g1 ^ g2) . b2
per cases ( ( n in dom (g1 ^ g2) & m in dom (g1 ^ g2) ) or not n in dom (g1 ^ g2) or not m in dom (g1 ^ g2) ) ;
suppose A8: ( n in dom (g1 ^ g2) & m in dom (g1 ^ g2) ) ; :: thesis: (g1 ^ g2) . b1 misses (g1 ^ g2) . b2
then reconsider n1 = n, m1 = m as Nat ;
A9: ( n1 in dom g1 or ex k being Nat st
( k in dom g2 & n1 = (len g1) + k ) ) by A8, FINSEQ_1:25;
A10: ( m1 in dom g1 or ex k being Nat st
( k in dom g2 & m1 = (len g1) + k ) ) by A8, FINSEQ_1:25;
per cases ( ( n1 in dom g1 & m1 in dom g1 ) or ( n1 in dom g1 & ex k being Nat st
( k in dom g2 & m1 = (len g1) + k ) ) or ( m1 in dom g1 & ex k being Nat st
( k in dom g2 & n1 = (len g1) + k ) ) or ex k being Nat st
( k in dom g2 & n1 = (len g1) + k & ex k being Nat st
( k in dom g2 & m1 = (len g1) + k ) ) ) by A9, A10;
suppose ( n1 in dom g1 & m1 in dom g1 ) ; :: thesis: (g1 ^ g2) . b1 misses (g1 ^ g2) . b2
then ( (g1 ^ g2) . n = g1 . n1 & (g1 ^ g2) . m = g1 . m1 ) by FINSEQ_1:def 7;
hence (g1 ^ g2) . n misses (g1 ^ g2) . m by A7, PROB_2:def 2; :: thesis: verum
end;
suppose A11: ( n1 in dom g1 & ex k being Nat st
( k in dom g2 & m1 = (len g1) + k ) ) ; :: thesis: (g1 ^ g2) . b1 misses (g1 ^ g2) . b2
then consider k being Nat such that
A12: ( k in dom g2 & m1 = (len g1) + k ) ;
( (g1 ^ g2) . n = g1 . n1 & (g1 ^ g2) . m = g2 . k ) by A11, A12, FINSEQ_1:def 7;
then A13: ( (g1 ^ g2) . n in rng g1 & (g1 ^ g2) . m in rng g2 ) by A11, A12, FUNCT_1:3;
now :: thesis: not (g1 ^ g2) . n meets (g1 ^ g2) . m
assume (g1 ^ g2) . n meets (g1 ^ g2) . m ; :: thesis: contradiction
then consider x being object such that
A14: ( x in (g1 ^ g2) . n & x in (g1 ^ g2) . m ) by XBOOLE_0:3;
( x in union (rng g1) & x in union (rng g2) ) by A13, A14, TARSKI:def 4;
hence contradiction by A2, A3, A5, A4, A6, XBOOLE_0:def 4; :: thesis: verum
end;
hence (g1 ^ g2) . n misses (g1 ^ g2) . m ; :: thesis: verum
end;
suppose A15: ( m1 in dom g1 & ex k being Nat st
( k in dom g2 & n1 = (len g1) + k ) ) ; :: thesis: (g1 ^ g2) . b1 misses (g1 ^ g2) . b2
then consider k being Nat such that
A16: ( k in dom g2 & n1 = (len g1) + k ) ;
( (g1 ^ g2) . n = g2 . k & (g1 ^ g2) . m = g1 . m ) by A15, A16, FINSEQ_1:def 7;
then A17: ( (g1 ^ g2) . n in rng g2 & (g1 ^ g2) . m in rng g1 ) by A15, A16, FUNCT_1:3;
now :: thesis: not (g1 ^ g2) . n meets (g1 ^ g2) . m
assume (g1 ^ g2) . n meets (g1 ^ g2) . m ; :: thesis: contradiction
then consider x being object such that
A18: ( x in (g1 ^ g2) . n & x in (g1 ^ g2) . m ) by XBOOLE_0:3;
( x in union (rng g1) & x in union (rng g2) ) by A17, A18, TARSKI:def 4;
hence contradiction by A2, A3, A5, A4, A6, XBOOLE_0:def 4; :: thesis: verum
end;
hence (g1 ^ g2) . n misses (g1 ^ g2) . m ; :: thesis: verum
end;
suppose A19: ex k being Nat st
( k in dom g2 & n1 = (len g1) + k & ex k being Nat st
( k in dom g2 & m1 = (len g1) + k ) ) ; :: thesis: (g1 ^ g2) . b1 misses (g1 ^ g2) . b2
then consider k1 being Nat such that
A20: ( k1 in dom g2 & n1 = (len g1) + k1 ) ;
consider k2 being Nat such that
A21: ( k2 in dom g2 & m1 = (len g1) + k2 ) by A19;
( (g1 ^ g2) . n = g2 . k1 & (g1 ^ g2) . m = g2 . k2 ) by A20, A21, FINSEQ_1:def 7;
hence (g1 ^ g2) . n misses (g1 ^ g2) . m by A7, A20, A21, PROB_2:def 2; :: thesis: verum
end;
end;
end;
suppose ( not n in dom (g1 ^ g2) or not m in dom (g1 ^ g2) ) ; :: thesis: (g1 ^ g2) . b1 misses (g1 ^ g2) . b2
then ( (g1 ^ g2) . n = {} or (g1 ^ g2) . m = {} ) by FUNCT_1:def 2;
hence (g1 ^ g2) . n misses (g1 ^ g2) . m ; :: thesis: verum
end;
end;
end;
then reconsider F = g1 ^ g2 as disjoint_valued FinSequence of S by PROB_2:def 2;
rng F = (rng g1) \/ (rng g2) by FINSEQ_1:31;
then Union F = A1 \/ B1 by A4, A6, ZFMISC_1:78;
hence A \/ B in P by A1, A3, A5; :: thesis: verum