let X be set ; :: thesis: for A being non empty set
for S being cap-finite-partition-closed Subset-Family of X
for P1, P2 being a_partition of A st P1 is finite Subset of S & P2 is finite Subset of S holds
ex P being a_partition of A st
( P is finite Subset of S & P '<' P1 '/\' P2 )
let x be non empty set ; :: thesis: for S being cap-finite-partition-closed Subset-Family of X
for P1, P2 being a_partition of x st P1 is finite Subset of S & P2 is finite Subset of S holds
ex P being a_partition of x st
( P is finite Subset of S & P '<' P1 '/\' P2 )
let S be cap-finite-partition-closed Subset-Family of X; :: thesis: for P1, P2 being a_partition of x st P1 is finite Subset of S & P2 is finite Subset of S holds
ex P being a_partition of x st
( P is finite Subset of S & P '<' P1 '/\' P2 )
let P1, P2 be a_partition of x; :: thesis: ( P1 is finite Subset of S & P2 is finite Subset of S implies ex P being a_partition of x st
( P is finite Subset of S & P '<' P1 '/\' P2 ) )
assume that
A1: P1 is finite Subset of S and
A2: P2 is finite Subset of S ; :: thesis: ex P being a_partition of x st
( P is finite Subset of S & P '<' P1 '/\' P2 )
defpred S1[ object , object ] means ( $1 in P1 '/\' P2 & $2 is finite Subset of S & ex A being set st
( A = $1 & $2 is a_partition of A ) );
set FOUT = { y where y is finite Subset of S : ex t being set st
( t in P1 '/\' P2 & y is a_partition of t ) } ;
{ y where y is finite Subset of S : ex t being set st
( t in P1 '/\' P2 & y is a_partition of t ) } c= bool (bool x)
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { y where y is finite Subset of S : ex t being set st
( t in P1 '/\' P2 & y is a_partition of t ) } or u in bool (bool x) )
assume u in { y where y is finite Subset of S : ex t being set st
( t in P1 '/\' P2 & y is a_partition of t ) } ; :: thesis: u in bool (bool x)
then consider y being finite Subset of S such that
A3: u = y and
A4: ex t being set st
( t in P1 '/\' P2 & y is a_partition of t ) ;
consider t0 being set such that
A5: t0 in P1 '/\' P2 and
A6: y is a_partition of t0 by A4;
reconsider u = u as set by TARSKI:1;
u c= bool x
proof
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in u or v in bool x )
assume A7: v in u ; :: thesis: v in bool x
A8: v in bool t0 by A3, A6, A7;
bool t0 c= bool x by A5, ZFMISC_1:67;
hence v in bool x by A8; :: thesis: verum
end;
hence u in bool (bool x) ; :: thesis: verum
end;
then A9: union { y where y is finite Subset of S : ex t being set st
( t in P1 '/\' P2 & y is a_partition of t ) } c= union (bool (bool x)) by ZFMISC_1:77;
A10: for u being object st u in P1 '/\' P2 holds
ex v being object st
( v in { y where y is finite Subset of S : ex t being set st
( t in P1 '/\' P2 & y is a_partition of t ) } & S1[u,v] )
proof
let u be object ; :: thesis: ( u in P1 '/\' P2 implies ex v being object st
( v in { y where y is finite Subset of S : ex t being set st
( t in P1 '/\' P2 & y is a_partition of t ) } & S1[u,v] ) )
assume A11: u in P1 '/\' P2 ; :: thesis: ex v being object st
( v in { y where y is finite Subset of S : ex t being set st
( t in P1 '/\' P2 & y is a_partition of t ) } & S1[u,v] )
reconsider u = u as set by TARSKI:1;
consider P being finite Subset of S such that
A12: P is a_partition of u by A1, A2, A11, Th1;
A13: P in { y where y is finite Subset of S : ex t being set st
( t in P1 '/\' P2 & y is a_partition of t ) } by A11, A12;
thus ex v being object st
( v in { y where y is finite Subset of S : ex t being set st
( t in P1 '/\' P2 & y is a_partition of t ) } & S1[u,v] ) by A11, A12, A13; :: thesis: verum
end;
consider f being Function such that
A14: ( dom f = P1 '/\' P2 & rng f c= { y where y is finite Subset of S : ex t being set st
( t in P1 '/\' P2 & y is a_partition of t ) } ) and
A15: for x being object st x in P1 '/\' P2 holds
S1[x,f . x] from FUNCT_1:sch 6(A10);
 A16: Union f is finite Subset of S
proof
A17: Union f c= S
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Union f or u in S )
assume u in Union f ; :: thesis: u in S
then consider v being set such that
A18: u in v and
A19: v in rng f by TARSKI:def 4;
consider w being object such that
A20: ( w in P1 '/\' P2 & v = f . w ) by A14, A19, FUNCT_1:def 3;
v is Subset of S by A15, A20;
hence u in S by A18; :: thesis: verum
end;
Union f is finite
proof
for u being object st u in dom f holds
f . u is finite by A14, A15;
hence Union f is finite by A1, A2, A14, CARD_2:88; :: thesis: verum
end;
hence Union f is finite Subset of S by A17; :: thesis: verum
end;
A22: Union f is a_partition of x
proof
A23: Union f c= bool x
proof
A24: Union f c= union { y where y is finite Subset of S : ex t being set st
( t in P1 '/\' P2 & y is a_partition of t ) } by A14, ZFMISC_1:77;
union { y where y is finite Subset of S : ex t being set st
( t in P1 '/\' P2 & y is a_partition of t ) } c= bool x by A9, ZFMISC_1:81;
hence Union f c= bool x by A24, XBOOLE_1:1; :: thesis: verum
end;
A25: union (Union f) = x
proof
thus union (Union f) c= x :: according to XBOOLE_0:def 10 :: thesis: x c= union (Union f) thus x c= union (Union f) :: thesis: verum
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in x or a in union (Union f) )
assume a in x ; :: thesis: a in union (Union f)
then A27: ( a in union P1 & a in union P2 ) by EQREL_1:def 4;
consider b1 being set such that
A28: a in b1 and
A29: b1 in P1 by A27, TARSKI:def 4;
consider b2 being set such that
A30: a in b2 and
A31: b2 in P2 by A27, TARSKI:def 4;
A32: b1 /\ b2 in INTERSECTION (P1,P2) by A29, A31, SETFAM_1:def 5;
not b1 /\ b2 = {} by A28, A30, XBOOLE_0:def 4;
then not b1 /\ b2 in {{}} by TARSKI:def 1;
then A33: b1 /\ b2 in P1 '/\' P2 by A32, XBOOLE_0:def 5;
then S1[b1 /\ b2,f . (b1 /\ b2)] by A15;
then union (f . (b1 /\ b2)) = b1 /\ b2 by EQREL_1:def 4;
then A34: a in union (f . (b1 /\ b2)) by A28, A30, XBOOLE_0:def 4;
A35: f . (b1 /\ b2) in rng f by A14, A33, FUNCT_1:def 3;
consider bb being set such that
A36: a in bb and
A37: bb in f . (b1 /\ b2) by A34, TARSKI:def 4;
bb in Union f by A35, A37, TARSKI:def 4;
hence a in union (Union f) by A36, TARSKI:def 4; :: thesis: verum
end;
end;
for A being Subset of x st A in Union f holds
( A <> {} & ( for B being Subset of x holds
( not B in Union f or A = B or A misses B ) ) )
proof
let A be Subset of x; :: thesis: ( A in Union f implies ( A <> {} & ( for B being Subset of x holds
( not B in Union f or A = B or A misses B ) ) ) )
assume A in Union f ; :: thesis: ( A <> {} & ( for B being Subset of x holds
( not B in Union f or A = B or A misses B ) ) )
then consider b being set such that
A38: ( A in b & b in rng f ) by TARSKI:def 4;
consider c being object such that
A39: c in dom f and
A40: b = f . c by A38, FUNCT_1:def 3;
reconsider c = c as set by TARSKI:1;
A41: S1[c,f . c] by A14, A15, A39;
for B being Subset of x holds
( not B in Union f or A = B or A misses B )
proof
let B be Subset of x; :: thesis: ( not B in Union f or A = B or A misses B )
assume B in Union f ; :: thesis: ( A = B or A misses B )
then consider b2 being set such that
A42: ( B in b2 & b2 in rng f ) by TARSKI:def 4;
consider c2 being object such that
A43: c2 in dom f and
A44: b2 = f . c2 by A42, FUNCT_1:def 3;
per cases ( c = c2 or not c = c2 ) ;
suppose c = c2 ; :: thesis: ( A = B or A misses B )
hence ( A = B or A misses B ) by A38, A40, A41, A42, A44, EQREL_1:def 4; :: thesis: verum
end;
suppose A45: not c = c2 ; :: thesis: ( A = B or A misses B )
consider p11, p21 being set such that
A46: p11 in P1 and
A47: p21 in P2 and
A48: c = p11 /\ p21 by A14, A39, SETFAM_1:def 5;
consider p12, p22 being set such that
A49: p12 in P1 and
A50: p22 in P2 and
A51: c2 = p12 /\ p22 by A14, A43, SETFAM_1:def 5;
A52: ( p11 /\ p21 c= p12 /\ p22 or A = B or A misses B )
proof
assume not p11 /\ p21 c= p12 /\ p22 ; :: thesis: ( A = B or A misses B )
then consider u being object such that
A53: u in p11 /\ p21 and
A54: not u in p12 /\ p22 by TARSKI:def 3;
A55: ( u in p11 & u in p21 & not u in p12 & not A = B implies A misses B )
proof
assume A56: ( u in p11 & u in p21 & not u in p12 ) ; :: thesis: ( A = B or A misses B )
( S1[c,f . c] & S1[c2,f . c2] ) by A14, A15, A39, A43;
then ( union (f . c) = p11 /\ p21 & union (f . c2) = p12 /\ p22 ) by A48, A51, EQREL_1:def 4;
then A57: ( union (f . c) c= p11 & union (f . c2) c= p12 & p11 misses p12 ) by A46, A49, A56, EQREL_1:def 4, XBOOLE_1:17;
( A c= union (f . c) & B c= union (f . c2) ) by A38, A40, A42, A44, ZFMISC_1:74;
then ( A c= p11 & B c= p12 & p11 misses p12 ) by A57, XBOOLE_1:1;
hence ( A = B or A misses B ) by XBOOLE_1:64; :: thesis: verum
end;
( u in p11 & u in p21 & not u in p22 & not A = B implies A misses B )
proof
assume A58: ( u in p11 & u in p21 & not u in p22 ) ; :: thesis: ( A = B or A misses B )
( S1[c,f . c] & S1[c2,f . c2] ) by A14, A15, A39, A43;
then ( union (f . c) = p11 /\ p21 & union (f . c2) = p12 /\ p22 ) by A48, A51, EQREL_1:def 4;
then A59: ( union (f . c) c= p21 & union (f . c2) c= p22 & p21 misses p22 ) by A47, A50, A58, EQREL_1:def 4, XBOOLE_1:17;
( A c= union (f . c) & B c= union (f . c2) ) by A38, A40, A42, A44, ZFMISC_1:74;
then ( A c= p21 & B c= p22 & p21 misses p22 ) by A59, XBOOLE_1:1;
hence ( A = B or A misses B ) by XBOOLE_1:64; :: thesis: verum
end;
hence ( A = B or A misses B ) by A53, A54, A55, XBOOLE_0:def 4; :: thesis: verum
end;
( p12 /\ p22 c= p11 /\ p21 or A = B or A misses B )
proof
assume not p12 /\ p22 c= p11 /\ p21 ; :: thesis: ( A = B or A misses B )
then consider u being object such that
A60: u in p12 /\ p22 and
A61: not u in p11 /\ p21 by TARSKI:def 3;
A62: ( u in p12 & u in p22 & not u in p11 & not A = B implies A misses B )
proof
assume A63: ( u in p12 & u in p22 & not u in p11 ) ; :: thesis: ( A = B or A misses B )
( S1[c,f . c] & S1[c2,f . c2] ) by A14, A15, A39, A43;
then ( union (f . c) = p11 /\ p21 & union (f . c2) = p12 /\ p22 ) by A48, A51, EQREL_1:def 4;
then A64: ( union (f . c) c= p11 & union (f . c2) c= p12 & p11 misses p12 ) by A46, A49, A63, EQREL_1:def 4, XBOOLE_1:17;
( A c= union (f . c) & B c= union (f . c2) ) by A38, A40, A42, A44, ZFMISC_1:74;
then ( A c= p11 & B c= p12 & p11 misses p12 ) by A64, XBOOLE_1:1;
hence ( A = B or A misses B ) by XBOOLE_1:64; :: thesis: verum
end;
( u in p12 & u in p22 & not u in p21 & not A = B implies A misses B )
proof
assume A65: ( u in p12 & u in p22 & not u in p21 ) ; :: thesis: ( A = B or A misses B )
( S1[c,f . c] & S1[c2,f . c2] ) by A14, A15, A39, A43;
then ( union (f . c) = p11 /\ p21 & union (f . c2) = p12 /\ p22 ) by A48, A51, EQREL_1:def 4;
then A66: ( union (f . c) c= p21 & union (f . c2) c= p22 & p21 misses p22 ) by A47, A50, A65, EQREL_1:def 4, XBOOLE_1:17;
( A c= union (f . c) & B c= union (f . c2) ) by A38, A40, A42, A44, ZFMISC_1:74;
then ( A c= p21 & B c= p22 & p21 misses p22 ) by A66, XBOOLE_1:1;
hence ( A = B or A misses B ) by XBOOLE_1:64; :: thesis: verum
end;
hence ( A = B or A misses B ) by A60, A61, A62, XBOOLE_0:def 4; :: thesis: verum
end;
hence ( A = B or A misses B ) by A45, A48, A51, A52, XBOOLE_0:def 10; :: thesis: verum
end;
end;
end;
hence ( A <> {} & ( for B being Subset of x holds
( not B in Union f or A = B or A misses B ) ) ) by A38, A40, A41; :: thesis: verum
end;
hence Union f is a_partition of x by A23, A25, EQREL_1:def 4; :: thesis: verum
end;
Union f '<' P1 '/\' P2
proof
for a being set st a in Union f holds
ex b being set st
( b in P1 '/\' P2 & a c= b )
proof
let a be set ; :: thesis: ( a in Union f implies ex b being set st
( b in P1 '/\' P2 & a c= b ) )
assume a in Union f ; :: thesis: ex b being set st
( b in P1 '/\' P2 & a c= b )
then consider b being set such that
A67: a in b and
A68: b in rng f by TARSKI:def 4;
consider c being object such that
A69: c in dom f and
A70: b = f . c by A68, FUNCT_1:def 3;
reconsider c = c as set by TARSKI:1;
S1[c,f . c] by A14, A15, A69;
hence ex b being set st
( b in P1 '/\' P2 & a c= b ) by A67, A70; :: thesis: verum
end;
hence Union f '<' P1 '/\' P2 by SETFAM_1:def 2; :: thesis: verum
end;
hence ex P being a_partition of x st
( P is finite Subset of S & P '<' P1 '/\' P2 ) by A16, A22; :: thesis: verum