let X be set ; :: thesis: for S being cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X
for SM being Function of NATPLUS,S ex P being countable Subset of S st
( P is a_partition of Union SM & ( for n being NatPlus holds Union (SM | (Seg n)) = union { s where s is Element of S : ( s in P & s c= Union (SM | (Seg n)) ) } ) )
let S be cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X; :: thesis: for SM being Function of NATPLUS,S ex P being countable Subset of S st
( P is a_partition of Union SM & ( for n being NatPlus holds Union (SM | (Seg n)) = union { s where s is Element of S : ( s in P & s c= Union (SM | (Seg n)) ) } ) )
let SM be Function of NATPLUS,S; :: thesis: ex P being countable Subset of S st
( P is a_partition of Union SM & ( for n being NatPlus holds Union (SM | (Seg n)) = union { s where s is Element of S : ( s in P & s c= Union (SM | (Seg n)) ) } ) )
per cases ( S = {} or not S = {} ) ;
suppose A1: S = {} ; :: thesis: ex P being countable Subset of S st
( P is a_partition of Union SM & ( for n being NatPlus holds Union (SM | (Seg n)) = union { s where s is Element of S : ( s in P & s c= Union (SM | (Seg n)) ) } ) )
then A2: Union SM = {} by ZFMISC_1:2;
set P = {} ;
A3: ( {} is finite Subset of S & {} is a_partition of {} ) by SUBSET_1:1, EQREL_1:45;
for n being NatPlus holds Union (SM | (Seg n)) = union { s where s is Element of S : ( s in {} & s c= Union (SM | (Seg n)) ) }
proof
let n be NatPlus; :: thesis: Union (SM | (Seg n)) = union { s where s is Element of S : ( s in {} & s c= Union (SM | (Seg n)) ) }
thus Union (SM | (Seg n)) c= union { s where s is Element of S : ( s in {} & s c= Union (SM | (Seg n)) ) } :: according to XBOOLE_0:def 10 :: thesis: union { s where s is Element of S : ( s in {} & s c= Union (SM | (Seg n)) ) } c= Union (SM | (Seg n))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union (SM | (Seg n)) or x in union { s where s is Element of S : ( s in {} & s c= Union (SM | (Seg n)) ) } )
assume x in Union (SM | (Seg n)) ; :: thesis: x in union { s where s is Element of S : ( s in {} & s c= Union (SM | (Seg n)) ) }
hence x in union { s where s is Element of S : ( s in {} & s c= Union (SM | (Seg n)) ) } by A1, ZFMISC_1:2; :: thesis: verum
end;
thus union { s where s is Element of S : ( s in {} & s c= Union (SM | (Seg n)) ) } c= Union (SM | (Seg n)) :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { s where s is Element of S : ( s in {} & s c= Union (SM | (Seg n)) ) } or x in Union (SM | (Seg n)) )
assume x in union { s where s is Element of S : ( s in {} & s c= Union (SM | (Seg n)) ) } ; :: thesis: x in Union (SM | (Seg n))
then consider y being set such that
A5: x in y and
A6: y in { s where s is Element of S : ( s in {} & s c= Union (SM | (Seg n)) ) } by TARSKI:def 4;
consider s0 being Element of S such that
A7: y = s0 and
s0 in {} and
A8: s0 c= Union (SM | (Seg n)) by A6;
thus x in Union (SM | (Seg n)) by A5, A7, A8; :: thesis: verum
end;
end;
hence ex P being countable Subset of S st
( P is a_partition of Union SM & ( for n being NatPlus holds Union (SM | (Seg n)) = union { s where s is Element of S : ( s in P & s c= Union (SM | (Seg n)) ) } ) ) by A2, A3; :: thesis: verum
end;
suppose A9: not S = {} ; :: thesis: ex P being countable Subset of S st
( P is a_partition of Union SM & ( for n being NatPlus holds Union (SM | (Seg n)) = union { s where s is Element of S : ( s in P & s c= Union (SM | (Seg n)) ) } ) )
then A10: dom SM = NATPLUS by FUNCT_2:def 1;
A11: for x being NatPlus ex x1 being Nat st
( x1 = x - 1 & ex Px being finite Subset of S st Px is a_partition of (SM . x) \ (Union (SM | (Seg x1))) )
proof
let x be NatPlus; :: thesis: ex x1 being Nat st
( x1 = x - 1 & ex Px being finite Subset of S st Px is a_partition of (SM . x) \ (Union (SM | (Seg x1))) )
set x1 = x - 1;
reconsider x1 = x - 1 as Nat by CHORD:1;
rng (SM | (Seg x1)) is finite Subset of S ;
then ex P being finite Subset of S st P is a_partition of (SM . x) \ (Union (SM | (Seg x1))) by Thm1;
hence ex x1 being Nat st
( x1 = x - 1 & ex Px being finite Subset of S st Px is a_partition of (SM . x) \ (Union (SM | (Seg x1))) ) ; :: thesis: verum
end;
defpred S1[ object , object ] means ex x, xp being Nat st
( $1 = x & xp = x - 1 & $2 is finite Subset of S & $2 is a_partition of (SM . x) \ (Union (SM | (Seg xp))) );
A12: for n being object st n in NATPLUS holds
ex y being object st
( y in bool S & S1[n,y] )
proof
let n be object ; :: thesis: ( n in NATPLUS implies ex y being object st
( y in bool S & S1[n,y] ) )
assume n in NATPLUS ; :: thesis: ex y being object st
( y in bool S & S1[n,y] )
then consider n1 being NatPlus such that
A13: n = n1 ;
reconsider n = n as NatPlus by A13;
consider x1 being Nat such that
A14: ( x1 = n - 1 & ex Px being finite Subset of S st Px is a_partition of (SM . n) \ (Union (SM | (Seg x1))) ) by A11;
thus ex y being object st
( y in bool S & S1[n,y] ) by A14; :: thesis: verum
end;
consider fi being Function such that
A15: ( dom fi = NATPLUS & rng fi c= bool S ) and
A16: for n being object st n in NATPLUS holds
S1[n,fi . n] from FUNCT_1:sch 6(A12);
A17: ( Union fi is countable Subset of S & Union fi is a_partition of Union SM )
proof
A18: Union fi is countable Subset of S
proof
A19: Union fi is countable
proof
for v being set st v in dom fi holds
fi . v is countable
proof
let v be set ; :: thesis: ( v in dom fi implies fi . v is countable )
assume v in dom fi ; :: thesis: fi . v is countable
then S1[v,fi . v] by A15, A16;
hence fi . v is countable ; :: thesis: verum
end;
hence Union fi is countable by A15, CARD_4:11; :: thesis: verum
end;
Union fi c= S
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Union fi or u in S )
assume u in Union fi ; :: thesis: u in S
then ex v being set st
( u in v & v in rng fi ) by TARSKI:def 4;
hence u in S by A15; :: thesis: verum
end;
hence Union fi is countable Subset of S by A19; :: thesis: verum
end;
A21: Union fi is a_partition of Union SM
proof
A22: Union fi c= bool (Union SM)
proof
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in Union fi or w in bool (Union SM) )
assume w in Union fi ; :: thesis: w in bool (Union SM)
then consider w0 being set such that
A23: ( w in w0 & w0 in rng fi ) by TARSKI:def 4;
consider v0 being object such that
A24: ( v0 in dom fi & w0 = fi . v0 ) by A23, FUNCT_1:def 3;
reconsider w = w as set by TARSKI:1;
w c= union (rng SM)
proof
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in w or v in union (rng SM) )
assume A25: v in w ; :: thesis: v in union (rng SM)
consider mx, mxp being Nat such that
A26: ( v0 = mx & mxp = mx - 1 & fi . v0 is finite Subset of S & fi . v0 is a_partition of (SM . mx) \ (Union (SM | (Seg mxp))) ) by A15, A16, A24;
A27: v in (SM . mx) \ (Union (SM | (Seg mxp))) by A23, A24, A25, A26;
mx in dom SM by A9, A15, A24, A26, FUNCT_2:def 1;
then SM . mx in rng SM by FUNCT_1:def 3;
hence v in union (rng SM) by A27, TARSKI:def 4; :: thesis: verum
end;
hence w in bool (Union SM) ; :: thesis: verum
end;
A28: union (Union fi) = Union SM
proof
thus union (Union fi) c= Union SM :: according to XBOOLE_0:def 10 :: thesis: Union SM c= union (Union fi) let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in Union SM or v in union (Union fi) )
assume v in Union SM ; :: thesis: v in union (Union fi)
then consider v0 being set such that
A30: ( v in v0 & v0 in rng SM ) by TARSKI:def 4;
consider v1 being object such that
A31: ( v1 in dom SM & v0 = SM . v1 ) by A30, FUNCT_1:def 3;
reconsider v1 = v1 as NatPlus by A31;
consider n0 being NatPlus, np being Nat such that
A32: ( n0 <= v1 & np = n0 - 1 & v in (SM . n0) \ (Union (SM | (Seg np))) ) by A30, A31, Lem11;
S1[n0,fi . n0] by A16;
then consider x, xp being Nat such that
A33: ( n0 = x & xp = x - 1 & fi . n0 is finite Subset of S & fi . n0 is a_partition of (SM . n0) \ (Union (SM | (Seg xp))) ) ;
A34: union (fi . n0) = (SM . n0) \ (Union (SM | (Seg xp))) by A33, EQREL_1:def 4;
fi . n0 c= Union fi
proof
fi . n0 in rng fi by A15, FUNCT_1:def 3;
hence fi . n0 c= Union fi by ZFMISC_1:74; :: thesis: verum
end;
then union (fi . n0) c= union (Union fi) by ZFMISC_1:77;
hence v in union (Union fi) by A32, A33, A34; :: thesis: verum
end;
for A being Subset of (Union SM) st A in Union fi holds
( A <> {} & ( for B being Subset of (Union SM) holds
( not B in Union fi or A = B or A misses B ) ) )
proof
let A be Subset of (Union SM); :: thesis: ( A in Union fi implies ( A <> {} & ( for B being Subset of (Union SM) holds
( not B in Union fi or A = B or A misses B ) ) ) )
assume A in Union fi ; :: thesis: ( A <> {} & ( for B being Subset of (Union SM) holds
( not B in Union fi or A = B or A misses B ) ) )
then consider a0 being set such that
A35: ( A in a0 & a0 in rng fi ) by TARSKI:def 4;
consider a1 being object such that
A36: ( a1 in dom fi & a0 = fi . a1 ) by A35, FUNCT_1:def 3;
S1[a1,fi . a1] by A15, A16, A36;
then consider xa, xap being Nat such that
A37: ( a1 = xa & xap = xa - 1 & fi . a1 is finite Subset of S & fi . a1 is a_partition of (SM . a1) \ (Union (SM | (Seg xap))) ) ;
for B being Subset of (Union SM) holds
( not B in Union fi or A = B or A misses B )
proof
let B be Subset of (Union SM); :: thesis: ( not B in Union fi or A = B or A misses B )
assume B in Union fi ; :: thesis: ( A = B or A misses B )
then consider b0 being set such that
A38: ( B in b0 & b0 in rng fi ) by TARSKI:def 4;
consider b1 being object such that
A39: ( b1 in dom fi & b0 = fi . b1 ) by A38, FUNCT_1:def 3;
S1[b1,fi . b1] by A15, A16, A39;
then consider xb, xbp being Nat such that
A40: ( b1 = xb & xbp = xb - 1 & fi . b1 is finite Subset of S & fi . b1 is a_partition of (SM . b1) \ (Union (SM | (Seg xbp))) ) ;
( a1 = b1 or A = B or A misses B )
proof
assume A41: not a1 = b1 ; :: thesis: ( A = B or A misses B )
reconsider a1 = a1 as NatPlus by A15, A36;
reconsider b1 = b1 as NatPlus by A15, A39;
(SM . a1) \ (Union (SM | (Seg xap))) misses (SM . b1) \ (Union (SM | (Seg xbp)))
proof
A42: ( a1 < b1 implies (SM . a1) \ (Union (SM | (Seg xap))) misses (SM . b1) \ (Union (SM | (Seg xbp))) )
proof
assume A43: a1 < b1 ; :: thesis: (SM . a1) \ (Union (SM | (Seg xap))) misses (SM . b1) \ (Union (SM | (Seg xbp)))
assume not (SM . a1) \ (Union (SM | (Seg xap))) misses (SM . b1) \ (Union (SM | (Seg xbp))) ; :: thesis: contradiction
then consider u being object such that
A44: u in ((SM . a1) \ (Union (SM | (Seg xap)))) /\ ((SM . b1) \ (Union (SM | (Seg xbp)))) by XBOOLE_0:def 1;
A45: ( u in (SM . a1) \ (Union (SM | (Seg xap))) & u in (SM . b1) \ (Union (SM | (Seg xbp))) ) by A44, XBOOLE_0:def 4;
( u in SM . a1 implies u in Union (SM | (Seg xbp)) )
proof
assume A46: u in SM . a1 ; :: thesis: u in Union (SM | (Seg xbp))
A47: 1 <= a1 by CHORD:1;
xa < xbp + 1 by A37, A40, A43;
then xa <= xbp by NAT_1:13;
then A48: xa in Seg xbp by A37, A47;
A49: a1 in dom (SM | (Seg xbp)) by A10, A37, A48, RELAT_1:57;
then (SM | (Seg xbp)) . a1 in rng (SM | (Seg xbp)) by FUNCT_1:def 3;
then SM . a1 in rng (SM | (Seg xbp)) by A49, FUNCT_1:47;
then SM . a1 c= Union (SM | (Seg xbp)) by ZFMISC_1:74;
hence u in Union (SM | (Seg xbp)) by A46; :: thesis: verum
end;
hence contradiction by A45, XBOOLE_0:def 5; :: thesis: verum
end;
( b1 < a1 implies (SM . a1) \ (Union (SM | (Seg xap))) misses (SM . b1) \ (Union (SM | (Seg xbp))) )
proof
assume A50: b1 < a1 ; :: thesis: (SM . a1) \ (Union (SM | (Seg xap))) misses (SM . b1) \ (Union (SM | (Seg xbp)))
assume A51: not (SM . a1) \ (Union (SM | (Seg xap))) misses (SM . b1) \ (Union (SM | (Seg xbp))) ; :: thesis: contradiction
A52: not ((SM . a1) \ (Union (SM | (Seg xap)))) /\ ((SM . b1) \ (Union (SM | (Seg xbp)))) is empty by A51;
consider u being object such that
A53: u in ((SM . a1) \ (Union (SM | (Seg xap)))) /\ ((SM . b1) \ (Union (SM | (Seg xbp)))) by A52;
A54: ( u in (SM . a1) \ (Union (SM | (Seg xap))) & u in (SM . b1) \ (Union (SM | (Seg xbp))) ) by A53, XBOOLE_0:def 4;
( u in SM . b1 implies u in Union (SM | (Seg xap)) )
proof
assume A55: u in SM . b1 ; :: thesis: u in Union (SM | (Seg xap))
A56: 1 <= b1 by CHORD:1;
xb < xap + 1 by A37, A40, A50;
then xb <= xap by NAT_1:13;
then A57: b1 in Seg xap by A40, A56;
A58: b1 in dom (SM | (Seg xap)) by A10, A57, RELAT_1:57;
then (SM | (Seg xap)) . b1 in rng (SM | (Seg xap)) by FUNCT_1:def 3;
then SM . b1 in rng (SM | (Seg xap)) by A58, FUNCT_1:47;
then SM . b1 c= Union (SM | (Seg xap)) by ZFMISC_1:74;
hence u in Union (SM | (Seg xap)) by A55; :: thesis: verum
end;
hence contradiction by A54, XBOOLE_0:def 5; :: thesis: verum
end;
hence (SM . a1) \ (Union (SM | (Seg xap))) misses (SM . b1) \ (Union (SM | (Seg xbp))) by A41, A42, XXREAL_0:1; :: thesis: verum
end;
hence ( A = B or A misses B ) by A35, A36, A37, A38, A39, A40, XBOOLE_1:64; :: thesis: verum
end;
hence ( A = B or A misses B ) by A35, A36, A37, A38, A39, EQREL_1:def 4; :: thesis: verum
end;
hence ( A <> {} & ( for B being Subset of (Union SM) holds
( not B in Union fi or A = B or A misses B ) ) ) by A35, A36, A37; :: thesis: verum
end;
hence Union fi is a_partition of Union SM by A22, A28, EQREL_1:def 4; :: thesis: verum
end;
thus ( Union fi is countable Subset of S & Union fi is a_partition of Union SM ) by A18, A21; :: thesis: verum
end;
A59: for l being Nat holds { s where s is Element of S : ( s in Union fi & s c= Union (SM | (Seg l)) ) } = (Union fi) /\ (bool (Union (SM | (Seg l))))
proof
let l be Nat; :: thesis: { s where s is Element of S : ( s in Union fi & s c= Union (SM | (Seg l)) ) } = (Union fi) /\ (bool (Union (SM | (Seg l))))
A60: { s where s is Element of S : ( s in Union fi & s c= Union (SM | (Seg l)) ) } c= (Union fi) /\ (bool (Union (SM | (Seg l))))
proof
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in { s where s is Element of S : ( s in Union fi & s c= Union (SM | (Seg l)) ) } or v in (Union fi) /\ (bool (Union (SM | (Seg l)))) )
assume v in { s where s is Element of S : ( s in Union fi & s c= Union (SM | (Seg l)) ) } ; :: thesis: v in (Union fi) /\ (bool (Union (SM | (Seg l))))
then consider s0 being Element of S such that
A61: ( v = s0 & s0 in Union fi & s0 c= Union (SM | (Seg l)) ) ;
thus v in (Union fi) /\ (bool (Union (SM | (Seg l)))) by A61, XBOOLE_0:def 4; :: thesis: verum
end;
(Union fi) /\ (bool (Union (SM | (Seg l)))) c= { s where s is Element of S : ( s in Union fi & s c= Union (SM | (Seg l)) ) }
proof
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in (Union fi) /\ (bool (Union (SM | (Seg l)))) or v in { s where s is Element of S : ( s in Union fi & s c= Union (SM | (Seg l)) ) } )
assume A62: v in (Union fi) /\ (bool (Union (SM | (Seg l)))) ; :: thesis: v in { s where s is Element of S : ( s in Union fi & s c= Union (SM | (Seg l)) ) }
then ( v in Union fi & v in bool (Union (SM | (Seg l))) ) by XBOOLE_0:def 4;
then consider v0 being set such that
A63: ( v in v0 & v0 in rng fi ) by TARSKI:def 4;
consider n0 being object such that
A64: ( n0 in dom fi & v0 = fi . n0 ) by A63, FUNCT_1:def 3;
S1[n0,fi . n0] by A15, A16, A64;
then consider x, xp being Nat such that
A65: ( n0 = x & xp = x - 1 & fi . n0 is finite Subset of S & fi . n0 is a_partition of (SM . n0) \ (Union (SM | (Seg xp))) ) ;
( v in S & v in Union fi & v in bool (Union (SM | (Seg l))) ) by A62, A63, A64, A65, XBOOLE_0:def 4;
hence v in { s where s is Element of S : ( s in Union fi & s c= Union (SM | (Seg l)) ) } ; :: thesis: verum
end;
hence { s where s is Element of S : ( s in Union fi & s c= Union (SM | (Seg l)) ) } = (Union fi) /\ (bool (Union (SM | (Seg l)))) by A60; :: thesis: verum
end;
for n being NatPlus holds Union (SM | (Seg n)) = union { s where s is Element of S : ( s in Union fi & s c= Union (SM | (Seg n)) ) }
proof
let n be NatPlus; :: thesis: Union (SM | (Seg n)) = union { s where s is Element of S : ( s in Union fi & s c= Union (SM | (Seg n)) ) }
A66: Union (SM | (Seg n)) c= Union SM by ZFMISC_1:77, RELAT_1:70;
Union (SM | (Seg n)) = union ((Union fi) /\ (bool (Union (SM | (Seg n)))))
proof
A67: Union (SM | (Seg n)) c= union ((Union fi) /\ (bool (Union (SM | (Seg n)))))
proof
let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in Union (SM | (Seg n)) or v in union ((Union fi) /\ (bool (Union (SM | (Seg n))))) )
assume A68: v in Union (SM | (Seg n)) ; :: thesis: v in union ((Union fi) /\ (bool (Union (SM | (Seg n)))))
then v in Union SM by A66;
then v in union (Union fi) by A17, EQREL_1:def 4;
then consider v0 being set such that
A69: ( v in v0 & v0 in Union fi ) by TARSKI:def 4;
v0 c= Union (SM | (Seg n))
proof
consider v1 being set such that
A70: ( v0 in v1 & v1 in rng fi ) by A69, TARSKI:def 4;
consider v2 being object such that
A71: ( v2 in dom fi & v1 = fi . v2 ) by A70, FUNCT_1:def 3;
S1[v2,fi . v2] by A15, A16, A71;
then consider x2, x2p being Nat such that
A72: ( v2 = x2 & x2p = x2 - 1 & fi . v2 is finite Subset of S & fi . v2 is a_partition of (SM . v2) \ (Union (SM | (Seg x2p))) ) ;
( not v in Union (SM | (Seg x2p)) & v in Union (SM | (Seg n)) ) by A68, A69, A70, A71, A72, XBOOLE_0:def 5;
then A73: v in (Union (SM | (Seg n))) \ (Union (SM | (Seg x2p))) by XBOOLE_0:def 5;
A74: for n1, n2 being Nat st n1 <= n2 holds
Union (SM | (Seg n1)) c= Union (SM | (Seg n2))
proof
let n1, n2 be Nat; :: thesis: ( n1 <= n2 implies Union (SM | (Seg n1)) c= Union (SM | (Seg n2)) )
assume n1 <= n2 ; :: thesis: Union (SM | (Seg n1)) c= Union (SM | (Seg n2))
then SM | (Seg n1) c= SM | (Seg n2) by FINSEQ_1:5, RELAT_1:75;
hence Union (SM | (Seg n1)) c= Union (SM | (Seg n2)) by RELAT_1:11, ZFMISC_1:77; :: thesis: verum
end;
A75: for n1, n2 being Nat st n1 <= n2 holds
(Union (SM | (Seg n1))) \ (Union (SM | (Seg n2))) = {}
proof
let n1, n2 be Nat; :: thesis: ( n1 <= n2 implies (Union (SM | (Seg n1))) \ (Union (SM | (Seg n2))) = {} )
assume n1 <= n2 ; :: thesis: (Union (SM | (Seg n1))) \ (Union (SM | (Seg n2))) = {}
then A76: SM | (Seg n1) c= SM | (Seg n2) by FINSEQ_1:5, RELAT_1:75;
Union (SM | (Seg n1)) c= Union (SM | (Seg n2)) by A76, RELAT_1:11, ZFMISC_1:77;
hence (Union (SM | (Seg n1))) \ (Union (SM | (Seg n2))) = {} by XBOOLE_1:37; :: thesis: verum
end;
(x2 - 1) + 1 <= n + 1 by XREAL_1:6, A72, A73, A75;
then A77: ( x2 <= n or x2 = n + 1 ) by NAT_1:8;
reconsider v2 = v2 as Nat by A72;
A78: v0 c= SM . v2 by A70, A71, A72, XBOOLE_1:1;
for x being set
for i, j being Nat st x c= SM . i & i <= j holds
x c= Union (SM | (Seg j))
proof
let x be set ; :: thesis: for i, j being Nat st x c= SM . i & i <= j holds
x c= Union (SM | (Seg j))
let i, j be Nat; :: thesis: ( x c= SM . i & i <= j implies x c= Union (SM | (Seg j)) )
assume A79: x c= SM . i ; :: thesis: ( not i <= j or x c= Union (SM | (Seg j)) )
assume A80: i <= j ; :: thesis: x c= Union (SM | (Seg j))
A81: SM . i c= Union (SM | (Seg i))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in SM . i or y in Union (SM | (Seg i)) )
assume A82: y in SM . i ; :: thesis: y in Union (SM | (Seg i))
per cases ( i is zero or not i is zero ) ;
suppose not i is zero ; :: thesis: y in Union (SM | (Seg i))
then A83: ( 1 <= i & i <= i ) by CHORD:1;
Seg i c= dom SM
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in Seg i or o in dom SM )
assume A84: o in Seg i ; :: thesis: o in dom SM
then reconsider o = o as Nat ;
not o is zero by A84, FINSEQ_1:1;
hence o in dom SM by A10, NAT_LAT:def 6; :: thesis: verum
end;
then A85: dom (SM | (Seg i)) = Seg i by RELAT_1:62;
A86: SM . i = (SM | (Seg i)) . i by A83, A85, FINSEQ_1:1, FUNCT_1:47;
(SM | (Seg i)) . i in rng (SM | (Seg i)) by A83, A85, FINSEQ_1:1, FUNCT_1:3;
then SM . i c= Union (SM | (Seg i)) by A86, ZFMISC_1:74;
hence y in Union (SM | (Seg i)) by A82; :: thesis: verum
end;
end;
end;
Union (SM | (Seg i)) c= Union (SM | (Seg j)) by A74, A80;
then SM . i c= Union (SM | (Seg j)) by A81, XBOOLE_1:1;
hence x c= Union (SM | (Seg j)) by A79, XBOOLE_1:1; :: thesis: verum
end;
hence v0 c= Union (SM | (Seg n)) by A77, A72, A68, A69, A70, A71, A78, XBOOLE_0:def 5; :: thesis: verum
end;
then ( v in v0 & v0 in (Union fi) /\ (bool (Union (SM | (Seg n)))) ) by A69, XBOOLE_0:def 4;
hence v in union ((Union fi) /\ (bool (Union (SM | (Seg n))))) by TARSKI:def 4; :: thesis: verum
end;
union ((Union fi) /\ (bool (Union (SM | (Seg n))))) c= Union (SM | (Seg n))
proof
A87: (union (Union fi)) /\ (union (bool (Union (SM | (Seg n))))) = (union (Union fi)) /\ (Union (SM | (Seg n))) by ZFMISC_1:81;
union (Union fi) = Union SM by A17, EQREL_1:def 4;
then union ((Union fi) /\ (bool (Union (SM | (Seg n))))) c= (Union SM) /\ (Union (SM | (Seg n))) by A87, ZFMISC_1:79;
hence union ((Union fi) /\ (bool (Union (SM | (Seg n))))) c= Union (SM | (Seg n)) by A66, XBOOLE_1:28; :: thesis: verum
end;
hence Union (SM | (Seg n)) = union ((Union fi) /\ (bool (Union (SM | (Seg n))))) by A67; :: thesis: verum
end;
hence Union (SM | (Seg n)) = union { s where s is Element of S : ( s in Union fi & s c= Union (SM | (Seg n)) ) } by A59; :: thesis: verum
end;
hence ex P being countable Subset of S st
( P is a_partition of Union SM & ( for n being NatPlus holds Union (SM | (Seg n)) = union { s where s is Element of S : ( s in P & s c= Union (SM | (Seg n)) ) } ) ) by A17; :: thesis: verum
end;
end;