let X be set ; :: thesis: for S being non empty Subset-Family of X st ( for A, B being Element of S ex P being finite Subset of S st P is a_partition of A /\ B ) & ( for C, D being Element of S st D c= C holds
ex P being finite Subset of S st P is a_partition of C \ D ) holds
for A being Element of S
for Q being finite Subset of S st not A is empty & union Q c= A & Q is a_partition of union Q holds
ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )
let S be non empty Subset-Family of X; :: thesis: ( ( for A, B being Element of S ex P being finite Subset of S st P is a_partition of A /\ B ) & ( for C, D being Element of S st D c= C holds
ex P being finite Subset of S st P is a_partition of C \ D ) implies for A being Element of S
for Q being finite Subset of S st not A is empty & union Q c= A & Q is a_partition of union Q holds
ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A ) )
assume A1: for A, B being Element of S ex P being finite Subset of S st P is a_partition of A /\ B ; :: thesis: ( ex C, D being Element of S st
( D c= C & ( for P being finite Subset of S holds P is not a_partition of C \ D ) ) or for A being Element of S
for Q being finite Subset of S st not A is empty & union Q c= A & Q is a_partition of union Q holds
ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A ) )
assume A2: for C, D being Element of S st D c= C holds
ex P being finite Subset of S st P is a_partition of C \ D ; :: thesis: for A being Element of S
for Q being finite Subset of S st not A is empty & union Q c= A & Q is a_partition of union Q holds
ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )
let A be Element of S; :: thesis: for Q being finite Subset of S st not A is empty & union Q c= A & Q is a_partition of union Q holds
ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )
let Q be finite Subset of S; :: thesis: ( not A is empty & union Q c= A & Q is a_partition of union Q implies ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A ) )
assume that
A3: not A is empty and
A4: union Q c= A and
A5: Q is a_partition of union Q ; :: thesis: ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )
consider qq being FinSequence such that
A6: Q = rng qq by FINSEQ_1:52;
A7: for i being set st i in dom qq holds
qq . i <> {}
proof
let i be set ; :: thesis: ( i in dom qq implies qq . i <> {} )
assume i in dom qq ; :: thesis: qq . i <> {}
then qq . i in Q by A6, FUNCT_1:def 3;
hence qq . i <> {} by A5; :: thesis: verum
end;
per cases ( qq = {} or qq <> {} ) ;
suppose A8: qq = {} ; :: thesis: ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )
then A9: Q = {} by A6;
A10: {A} is finite Subset of S by SUBSET_1:33;
A11: {A} is a_partition of A by A3, EQREL_1:39;
A12: union {A} misses union Q {} \/ {A} = {A} ;
hence ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A ) by A9, A10, A11, A12; :: thesis: verum
end;
suppose A13: qq <> {} ; :: thesis: ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A )
defpred S1[ Nat] means for n being Nat st $1 = n & 1 <= n & n <= len qq holds
ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A );
A14: S1[1]
proof
let n be Nat; :: thesis: ( 1 = n & 1 <= n & n <= len qq implies ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A ) )
assume A15: ( n = 1 & 1 <= n & n <= len qq ) ; :: thesis: ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A )
A16: 1 in Seg (len qq) by A15;
then A17: 1 in dom qq by FINSEQ_1:def 3;
then A18: rng (qq | (Seg 1)) = {(qq . 1)} by FINSEQ_1:2, FUNCT_1:98;
A19: qq . 1 c= A A20: qq . 1 is Element of S
proof
1 in dom qq by A16, FINSEQ_1:def 3;
then qq . 1 in rng qq by FUNCT_1:def 3;
hence qq . 1 is Element of S by A6; :: thesis: verum
end;
then consider PP being finite Subset of S such that
A21: PP is a_partition of A \ (qq . 1) by A2, A19;
A21a: union PP misses qq . 1
proof
union PP = A \ (qq . 1) by A21, EQREL_1:def 4;
hence union PP misses qq . 1 by XBOOLE_1:79; :: thesis: verum
end;
{(qq . 1)} \/ PP is a_partition of A by A17, A7, A19, A20, A21, Lem5;
hence ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A ) by A15, A18, A21a; :: thesis: verum
end;
A23: for j being Nat st 1 <= j & S1[j] holds
S1[j + 1]
proof
let j be Nat; :: thesis: ( 1 <= j & S1[j] implies S1[j + 1] )
assume that
A24: 1 <= j and
A25: S1[j] ; :: thesis: S1[j + 1]
for n being Nat st j + 1 = n & 1 <= n & n <= len qq holds
ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A )
proof
let n be Nat; :: thesis: ( j + 1 = n & 1 <= n & n <= len qq implies ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A ) )
assume that
A26: j + 1 = n and
A27: 1 <= n and
A28: n <= len qq ; :: thesis: ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A )
per cases ( j <= len qq or not j <= len qq ) ;
suppose j <= len qq ; :: thesis: ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A )
then consider R1 being finite Subset of S such that
A29: union R1 misses union (rng (qq | (Seg j))) and
A30: (rng (qq | (Seg j))) \/ R1 is a_partition of A by A24, A25;
A31: n in Seg (len qq) by A27, A28;
then A32: j + 1 in dom qq by A26, FINSEQ_1:def 3;
Seg (j + 1) = (Seg j) \/ {(j + 1)} by FINSEQ_1:9;
then qq | (Seg (j + 1)) = (qq | (Seg j)) \/ (qq | {(j + 1)}) by RELAT_1:78;
then A33: rng (qq | (Seg (j + 1))) = (rng (qq | (Seg j))) \/ (rng (qq | {(j + 1)})) by RELAT_1:12;
then A34: rng (qq | (Seg (j + 1))) = (rng (qq | (Seg j))) \/ {(qq . (j + 1))} by A32, FUNCT_1:98;
per cases ( qq . (j + 1) in rng (qq | (Seg j)) or not qq . (j + 1) in rng (qq | (Seg j)) ) ;
suppose qq . (j + 1) in rng (qq | (Seg j)) ; :: thesis: ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A )
then (rng (qq | (Seg j))) \/ {(qq . (j + 1))} = rng (qq | (Seg j)) by ZFMISC_1:31, XBOOLE_1:12;
then rng (qq | (Seg (j + 1))) = rng (qq | (Seg j)) by A33, A32, FUNCT_1:98;
hence ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A ) by A26, A29, A30; :: thesis: verum
end;
suppose A35: not qq . (j + 1) in rng (qq | (Seg j)) ; :: thesis: ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A )
A36: qq . (j + 1) misses union (rng (qq | (Seg j)))
proof
assume not (qq . (j + 1)) /\ (union (rng (qq | (Seg j)))) = {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x0 being object such that
A37: x0 in (qq . (j + 1)) /\ (union (rng (qq | (Seg j)))) by XBOOLE_0:def 1;
( x0 in qq . (j + 1) & x0 in Union (qq | (Seg j)) ) by A37, XBOOLE_0:def 4;
then consider y0 being set such that
A38: ( x0 in y0 & y0 in rng (qq | (Seg j)) ) by TARSKI:def 4;
consider j0 being object such that
A39: j0 in dom (qq | (Seg j)) and
A40: y0 = (qq | (Seg j)) . j0 by A38, FUNCT_1:def 3;
( x0 in qq . j0 & x0 in qq . (j + 1) ) by A37, XBOOLE_0:def 4, A38, A40, A39, FUNCT_1:47;
then A41: x0 in (qq . j0) /\ (qq . (j + 1)) by XBOOLE_0:def 4;
dom (qq | (Seg j)) c= dom qq by RELAT_1:60;
then ( j0 in dom qq & j + 1 in dom qq ) by A39, A31, A26, FINSEQ_1:def 3;
then ( qq . j0 in Q & qq . (j + 1) in Q ) by A6, FUNCT_1:def 3;
then qq . j0 = qq . (j + 1) by A5, A41, XBOOLE_0:def 7, EQREL_1:def 4;
hence contradiction by A35, A38, A40, A39, FUNCT_1:47; :: thesis: verum
end;
A42: qq . (j + 1) in Q by A32, A6, FUNCT_1:def 3;
then A43: qq . (j + 1) c= union Q by ZFMISC_1:74;
then A44: qq . (j + 1) c= A by A4, XBOOLE_1:1;
consider RA being finite Subset of S such that
A45: RA is a_partition of A \ (qq . (j + 1)) by A42, A43, A4, XBOOLE_1:1, A2;
A46: for x being set st x in [:R1,RA:] holds
ex x1, x2 being set ex px being finite Subset of S st
( x = [x1,x2] & x1 in R1 & x2 in RA & px is a_partition of x1 /\ x2 )
proof
let x be set ; :: thesis: ( x in [:R1,RA:] implies ex x1, x2 being set ex px being finite Subset of S st
( x = [x1,x2] & x1 in R1 & x2 in RA & px is a_partition of x1 /\ x2 ) )
assume x in [:R1,RA:] ; :: thesis: ex x1, x2 being set ex px being finite Subset of S st
( x = [x1,x2] & x1 in R1 & x2 in RA & px is a_partition of x1 /\ x2 )
then consider x1, x2 being object such that
A47: ( x1 in R1 & x2 in RA & x = [x1,x2] ) by ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as set by TARSKI:1;
consider px being finite Subset of S such that
A48: px is a_partition of x1 /\ x2 by A47, A1;
thus ex x1, x2 being set ex px being finite Subset of S st
( x = [x1,x2] & x1 in R1 & x2 in RA & px is a_partition of x1 /\ x2 ) by A47, A48; :: thesis: verum
end;
defpred S2[ object , object ] means ( $1 in [:R1,RA:] & ex x1, x2 being set ex px being finite Subset of S st
( $1 = [x1,x2] & x1 in R1 & x2 in RA & $2 = px & $2 is a_partition of x1 /\ x2 ) );
set XA = { x where x is finite Subset of S : verum } ;
A49: for x being object st x in [:R1,RA:] holds
ex y being object st
( y in { x where x is finite Subset of S : verum } & S2[x,y] )
proof
let x be object ; :: thesis: ( x in [:R1,RA:] implies ex y being object st
( y in { x where x is finite Subset of S : verum } & S2[x,y] ) )
assume A50: x in [:R1,RA:] ; :: thesis: ex y being object st
( y in { x where x is finite Subset of S : verum } & S2[x,y] )
then consider x1, x2 being set , px being finite Subset of S such that
A51: x = [x1,x2] and
A52: ( x1 in R1 & x2 in RA ) and
A53: px is a_partition of x1 /\ x2 by A46;
px in { x where x is finite Subset of S : verum } ;
hence ex y being object st
( y in { x where x is finite Subset of S : verum } & S2[x,y] ) by A50, A51, A52, A53; :: thesis: verum
end;
consider h being Function such that
A55: ( dom h = [:R1,RA:] & rng h c= { x where x is finite Subset of S : verum } ) and
A56: for x being object st x in [:R1,RA:] holds
S2[x,h . x] from FUNCT_1:sch 6(A49);
A57: Union h is finite
proof
for x being set st x in rng h holds
x is finite
proof
let x be set ; :: thesis: ( x in rng h implies x is finite )
assume x in rng h ; :: thesis: x is finite
then consider x0 being object such that
A58: x0 in dom h and
A59: x = h . x0 by FUNCT_1:def 3;
consider x1, x2 being set , px being finite Subset of S such that
x0 = [x1,x2] and
( x1 in R1 & x2 in RA ) and
A60: x = px and
x is a_partition of x1 /\ x2 by A58, A59, A55, A56;
thus x is finite by A60; :: thesis: verum
end;
hence Union h is finite by A55, FINSET_1:7, FINSET_1:8; :: thesis: verum
end;
A61: rng h c= bool S
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng h or x in bool S )
assume x in rng h ; :: thesis: x in bool S
then consider x0 being object such that
A62: x0 in dom h and
A63: x = h . x0 by FUNCT_1:def 3;
consider x1, x2 being set , px being finite Subset of S such that
x0 = [x1,x2] and
( x1 in R1 & x2 in RA ) and
A64: x = px and
x is a_partition of x1 /\ x2 by A62, A63, A55, A56;
thus x in bool S by A64; :: thesis: verum
end;
A65: Union h c= S
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union h or x in S )
assume x in Union h ; :: thesis: x in S
then ex x0 being set st
( x in x0 & x0 in rng h ) by TARSKI:def 4;
hence x in S by A61; :: thesis: verum
end;
A68: union (Union h) misses union (rng (qq | (Seg n)))
proof
(union (Union h)) /\ (union (rng (qq | (Seg (j + 1))))) c= {}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union (Union h)) /\ (union (rng (qq | (Seg (j + 1))))) or x in {} )
assume x in (union (Union h)) /\ (union (rng (qq | (Seg (j + 1))))) ; :: thesis: x in {}
then A69: ( x in union (Union h) & x in union (rng (qq | (Seg (j + 1)))) ) by XBOOLE_0:def 4;
then consider x0 being set such that
A70: x in x0 and
A71: x0 in Union h by TARSKI:def 4;
consider x1 being set such that
A72: x in x1 and
A73: x1 in rng (qq | (Seg (j + 1))) by A69, TARSKI:def 4;
x0 /\ x1 = {}
proof
x0 /\ x1 c= {}
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in x0 /\ x1 or u in {} )
assume A74: u in x0 /\ x1 ; :: thesis: u in {}
then A75: ( u in x0 & u in x1 ) by XBOOLE_0:def 4;
consider x0a being set such that
A76: x0 in x0a and
A77: x0a in rng h by A71, TARSKI:def 4;
consider t being object such that
A78: t in dom h and
A79: h . t = x0a by A77, FUNCT_1:def 3;
consider ax1, ax2 being set , apx being finite Subset of S such that
t = [ax1,ax2] and
A80: ( ax1 in R1 & ax2 in RA ) and
A81: x0a = apx and
A82: x0a is a_partition of ax1 /\ ax2 by A78, A79, A55, A56;
A83: ( u in x0 & x0 in apx ) by A74, XBOOLE_0:def 4, A76, A81;
( u in ax1 & ax1 in R1 ) by A83, A82, A81, A80, XBOOLE_0:def 4;
then u in union R1 by TARSKI:def 4;
then A85: not u in union (rng (qq | (Seg j))) by A29, XBOOLE_0:def 4;
( u in ax2 & ax2 in RA ) by A83, A82, A81, XBOOLE_0:def 4, A80;
then A85a: not u in qq . (j + 1) by A45, XBOOLE_0:def 5;
union (rng (qq | (Seg (j + 1)))) = union ((rng (qq | (Seg j))) \/ {(qq . (j + 1))}) by A33, A32, FUNCT_1:98;
then union (rng (qq | (Seg (j + 1)))) = (union (rng (qq | (Seg j)))) \/ (union {(qq . (j + 1))}) by ZFMISC_1:78;
then not u in union (rng (qq | (Seg (j + 1)))) by A85, XBOOLE_0:def 3, A85a;
hence u in {} by A75, A73, TARSKI:def 4; :: thesis: verum
end;
hence x0 /\ x1 = {} ; :: thesis: verum
end;
hence x in {} by A70, A72, XBOOLE_0:def 4; :: thesis: verum
end;
hence union (Union h) misses union (rng (qq | (Seg n))) by A26; :: thesis: verum
end;
(rng (qq | (Seg n))) \/ (Union h) is a_partition of A
proof
A87: (rng (qq | (Seg n))) \/ (Union h) c= bool A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng (qq | (Seg n))) \/ (Union h) or x in bool A )
assume A88: x in (rng (qq | (Seg n))) \/ (Union h) ; :: thesis: x in bool A
A89: ( x in rng (qq | (Seg n)) implies x in bool A )
proof
assume x in rng (qq | (Seg n)) ; :: thesis: x in bool A
then x in (rng (qq | (Seg j))) \/ {(qq . (j + 1))} by A26, A33, A32, FUNCT_1:98;
then ( x in rng (qq | (Seg j)) or x in {(qq . (j + 1))} ) by XBOOLE_0:def 3;
then A90: ( x in rng (qq | (Seg j)) or x = qq . (j + 1) ) by TARSKI:def 1;
( x in rng (qq | (Seg j)) implies x in bool A )
proof
assume x in rng (qq | (Seg j)) ; :: thesis: x in bool A
then x in (rng (qq | (Seg j))) \/ R1 by XBOOLE_1:7, TARSKI:def 3;
hence x in bool A by A30; :: thesis: verum
end;
hence x in bool A by A90, A44; :: thesis: verum
end;
( x in Union h implies x in bool A )
proof
assume x in Union h ; :: thesis: x in bool A
then consider y being set such that
A91: x in y and
A92: y in rng h by TARSKI:def 4;
consider z being object such that
A93: z in dom h and
A94: y = h . z by A92, FUNCT_1:def 3;
consider x1, x2 being set , px being finite Subset of S such that
z = [x1,x2] and
A95: ( x1 in R1 & x2 in RA ) and
y = px and
A96: y is a_partition of x1 /\ x2 by A55, A56, A93, A94;
A97: x1 /\ x2 c= x2 by XBOOLE_1:17;
A \ (qq . (j + 1)) c= A by XBOOLE_1:36;
then x2 c= A by A45, A95, XBOOLE_1:1;
then x1 /\ x2 c= A by A97, XBOOLE_1:1;
then bool (x1 /\ x2) c= bool A by ZFMISC_1:67;
then y c= bool A by A96, XBOOLE_1:1;
hence x in bool A by A91; :: thesis: verum
end;
hence x in bool A by A88, A89, XBOOLE_0:def 3; :: thesis: verum
end;
A98: union ((rng (qq | (Seg n))) \/ (Union h)) = A
proof
A99: union ((rng (qq | (Seg n))) \/ (Union h)) c= A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union ((rng (qq | (Seg n))) \/ (Union h)) or x in A )
assume x in union ((rng (qq | (Seg n))) \/ (Union h)) ; :: thesis: x in A
then consider y being set such that
A100: x in y and
A101: y in (rng (qq | (Seg n))) \/ (Union h) by TARSKI:def 4;
thus x in A by A100, A87, A101; :: thesis: verum
end;
A c= union ((rng (qq | (Seg n))) \/ (Union h))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in union ((rng (qq | (Seg n))) \/ (Union h)) )
assume x in A ; :: thesis: x in union ((rng (qq | (Seg n))) \/ (Union h))
then x in union ((rng (qq | (Seg j))) \/ R1) by A30, EQREL_1:def 4;
then A102: x in (union (rng (qq | (Seg j)))) \/ (union R1) by ZFMISC_1:78;
A103: ( x in union (rng (qq | (Seg j))) implies x in union (rng (qq | (Seg (j + 1)))) )
proof
assume A104: x in union (rng (qq | (Seg j))) ; :: thesis: x in union (rng (qq | (Seg (j + 1))))
union (rng (qq | (Seg j))) c= union (rng (qq | (Seg (j + 1)))) by ZFMISC_1:77, A33, XBOOLE_1:7;
hence x in union (rng (qq | (Seg (j + 1)))) by A104; :: thesis: verum
end;
( not x in union R1 or x in union (Union h) or x in union (rng (qq | (Seg (j + 1)))) )
proof
assume A105: x in union R1 ; :: thesis: ( x in union (Union h) or x in union (rng (qq | (Seg (j + 1)))) )
union R1 c= (union R1) \/ (union (rng (qq | (Seg j)))) by XBOOLE_1:7;
then union R1 c= union (R1 \/ (rng (qq | (Seg j)))) by ZFMISC_1:78;
then A106: union R1 c= A by A30, EQREL_1:def 4;
A107: ( x in qq . (j + 1) implies x in union (rng (qq | (Seg (j + 1)))) )
proof
assume A108: x in qq . (j + 1) ; :: thesis: x in union (rng (qq | (Seg (j + 1))))
union (rng (qq | (Seg (j + 1)))) = union ((rng (qq | (Seg j))) \/ {(qq . (j + 1))}) by A33, A32, FUNCT_1:98;
then A108aa: union (rng (qq | (Seg (j + 1)))) = (union (rng (qq | (Seg j)))) \/ (union {(qq . (j + 1))}) by ZFMISC_1:78;
qq . (j + 1) c= union (rng (qq | (Seg (j + 1)))) by A108aa, XBOOLE_1:7;
hence x in union (rng (qq | (Seg (j + 1)))) by A108; :: thesis: verum
end;
( not x in qq . (j + 1) implies x in union (Union h) )
proof
assume not x in qq . (j + 1) ; :: thesis: x in union (Union h)
then x in A \ (qq . (j + 1)) by A105, A106, XBOOLE_0:def 5;
then x in union RA by A45, EQREL_1:def 4;
then consider y being set such that
A109: x in y and
A110: y in RA by TARSKI:def 4;
consider z being set such that
A111: x in z and
A112: z in R1 by A105, TARSKI:def 4;
consider t being set such that
A113: t = [z,y] ;
A114: [z,y] in [:R1,RA:] by A110, A112, ZFMISC_1:def 2;
A115: [z,y] in dom h by A110, A112, ZFMISC_1:def 2, A55;
consider x1, x2 being set , px being finite Subset of S such that
A116: t = [x1,x2] and
( x1 in R1 & x2 in RA ) and
h . t = px and
A117: h . t is a_partition of x1 /\ x2 by A113, A56, A114;
A118: ( z = x1 & y = x2 ) by A113, A116, XTUPLE_0:1;
x in z /\ y by A109, A111, XBOOLE_0:def 4;
then A119: x in union (h . t) by A117, A118, EQREL_1:def 4;
h . t in rng h by A113, A115, FUNCT_1:def 3;
then union (h . t) c= union (union (rng h)) by ZFMISC_1:74, ZFMISC_1:77;
hence x in union (Union h) by A119; :: thesis: verum
end;
hence ( x in union (Union h) or x in union (rng (qq | (Seg (j + 1)))) ) by A107; :: thesis: verum
end;
then x in (union (rng (qq | (Seg (j + 1))))) \/ (union (Union h)) by A102, A103, XBOOLE_0:def 3;
hence x in union ((rng (qq | (Seg n))) \/ (Union h)) by ZFMISC_1:78, A26; :: thesis: verum
end;
hence union ((rng (qq | (Seg n))) \/ (Union h)) = A by A99; :: thesis: verum
end;
for a being Subset of A st a in (rng (qq | (Seg n))) \/ (Union h) holds
( a <> {} & ( for b being Subset of A holds
( not b in (rng (qq | (Seg n))) \/ (Union h) or a = b or a misses b ) ) )
proof
let a be Subset of A; :: thesis: ( a in (rng (qq | (Seg n))) \/ (Union h) implies ( a <> {} & ( for b being Subset of A holds
( not b in (rng (qq | (Seg n))) \/ (Union h) or a = b or a misses b ) ) ) )
assume A120: a in (rng (qq | (Seg n))) \/ (Union h) ; :: thesis: ( a <> {} & ( for b being Subset of A holds
( not b in (rng (qq | (Seg n))) \/ (Union h) or a = b or a misses b ) ) )
A121: ( a in (rng (qq | (Seg j))) \/ {(qq . (j + 1))} or a in Union h ) by A34, A120, A26, XBOOLE_0:def 3;
A122: a <> {}
proof
A123: ( a in rng (qq | (Seg (j + 1))) implies a <> {} )
proof
assume a in rng (qq | (Seg (j + 1))) ; :: thesis: a <> {}
then A124: a in (rng (qq | (Seg j))) \/ {(qq . (j + 1))} by A33, A32, FUNCT_1:98;
A125: ( a in rng (qq | (Seg j)) implies a <> {} )
proof
assume A126: a in rng (qq | (Seg j)) ; :: thesis: a <> {}
rng (qq | (Seg j)) c= (rng (qq | (Seg j))) \/ R1 by XBOOLE_1:7;
hence a <> {} by A126, A30; :: thesis: verum
end;
( a in {(qq . (j + 1))} implies a <> {} )
proof
assume a in {(qq . (j + 1))} ; :: thesis: a <> {}
then a = qq . (j + 1) by TARSKI:def 1;
hence a <> {} by A7, A32; :: thesis: verum
end;
hence a <> {} by A124, A125, XBOOLE_0:def 3; :: thesis: verum
end;
( a in Union h implies a <> {} )
proof
assume a in Union h ; :: thesis: a <> {}
then consider a1 being set such that
A127: a in a1 and
A128: a1 in rng h by TARSKI:def 4;
consider a2 being object such that
A129: a2 in dom h and
A130: a1 = h . a2 by A128, FUNCT_1:def 3;
consider x1, x2 being set , px being finite Subset of S such that
( a2 = [x1,x2] & x1 in R1 & x2 in RA & a1 = px ) and
A131: a1 is a_partition of x1 /\ x2 by A129, A55, A56, A130;
thus a <> {} by A127, A131; :: thesis: verum
end;
hence a <> {} by A120, A26, XBOOLE_0:def 3, A123; :: thesis: verum
end;
for b being Subset of A holds
( not b in (rng (qq | (Seg n))) \/ (Union h) or a = b or a misses b )
proof
let b be Subset of A; :: thesis: ( not b in (rng (qq | (Seg n))) \/ (Union h) or a = b or a misses b )
assume b in (rng (qq | (Seg n))) \/ (Union h) ; :: thesis: ( a = b or a misses b )
then ( b in rng (qq | (Seg (j + 1))) or b in Union h ) by A26, XBOOLE_0:def 3;
then A132: ( b in (rng (qq | (Seg j))) \/ {(qq . (j + 1))} or b in Union h ) by A33, A32, FUNCT_1:98;
A133: ( not b in rng (qq | (Seg j)) or a = b or a misses b )
proof
assume A134: b in rng (qq | (Seg j)) ; :: thesis: ( a = b or a misses b )
then A135: b in (rng (qq | (Seg j))) \/ R1 by XBOOLE_1:7, TARSKI:def 3;
A136: ( not a in rng (qq | (Seg j)) or a = b or a misses b )
proof
assume a in rng (qq | (Seg j)) ; :: thesis: ( a = b or a misses b )
then a in (rng (qq | (Seg j))) \/ R1 by XBOOLE_1:7, TARSKI:def 3;
hence ( a = b or a misses b ) by A135, A30, EQREL_1:def 4; :: thesis: verum
end;
A137: ( not a in {(qq . (j + 1))} or a = b or a misses b )
proof
assume a in {(qq . (j + 1))} ; :: thesis: ( a = b or a misses b )
then a misses Union (qq | (Seg j)) by A36, TARSKI:def 1;
hence ( a = b or a misses b ) by XBOOLE_1:63, A134, ZFMISC_1:74; :: thesis: verum
end;
( not a in Union h or a = b or a misses b )
proof
assume a in Union h ; :: thesis: ( a = b or a misses b )
then A138: a c= union (Union h) by ZFMISC_1:74;
rng (qq | (Seg j)) c= rng (qq | (Seg (j + 1))) by A33, XBOOLE_1:7;
then b c= union (rng (qq | (Seg n))) by A134, A26, ZFMISC_1:74;
hence ( a = b or a misses b ) by A138, A68, XBOOLE_1:64; :: thesis: verum
end;
hence ( a = b or a misses b ) by A121, XBOOLE_0:def 3, A136, A137; :: thesis: verum
end;
A139: ( not b in {(qq . (j + 1))} or a = b or a misses b )
proof
assume A140: b in {(qq . (j + 1))} ; :: thesis: ( a = b or a misses b )
A141: ( not a in rng (qq | (Seg j)) or a = b or a misses b )
proof
assume A142: a in rng (qq | (Seg j)) ; :: thesis: ( a = b or a misses b )
b misses Union (qq | (Seg j)) by A140, TARSKI:def 1, A36;
hence ( a = b or a misses b ) by A142, ZFMISC_1:74, XBOOLE_1:63; :: thesis: verum
end;
A143: ( not a in {(qq . (j + 1))} or a = b or a misses b )
proof
assume a in {(qq . (j + 1))} ; :: thesis: ( a = b or a misses b )
then ( a = qq . (j + 1) & b = qq . (j + 1) ) by A140, TARSKI:def 1;
hence ( a = b or a misses b ) ; :: thesis: verum
end;
( not a in Union h or a = b or a misses b )
proof
assume a in Union h ; :: thesis: ( a = b or a misses b )
then consider a1 being set such that
A144: a in a1 and
A145: a1 in rng h by TARSKI:def 4;
consider t being object such that
A146: t in dom h and
A147: a1 = h . t by A145, FUNCT_1:def 3;
consider x1, x2 being set , px being finite Subset of S such that
t = [x1,x2] and
A148: ( x1 in R1 & x2 in RA ) and
a1 = px and
A149: a1 is a_partition of x1 /\ x2 by A146, A147, A55, A56;
x1 /\ x2 c= x2 by XBOOLE_1:17;
then x1 /\ x2 c= A \ (qq . (j + 1)) by A45, A148, XBOOLE_1:1;
then A150: bool (x1 /\ x2) c= bool (A \ (qq . (j + 1))) by ZFMISC_1:67;
A151: a1 c= bool (A \ (qq . (j + 1))) by A149, A150, XBOOLE_1:1;
b = qq . (j + 1) by A140, TARSKI:def 1;
hence ( a = b or a misses b ) by A151, A144, XBOOLE_1:63, XBOOLE_1:79; :: thesis: verum
end;
hence ( a = b or a misses b ) by A121, XBOOLE_0:def 3, A141, A143; :: thesis: verum
end;
( not b in Union h or a = b or a misses b )
proof
assume A152: b in Union h ; :: thesis: ( a = b or a misses b )
A153: ( not a in rng (qq | (Seg j)) or a = b or a misses b )
proof
assume A154: a in rng (qq | (Seg j)) ; :: thesis: ( a = b or a misses b )
A155: b c= union (Union h) by A152, ZFMISC_1:74;
rng (qq | (Seg j)) c= rng (qq | (Seg (j + 1))) by A33, XBOOLE_1:7;
then a c= union (rng (qq | (Seg n))) by A154, A26, ZFMISC_1:74;
hence ( a = b or a misses b ) by A155, A68, XBOOLE_1:64; :: thesis: verum
end;
A156: ( not a in {(qq . (j + 1))} or a = b or a misses b )
proof
assume a in {(qq . (j + 1))} ; :: thesis: ( a = b or a misses b )
then A157: a = qq . (j + 1) by TARSKI:def 1;
consider b1 being set such that
A158: b in b1 and
A159: b1 in rng h by A152, TARSKI:def 4;
consider tb being object such that
A160: tb in dom h and
A161: b1 = h . tb by A159, FUNCT_1:def 3;
consider bx1, bx2 being set , bpx being finite Subset of S such that
tb = [bx1,bx2] and
A162: ( bx1 in R1 & bx2 in RA ) and
b1 = bpx and
A163: b1 is a_partition of bx1 /\ bx2 by A160, A161, A55, A56;
A164: bool (bx1 /\ bx2) c= bool bx2 by XBOOLE_1:17, ZFMISC_1:67;
b1 c= bool bx2 by A163, A164, XBOOLE_1:1;
then b c= A \ (qq . (j + 1)) by A45, A162, A158, XBOOLE_1:1;
hence ( a = b or a misses b ) by XBOOLE_1:79, A157, XBOOLE_1:63; :: thesis: verum
end;
( not a in Union h or a = b or a misses b )
proof
assume a in Union h ; :: thesis: ( a = b or a misses b )
then consider a1 being set such that
A166: a in a1 and
A167: a1 in rng h by TARSKI:def 4;
consider t being object such that
A168: t in dom h and
A169: a1 = h . t by A167, FUNCT_1:def 3;
consider x1, x2 being set , px being finite Subset of S such that
A170: t = [x1,x2] and
A171: ( x1 in R1 & x2 in RA ) and
a1 = px and
A172: a1 is a_partition of x1 /\ x2 by A168, A169, A55, A56;
consider b1 being set such that
A173: b in b1 and
A174: b1 in rng h by A152, TARSKI:def 4;
consider tb being object such that
A175: tb in dom h and
A176: b1 = h . tb by A174, FUNCT_1:def 3;
consider bx1, bx2 being set , bpx being finite Subset of S such that
A177: tb = [bx1,bx2] and
A178: ( bx1 in R1 & bx2 in RA ) and
b1 = bpx and
A179: b1 is a_partition of bx1 /\ bx2 by A175, A176, A55, A56;
A180: ( not x1 = bx1 & not x2 = bx2 & not a = b implies a misses b )
proof
assume A181: ( not x1 = bx1 & not x2 = bx2 ) ; :: thesis: ( a = b or a misses b )
A182: ( x1 in (rng (qq | (Seg j))) \/ R1 & bx1 in (rng (qq | (Seg j))) \/ R1 ) by A171, A178, XBOOLE_1:7, TARSKI:def 3;
A183: ( bool (x1 /\ x2) c= bool x1 & bool (bx1 /\ bx2) c= bool bx1 ) by XBOOLE_1:17, ZFMISC_1:67;
( a1 c= bool x1 & b1 c= bool bx1 ) by A172, A179, A183, XBOOLE_1:1;
hence ( a = b or a misses b ) by A182, A181, A30, EQREL_1:def 4, A166, A173, XBOOLE_1:64; :: thesis: verum
end;
A184: ( x1 = bx1 & not x2 = bx2 & not a = b implies a misses b )
proof
assume A185: ( x1 = bx1 & not x2 = bx2 ) ; :: thesis: ( a = b or a misses b )
A186: ( bool (x1 /\ x2) c= bool x2 & bool (bx1 /\ bx2) c= bool bx2 ) by XBOOLE_1:17, ZFMISC_1:67;
( a1 c= bool x2 & b1 c= bool bx2 ) by A172, A179, A186, XBOOLE_1:1;
hence ( a = b or a misses b ) by A166, A173, A185, A171, A178, A45, EQREL_1:def 4, XBOOLE_1:64; :: thesis: verum
end;
( not x1 = bx1 & x2 = bx2 & not a = b implies a misses b )
proof
assume A187: ( not x1 = bx1 & x2 = bx2 ) ; :: thesis: ( a = b or a misses b )
A188: ( x1 in (rng (qq | (Seg j))) \/ R1 & bx1 in (rng (qq | (Seg j))) \/ R1 ) by A171, A178, XBOOLE_1:7, TARSKI:def 3;
A189: ( bool (x1 /\ x2) c= bool x1 & bool (bx1 /\ bx2) c= bool bx1 ) by XBOOLE_1:17, ZFMISC_1:67;
( a1 c= bool x1 & b1 c= bool bx1 ) by A172, A179, A189, XBOOLE_1:1;
hence ( a = b or a misses b ) by A166, A173, XBOOLE_1:64, A188, A187, A30, EQREL_1:def 4; :: thesis: verum
end;
hence ( a = b or a misses b ) by A169, A176, A170, A177, A166, A173, A172, EQREL_1:def 4, A180, A184; :: thesis: verum
end;
hence ( a = b or a misses b ) by A121, XBOOLE_0:def 3, A153, A156; :: thesis: verum
end;
hence ( a = b or a misses b ) by A132, XBOOLE_0:def 3, A133, A139; :: thesis: verum
end;
hence ( a <> {} & ( for b being Subset of A holds
( not b in (rng (qq | (Seg n))) \/ (Union h) or a = b or a misses b ) ) ) by A122; :: thesis: verum
end;
hence (rng (qq | (Seg n))) \/ (Union h) is a_partition of A by A87, A98, EQREL_1:def 4; :: thesis: verum
end;
hence ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A ) by A65, A57, A68; :: thesis: verum
end;
end;
end;
suppose not j <= len qq ; :: thesis: ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A )
hence ex R being finite Subset of S st
( union R misses union (rng (qq | (Seg n))) & (rng (qq | (Seg n))) \/ R is a_partition of A ) by A28, A26, XREAL_1:39; :: thesis: verum
end;
end;
end;
hence S1[j + 1] ; :: thesis: verum
end;
A190: for i being Nat st 1 <= i holds
S1[i] from NAT_1:sch 8(A14, A23);
A191: ( len qq is Nat & 1 <= len qq ) by A13, FINSEQ_1:20;
consider R being finite Subset of S such that
A192: union R misses union (rng (qq | (Seg (len qq)))) and
A193: (rng (qq | (Seg (len qq)))) \/ R is a_partition of A by A190, A191;
rng (qq | (Seg (len qq))) = Q
proof
rng (qq | (Seg (len qq))) = rng (qq | (dom qq)) by FINSEQ_1:def 3
.= rng qq ;
hence rng (qq | (Seg (len qq))) = Q by A6; :: thesis: verum
end;
hence ex R being finite Subset of S st
( union R misses union Q & Q \/ R is a_partition of A ) by A193, A192; :: thesis: verum
end;
end;