let X be set ; :: thesis: for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X holds S is diff-finite-partition-closed
let S be cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X; :: thesis: S is diff-finite-partition-closed
for S1, S2 being Element of S st not S1 \ S2 is empty holds
ex P0 being finite Subset of S st P0 is a_partition of S1 \ S2
proof
let S1, S2 be Element of S; :: thesis: ( not S1 \ S2 is empty implies ex P0 being finite Subset of S st P0 is a_partition of S1 \ S2 )
assume not S1 \ S2 is empty ; :: thesis: ex P0 being finite Subset of S st P0 is a_partition of S1 \ S2
consider P0 being finite Subset of S such that
A1: P0 is a_partition of S1 /\ S2 by Lem7;
A2: union P0 c= S1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union P0 or x in S1 )
assume x in union P0 ; :: thesis: x in S1
then consider x0 being set such that
A3: ( x in x0 & x0 in P0 ) by TARSKI:def 4;
S1 /\ S2 c= S1 by XBOOLE_1:17;
then x0 c= S1 by A1, A3, XBOOLE_1:1;
hence x in S1 by A3; :: thesis: verum
end;
P0 is a_partition of union P0 by A1, EQREL_1:def 4;
then consider R being finite Subset of S such that
union R misses union P0 and
A4: P0 \/ R is a_partition of S1 by A2, Thm5;
A5: ( R /\ (bool (S1 \ S2)) is finite Subset of S & R /\ (bool (S1 \ S2)) is a_partition of S1 \ S2 )
proof
A6: R /\ (bool (S1 \ S2)) is Subset-Family of (S1 \ S2) by XBOOLE_1:17;
A7: union (R /\ (bool (S1 \ S2))) = S1 \ S2
proof
A8: union (R /\ (bool (S1 \ S2))) c= S1 \ S2
proof
union (R /\ (bool (S1 \ S2))) c= union (bool (S1 \ S2)) by XBOOLE_1:17, ZFMISC_1:77;
hence union (R /\ (bool (S1 \ S2))) c= S1 \ S2 by ZFMISC_1:81; :: thesis: verum
end;
S1 \ S2 c= union (R /\ (bool (S1 \ S2)))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S1 \ S2 or x in union (R /\ (bool (S1 \ S2))) )
assume A9: x in S1 \ S2 ; :: thesis: x in union (R /\ (bool (S1 \ S2)))
then ( x in S1 & not x in S2 ) by XBOOLE_0:def 5;
then x in union (P0 \/ R) by A4, EQREL_1:def 4;
then consider X0 being set such that
A10: x in X0 and
A11: X0 in P0 \/ R by TARSKI:def 4;
A12: ( X0 in P0 implies X0 in bool S2 )
proof
assume A13: X0 in P0 ; :: thesis: X0 in bool S2
S1 /\ S2 c= S2 by XBOOLE_1:17;
then X0 c= S2 by A13, A1, XBOOLE_1:1;
hence X0 in bool S2 ; :: thesis: verum
end;
X0 in R /\ (bool (S1 \ S2))
proof
A14: X0 in R by A12, A9, XBOOLE_0:def 5, A10, A11, XBOOLE_0:def 3;
X0 c= S1 \ S2
proof
assume not X0 c= S1 \ S2 ; :: thesis: contradiction
then consider xx being object such that
A15: xx in X0 and
A16: not xx in S1 \ S2 by TARSKI:def 3;
( xx in X0 & X0 in R ) by A12, A9, XBOOLE_0:def 5, A10, A11, XBOOLE_0:def 3, A15;
then A17: xx in union R by TARSKI:def 4;
union R c= union (P0 \/ R) by XBOOLE_1:7, ZFMISC_1:77;
then A18: union R c= S1 by A4, EQREL_1:def 4;
A19: ( not xx in S1 or xx in S2 ) by A16, XBOOLE_0:def 5;
X0 in P0
proof
A20: xx in S1 /\ S2 by A18, A17, A19, XBOOLE_0:def 4;
union P0 = S1 /\ S2 by A1, EQREL_1:def 4;
then consider PP being set such that
A21: xx in PP and
A22: PP in P0 by A20, TARSKI:def 4;
A23: xx in PP /\ X0 by A21, A15, XBOOLE_0:def 4;
( PP in P0 \/ R & X0 in P0 \/ R ) by A22, XBOOLE_0:def 3, A11;
hence X0 in P0 by A22, A4, A23, XBOOLE_0:def 7, EQREL_1:def 4; :: thesis: verum
end;
hence contradiction by A10, A12, A9, XBOOLE_0:def 5; :: thesis: verum
end;
hence X0 in R /\ (bool (S1 \ S2)) by A14, XBOOLE_0:def 4; :: thesis: verum
end;
hence x in union (R /\ (bool (S1 \ S2))) by A10, TARSKI:def 4; :: thesis: verum
end;
hence union (R /\ (bool (S1 \ S2))) = S1 \ S2 by A8; :: thesis: verum
end;
for A being Subset of (S1 \ S2) st A in R /\ (bool (S1 \ S2)) holds
( A <> {} & ( for B being Subset of (S1 \ S2) holds
( not B in R /\ (bool (S1 \ S2)) or A = B or A misses B ) ) )
proof
let A be Subset of (S1 \ S2); :: thesis: ( A in R /\ (bool (S1 \ S2)) implies ( A <> {} & ( for B being Subset of (S1 \ S2) holds
( not B in R /\ (bool (S1 \ S2)) or A = B or A misses B ) ) ) )
assume A24: A in R /\ (bool (S1 \ S2)) ; :: thesis: ( A <> {} & ( for B being Subset of (S1 \ S2) holds
( not B in R /\ (bool (S1 \ S2)) or A = B or A misses B ) ) )
A in R by A24, XBOOLE_0:def 4;
then A25: A in P0 \/ R by XBOOLE_0:def 3;
now :: thesis: for B being Subset of (S1 \ S2) holds
( not B in R /\ (bool (S1 \ S2)) or A = B or A misses B )
let B be Subset of (S1 \ S2); :: thesis: ( not B in R /\ (bool (S1 \ S2)) or A = B or A misses B )
assume A26: B in R /\ (bool (S1 \ S2)) ; :: thesis: ( A = B or A misses B )
B in R by A26, XBOOLE_0:def 4;
then B in P0 \/ R by XBOOLE_0:def 3;
hence ( A = B or A misses B ) by A25, A4, EQREL_1:def 4; :: thesis: verum
end;
hence ( A <> {} & ( for B being Subset of (S1 \ S2) holds
( not B in R /\ (bool (S1 \ S2)) or A = B or A misses B ) ) ) by A25, A4; :: thesis: verum
end;
hence ( R /\ (bool (S1 \ S2)) is finite Subset of S & R /\ (bool (S1 \ S2)) is a_partition of S1 \ S2 ) by A6, A7, EQREL_1:def 4; :: thesis: verum
end;
thus ex P0 being finite Subset of S st P0 is a_partition of S1 \ S2 by A5; :: thesis: verum
end;
hence S is diff-finite-partition-closed ; :: thesis: verum