let e be object ; :: thesis: ( 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 ; :: thesis: 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;

assume A12: e in (bool (the_universe_of (X \/ NAT))) ^omega ; :: thesis: 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;

end;

suppose A15:
dom fs = 0
; :: thesis: F . e in bool (the_universe_of (X \/ NAT))

{} c= the_universe_of (X \/ NAT)
;

hence F . e in bool (the_universe_of (X \/ NAT)) by A15, A13; :: thesis: verum

end;hence F . e in bool (the_universe_of (X \/ NAT)) by A15, A13; :: thesis: verum

suppose
dom fs = 1
; :: thesis: F . e in bool (the_universe_of (X \/ NAT))

then A16:
F . e = X
by A12, A10;

for x being object st x in X holds

x in Tarski-Class (the_transitive-closure_of (X \/ NAT))

then X c= the_universe_of (X \/ NAT) by YELLOW_6:def 1;

hence F . e in bool (the_universe_of (X \/ NAT)) by A16; :: thesis: verum

end;for x being object st x in X holds

x in Tarski-Class (the_transitive-closure_of (X \/ NAT))

proof

then
X c= Tarski-Class (the_transitive-closure_of (X \/ NAT))
;
let x be object ; :: thesis: ( x in X implies x in Tarski-Class (the_transitive-closure_of (X \/ NAT)) )

reconsider xx = x as set by TARSKI:1;

assume x in X ; :: thesis: x in Tarski-Class (the_transitive-closure_of (X \/ NAT))

then xx c= (union X) \/ (union NAT) by XBOOLE_1:10, ZFMISC_1:74;

then A17: xx c= union (X \/ NAT) by ZFMISC_1:78;

A18: the_transitive-closure_of (X \/ NAT) in Tarski-Class (the_transitive-closure_of (X \/ NAT)) by CLASSES1:2;

A19: union (X \/ NAT) c= union (the_transitive-closure_of (X \/ NAT)) by CLASSES1:52, ZFMISC_1:77;

union (the_transitive-closure_of (X \/ NAT)) c= the_transitive-closure_of (X \/ NAT) by CLASSES1:48, CLASSES1:51;

then union (X \/ NAT) c= the_transitive-closure_of (X \/ NAT) by A19;

hence x in Tarski-Class (the_transitive-closure_of (X \/ NAT)) by A18, A17, CLASSES1:3, XBOOLE_1:1; :: thesis: verum

end;reconsider xx = x as set by TARSKI:1;

assume x in X ; :: thesis: x in Tarski-Class (the_transitive-closure_of (X \/ NAT))

then xx c= (union X) \/ (union NAT) by XBOOLE_1:10, ZFMISC_1:74;

then A17: xx c= union (X \/ NAT) by ZFMISC_1:78;

A18: the_transitive-closure_of (X \/ NAT) in Tarski-Class (the_transitive-closure_of (X \/ NAT)) by CLASSES1:2;

A19: union (X \/ NAT) c= union (the_transitive-closure_of (X \/ NAT)) by CLASSES1:52, ZFMISC_1:77;

union (the_transitive-closure_of (X \/ NAT)) c= the_transitive-closure_of (X \/ NAT) by CLASSES1:48, CLASSES1:51;

then union (X \/ NAT) c= the_transitive-closure_of (X \/ NAT) by A19;

hence x in Tarski-Class (the_transitive-closure_of (X \/ NAT)) by A18, A17, CLASSES1:3, XBOOLE_1:1; :: thesis: verum

then X c= the_universe_of (X \/ NAT) by YELLOW_6:def 1;

hence F . e in bool (the_universe_of (X \/ NAT)) by A16; :: thesis: verum

suppose A20:
dom fs >= 2
; :: thesis: 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)

x c= the_universe_of (X \/ NAT)

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; :: thesis: verum

end;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

for x being set st x in rng (disjoin fs1) holds
let p be Nat; :: thesis: ( p >= 1 & p <= (dom fs) - 1 implies fs1 . p c= the_universe_of (X \/ NAT) )

assume A24: ( p >= 1 & p <= (dom fs) - 1 ) ; :: thesis: 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; :: thesis: verum

end;assume A24: ( p >= 1 & p <= (dom fs) - 1 ) ; :: thesis: 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; :: thesis: verum

x c= the_universe_of (X \/ NAT)

proof

then
union (rng (disjoin fs1)) c= the_universe_of (X \/ NAT)
by ZFMISC_1:76;
let x be set ; :: thesis: ( x in rng (disjoin fs1) implies x c= the_universe_of (X \/ NAT) )

assume x in rng (disjoin fs1) ; :: thesis: 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

x in 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; :: thesis: verum

end;assume x in rng (disjoin fs1) ; :: thesis: 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

proof

for x being object st x in {p} holds
let y be set ; :: thesis: ( y in {p} implies y in NAT )

assume y in {p} ; :: thesis: y in NAT

then y = p by TARSKI:def 1;

hence y in NAT by ORDINAL1:def 12; :: thesis: verum

end;assume y in {p} ; :: thesis: y in NAT

then y = p by TARSKI:def 1;

hence y in NAT by ORDINAL1:def 12; :: thesis: verum

x in Tarski-Class (the_transitive-closure_of (X \/ NAT))

proof

then
{p} c= Tarski-Class (the_transitive-closure_of (X \/ NAT))
;
let x be object ; :: thesis: ( x in {p} implies x in Tarski-Class (the_transitive-closure_of (X \/ NAT)) )

reconsider xx = x as set by TARSKI:1;

assume x in {p} ; :: thesis: x in Tarski-Class (the_transitive-closure_of (X \/ NAT))

then x in NAT by A38;

then xx c= (union X) \/ (union NAT) by XBOOLE_1:10, ZFMISC_1:74;

then A39: xx c= union (X \/ NAT) by ZFMISC_1:78;

A40: the_transitive-closure_of (X \/ NAT) in Tarski-Class (the_transitive-closure_of (X \/ NAT)) by CLASSES1:2;

A41: union (X \/ NAT) c= union (the_transitive-closure_of (X \/ NAT)) by CLASSES1:52, ZFMISC_1:77;

union (the_transitive-closure_of (X \/ NAT)) c= the_transitive-closure_of (X \/ NAT) by CLASSES1:48, CLASSES1:51;

then union (X \/ NAT) c= the_transitive-closure_of (X \/ NAT) by A41;

hence x in Tarski-Class (the_transitive-closure_of (X \/ NAT)) by A40, A39, CLASSES1:3, XBOOLE_1:1; :: thesis: verum

end;reconsider xx = x as set by TARSKI:1;

assume x in {p} ; :: thesis: x in Tarski-Class (the_transitive-closure_of (X \/ NAT))

then x in NAT by A38;

then xx c= (union X) \/ (union NAT) by XBOOLE_1:10, ZFMISC_1:74;

then A39: xx c= union (X \/ NAT) by ZFMISC_1:78;

A40: the_transitive-closure_of (X \/ NAT) in Tarski-Class (the_transitive-closure_of (X \/ NAT)) by CLASSES1:2;

A41: union (X \/ NAT) c= union (the_transitive-closure_of (X \/ NAT)) by CLASSES1:52, ZFMISC_1:77;

union (the_transitive-closure_of (X \/ NAT)) c= the_transitive-closure_of (X \/ NAT) by CLASSES1:48, CLASSES1:51;

then union (X \/ NAT) c= the_transitive-closure_of (X \/ NAT) by A41;

hence x in Tarski-Class (the_transitive-closure_of (X \/ NAT)) by A40, A39, CLASSES1:3, XBOOLE_1:1; :: thesis: verum

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; :: thesis: verum

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; :: thesis: verum