let e be object ; ( 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))
then reconsider fs = e as XFinSequence of bool (the_universe_of (X \/ NAT)) 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 A12, A10;
( 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 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
Nat st
p >= 1 &
p <= (dom fs) - 1 holds
fs1 . p = [:(fs . p),(fs . ((dom fs) - p)):] ) &
F . e = Union (disjoin fs1) )
by A20, A12, A10;
reconsider n9 =
(dom fs) -' 1 as
Nat ;
(dom fs) - 1
>= 2
- 1
by A20, XREAL_1:9;
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 (X \/ NAT)
proof
let p be
Nat;
( 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:1;
(
- p <= - 1 &
- p >= - ((dom fs) - 1) )
by A24, XREAL_1:24;
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 A27, XREAL_0:def 2;
then A30:
(dom fs) -' p in Seg n9
by A28, FINSEQ_1:1;
A31:
Seg n9 c= Segm (n9 + 1)
by AFINSQ_1:3;
then A32:
fs . p in rng fs
by A26, A22, FUNCT_1:3;
fs . ((dom fs) - p) in rng fs
by A29, A31, A22, A30, FUNCT_1:3;
hence
fs1 . p c= the_universe_of (X \/ NAT)
by A25, A32, 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
object such that A33:
(
p in dom (disjoin fs1) &
x = (disjoin fs1) . p )
by FUNCT_1:def 3;
A34:
p in dom fs1
by A33, CARD_3:def 3;
then A35:
x = [:(fs1 . p),{p}:]
by A33, CARD_3:def 3;
A36:
p in Seg n9
by A21, A22, A34, FINSEQ_1:def 3;
reconsider p =
p as
Nat by A34;
(
p >= 1 &
p <= (dom fs) - 1 )
by A22, A36, FINSEQ_1:1;
then A37:
fs1 . p c= the_universe_of (X \/ NAT)
by A23;
A38:
for
y being
set st
y in {p} holds
y in NAT
for
x being
object 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))
;
then
{p} c= the_universe_of (X \/ NAT)
by YELLOW_6:def 1;
hence
x c= the_universe_of (X \/ NAT)
by A35, A37, Th1;
verum
end; then
union (rng (disjoin fs1)) c= the_universe_of (X \/ NAT)
by ZFMISC_1:76;
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;