let e be object ; :: thesis: ( e in (bool (the_universe_of ())) ^omega implies F . e in bool (the_universe_of ()) )
assume A12: e in (bool (the_universe_of ())) ^omega ; :: thesis: F . e in bool (the_universe_of ())
then reconsider fs = e as XFinSequence of bool (the_universe_of ()) by AFINSQ_1:def 7;
A13: ( ( dom fs = 0 implies F . e = {} ) & ( dom fs = 1 implies F . e = X ) & ( for n being Nat st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being Nat st p >= 1 & p <= n - 1 holds
fs1 . p = [:(fs . p),(fs . (n - p)):] ) & F . e = Union (disjoin fs1) ) ) ) by ;
( dom fs = 0 or (dom fs) + 1 > 0 + 1 ) by XREAL_1:6;
then ( dom fs = 0 or dom fs >= 1 ) by NAT_1:13;
then ( dom fs = 0 or dom fs = 1 or dom fs > 1 ) by XXREAL_0:1;
then A14: ( dom fs = 0 or dom fs = 1 or (dom fs) + 1 > 1 + 1 ) by XREAL_1:6;
per cases ( dom fs = 0 or dom fs = 1 or dom fs >= 2 ) by ;
suppose A15: dom fs = 0 ; :: thesis: F . e in bool (the_universe_of ())
end;
suppose dom fs = 1 ; :: thesis: F . e in bool (the_universe_of ())
end;
suppose A20: dom fs >= 2 ; :: thesis: F . e in bool (the_universe_of ())
set n = dom fs;
consider fs1 being FinSequence such that
A21: ( len fs1 = (dom fs) - 1 & ( for p being Nat st p >= 1 & p <= (dom fs) - 1 holds
fs1 . p = [:(fs . p),(fs . ((dom fs) - p)):] ) & F . e = Union (disjoin fs1) ) by ;
reconsider n9 = (dom fs) -' 1 as Nat ;
(dom fs) - 1 >= 2 - 1 by ;
then A22: n9 = (dom fs) - 1 by XREAL_0:def 2;
A23: for p being Nat st p >= 1 & p <= (dom fs) - 1 holds
fs1 . p c= the_universe_of ()
proof
let p be Nat; :: thesis: ( p >= 1 & p <= (dom fs) - 1 implies fs1 . p c= the_universe_of () )
assume A24: ( p >= 1 & p <= (dom fs) - 1 ) ; :: thesis: fs1 . p c= the_universe_of ()
then A25: fs1 . p = [:(fs . p),(fs . ((dom fs) - p)):] by A21;
A26: p in Seg n9 by ;
( - p <= - 1 & - p >= - ((dom fs) - 1) ) by ;
then A27: ( (- p) + (dom fs) <= (- 1) + (dom fs) & (- p) + (dom fs) >= (- ((dom fs) - 1)) + (dom fs) ) by XREAL_1:6;
then A28: ( (dom fs) - p <= (dom fs) -' 1 & (dom fs) - p >= 1 ) by XREAL_0:def 2;
A29: (dom fs) - p = (dom fs) -' p by ;
then A30: (dom fs) -' p in Seg n9 by ;
A31: Seg n9 c= Segm (n9 + 1) by AFINSQ_1:3;
then A32: fs . p in rng fs by ;
fs . ((dom fs) - p) in rng fs by ;
hence fs1 . p c= the_universe_of () by ; :: thesis: verum
end;
for x being set st x in rng (disjoin fs1) holds
x c= the_universe_of ()
proof
let x be set ; :: thesis: ( x in rng (disjoin fs1) implies x c= the_universe_of () )
assume x in rng (disjoin fs1) ; :: thesis: x c= the_universe_of ()
then consider p being object such that
A33: ( p in dom (disjoin fs1) & x = (disjoin fs1) . p ) by FUNCT_1:def 3;
A34: p in dom fs1 by ;
then A35: x = [:(fs1 . p),{p}:] by ;
A36: p in Seg n9 by ;
reconsider p = p as Nat by A34;
( p >= 1 & p <= (dom fs) - 1 ) by ;
then A37: fs1 . p c= the_universe_of () by A23;
A38: for y being set st y in {p} holds
y in NAT
proof
let y be set ; :: thesis: ( y in {p} implies y in NAT )
assume y in {p} ; :: thesis:
then y = p by TARSKI:def 1;
hence y in NAT by ORDINAL1:def 12; :: thesis: verum
end;
for x being object st x in {p} holds
x in Tarski-Class () then {p} c= Tarski-Class () ;
then {p} c= the_universe_of () by YELLOW_6:def 1;
hence x c= the_universe_of () by ; :: thesis: verum
end;
then union (rng (disjoin fs1)) c= the_universe_of () by ZFMISC_1:76;
then union (rng (disjoin fs1)) in bool (the_universe_of ()) ;
hence F . e in bool (the_universe_of ()) by ; :: thesis: verum
end;
end;