let e be set ; ( e in (bool (the_universe_of (X \/ NAT ))) ^omega implies F . e in bool (the_universe_of (X \/ NAT )) )
assume A12:
e in (bool (the_universe_of (X \/ NAT ))) ^omega
; F . e in bool (the_universe_of (X \/ NAT ))
reconsider fs = e as XFinSequence of bool (the_universe_of (X \/ NAT )) by A12, AFINSQ_1:def 8;
A13:
( ( dom fs = 0 implies F . e = {} ) & ( dom fs = 1 implies F . e = X ) & ( for n being natural number st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs1 . p = [:(fs . p),(fs . (n - p)):] ) & F . e = Union (disjoin fs1) ) ) )
by A12, A11;
( dom fs = 0 or (dom fs) + 1 > 0 + 1 )
by XREAL_1:8;
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:8;
per cases
( dom fs = 0 or dom fs = 1 or dom fs >= 2 )
by A14, NAT_1:13;
suppose A20:
dom fs >= 2
;
F . e in bool (the_universe_of (X \/ NAT ))set n =
dom fs;
consider fs1 being
FinSequence such that A21:
(
len fs1 = (dom fs) - 1 & ( for
p being
natural number st
p >= 1 &
p <= (dom fs) - 1 holds
fs1 . p = [:(fs . p),(fs . ((dom fs) - p)):] ) &
F . e = Union (disjoin fs1) )
by A20, A12, A11;
reconsider n9 =
(dom fs) -' 1 as
Nat ;
(dom fs) - 1
>= 2
- 1
by A20, XREAL_1:11;
then A22:
n9 = (dom fs) - 1
by XREAL_0:def 2;
A23:
for
p being
natural number st
p >= 1 &
p <= (dom fs) - 1 holds
fs1 . p c= the_universe_of (X \/ NAT )
proof
let p be
natural number ;
( p >= 1 & p <= (dom fs) - 1 implies fs1 . p c= the_universe_of (X \/ NAT ) )
assume A24:
(
p >= 1 &
p <= (dom fs) - 1 )
;
fs1 . p c= the_universe_of (X \/ NAT )
then A25:
fs1 . p = [:(fs . p),(fs . ((dom fs) - p)):]
by A21;
A26:
p in Seg n9
by A22, A24, FINSEQ_1:3;
(
- p <= - 1 &
- p >= - ((dom fs) - 1) )
by A24, XREAL_1:26;
then A27:
(
(- p) + (dom fs) <= (- 1) + (dom fs) &
(- p) + (dom fs) >= (- ((dom fs) - 1)) + (dom fs) )
by XREAL_1:8;
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 A27, XREAL_0:def 2;
then A30:
(dom fs) -' p in Seg n9
by A28, FINSEQ_1:3;
A31:
rng fs c= bool (the_universe_of (X \/ NAT ))
by RELAT_1:def 19;
A32:
Seg n9 c= n9 + 1
by AFINSQ_1:5;
then A33:
fs . p in rng fs
by A26, A22, FUNCT_1:12;
fs . ((dom fs) - p) in rng fs
by A29, A32, A22, A30, FUNCT_1:12;
hence
fs1 . p c= the_universe_of (X \/ NAT )
by A31, A25, A33, Th1;
verum
end;
for
x being
set st
x in rng (disjoin fs1) holds
x c= the_universe_of (X \/ NAT )
proof
let x be
set ;
( x in rng (disjoin fs1) implies x c= the_universe_of (X \/ NAT ) )
assume
x in rng (disjoin fs1)
;
x c= the_universe_of (X \/ NAT )
then consider p being
set such that A34:
(
p in dom (disjoin fs1) &
x = (disjoin fs1) . p )
by FUNCT_1:def 5;
A35:
p in dom fs1
by A34, CARD_3:def 3;
A36:
x = [:(fs1 . p),{p}:]
by A34, A35, CARD_3:def 3;
A37:
p in Seg n9
by A21, A22, A35, FINSEQ_1:def 3;
reconsider p =
p as
natural number by A35;
(
p >= 1 &
p <= (dom fs) - 1 )
by A22, A37, FINSEQ_1:3;
then A38:
fs1 . p c= the_universe_of (X \/ NAT )
by A23;
A39:
for
y being
set st
y in {p} holds
y in NAT
for
x being
set st
x in {p} holds
x in Tarski-Class (the_transitive-closure_of (X \/ NAT ))
then
{p} c= Tarski-Class (the_transitive-closure_of (X \/ NAT ))
by TARSKI:def 3;
then
{p} c= the_universe_of (X \/ NAT )
by YELLOW_6:def 3;
hence
x c= the_universe_of (X \/ NAT )
by A36, A38, Th1;
verum
end; then
union (rng (disjoin fs1)) c= the_universe_of (X \/ NAT )
by ZFMISC_1:94;
then
union (rng (disjoin fs1)) in bool (the_universe_of (X \/ NAT ))
;
hence
F . e in bool (the_universe_of (X \/ NAT ))
by A21, CARD_3:def 4;
verum end;