:: ZFREFLE1 semantic presentation

REAL is set

bool REAL is non empty set

[:1,1:] is non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty set
bool [:[:1,1:],1:] is non empty set

bool NAT is non empty V41() set
bool NAT is non empty V41() set
VAR is non empty Element of bool NAT
bool VAR is non empty set

is non empty trivial 1 -element set

WFF is non empty set

x. 0 is Element of VAR
x. 1 is Element of VAR

x. 2 is Element of VAR

K209(((x. 2) 'in' ()),((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 2),K209(((x. 2) 'in' ()),((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

K208((All ((x. 2),K209(((x. 2) 'in' ()),((x. 2) 'in' (x. 1))))),(() '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((),(x. 1),K208((All ((x. 2),K209(((x. 2) 'in' ()),((x. 2) 'in' (x. 1))))),(() '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
is non empty V41() set
bool is non empty V41() set
bool WFF is non empty set

Free b is V41() Element of bool VAR
a is non empty set
a is non empty set
b is non empty set

Free M is V41() Element of bool VAR
b is non empty set
[:VAR,b:] is non empty set
bool [:VAR,b:] is non empty set
M is non empty set
[:VAR,M:] is non empty set
bool [:VAR,M:] is non empty set
a is non empty set

x. 3 is Element of VAR

K207(((x. 3) '=' ()),((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
K209(((x. 3) 'in' (x. 2)),K207(((x. 3) '=' ()),((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 3),K209(((x. 3) 'in' (x. 2)),K207(((x. 3) '=' ()),((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
Ex ((x. 2),(All ((x. 3),K209(((x. 3) 'in' (x. 2)),K207(((x. 3) '=' ()),((x. 3) '=' (x. 1))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((),(x. 1),(Ex ((x. 2),(All ((x. 3),K209(((x. 3) 'in' (x. 2)),K207(((x. 3) '=' ()),((x. 3) '=' (x. 1))))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

K204(((x. 2) 'in' (x. 3)),((x. 3) 'in' ())) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
Ex ((x. 3),K204(((x. 2) 'in' (x. 3)),((x. 3) 'in' ()))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
K209(((x. 2) 'in' (x. 1)),(Ex ((x. 3),K204(((x. 2) 'in' (x. 3)),((x. 3) 'in' ()))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 2),K209(((x. 2) 'in' (x. 1)),(Ex ((x. 3),K204(((x. 2) 'in' (x. 3)),((x. 3) 'in' ())))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
Ex ((x. 1),(All ((x. 2),K209(((x. 2) 'in' (x. 1)),(Ex ((x. 3),K204(((x. 2) 'in' (x. 3)),((x. 3) 'in' ())))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((),(Ex ((x. 1),(All ((x. 2),K209(((x. 2) 'in' (x. 1)),(Ex ((x. 3),K204(((x. 2) 'in' (x. 3)),((x. 3) 'in' ())))))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

K203(((x. 3) '=' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
K204(((x. 3) 'in' ()),K203(((x. 3) '=' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

x. 4 is Element of VAR

K208(((x. 4) 'in' (x. 2)),((x. 4) 'in' (x. 3))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 4),K208(((x. 4) 'in' (x. 2)),((x. 4) 'in' (x. 3)))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
K204(K204(((x. 3) 'in' ()),K203(((x. 3) '=' (x. 2)))),(All ((x. 4),K208(((x. 4) 'in' (x. 2)),((x. 4) 'in' (x. 3)))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
Ex ((x. 3),K204(K204(((x. 3) 'in' ()),K203(((x. 3) '=' (x. 2)))),(All ((x. 4),K208(((x. 4) 'in' (x. 2)),((x. 4) 'in' (x. 3))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
K208(((x. 2) 'in' ()),(Ex ((x. 3),K204(K204(((x. 3) 'in' ()),K203(((x. 3) '=' (x. 2)))),(All ((x. 4),K208(((x. 4) 'in' (x. 2)),((x. 4) 'in' (x. 3))))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 2),K208(((x. 2) 'in' ()),(Ex ((x. 3),K204(K204(((x. 3) 'in' ()),K203(((x. 3) '=' (x. 2)))),(All ((x. 4),K208(((x. 4) 'in' (x. 2)),((x. 4) 'in' (x. 3)))))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
K204(((x. 1) 'in' ()),(All ((x. 2),K208(((x. 2) 'in' ()),(Ex ((x. 3),K204(K204(((x. 3) 'in' ()),K203(((x. 3) '=' (x. 2)))),(All ((x. 4),K208(((x. 4) 'in' (x. 2)),((x. 4) 'in' (x. 3)))))))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
Ex ((),(x. 1),K204(((x. 1) 'in' ()),(All ((x. 2),K208(((x. 2) 'in' ()),(Ex ((x. 3),K204(K204(((x. 3) 'in' ()),K203(((x. 3) '=' (x. 2)))),(All ((x. 4),K208(((x. 4) 'in' (x. 2)),((x. 4) 'in' (x. 3))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

K208(((x. 3) 'in' (x. 2)),((x. 3) 'in' ())) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 3),K208(((x. 3) 'in' (x. 2)),((x. 3) 'in' ()))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
K209(((x. 2) 'in' (x. 1)),(All ((x. 3),K208(((x. 3) 'in' (x. 2)),((x. 3) 'in' ()))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 2),K209(((x. 2) 'in' (x. 1)),(All ((x. 3),K208(((x. 3) 'in' (x. 2)),((x. 3) 'in' ())))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
Ex ((x. 1),(All ((x. 2),K209(((x. 2) 'in' (x. 1)),(All ((x. 3),K208(((x. 3) 'in' (x. 2)),((x. 3) 'in' ())))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((),(Ex ((x. 1),(All ((x. 2),K209(((x. 2) 'in' (x. 1)),(All ((x. 3),K208(((x. 3) 'in' (x. 2)),((x. 3) 'in' ())))))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
{(),(x. 1),(x. 2)} is non empty set
X is set
W is set
() is set
X is set

X is non empty set

X is non empty set
W is Element of bool WFF
a is Element of bool WFF

X is non empty set
W is Element of bool WFF
a is Element of bool WFF
W \/ a is Element of bool WFF

() is Element of bool WFF
X is non empty set

Free a is V41() Element of bool VAR

K209(a,((x. 4) '=' ())) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 4),K209(a,((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),K209(a,((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),K209(a,((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

K204(((x. 3) 'in' (x. 1)),a) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
Ex ((x. 3),K204(((x. 3) 'in' (x. 1)),a)) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
K209(((x. 4) 'in' (x. 2)),(Ex ((x. 3),K204(((x. 3) 'in' (x. 1)),a)))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 4),K209(((x. 4) 'in' (x. 2)),(Ex ((x. 3),K204(((x. 3) 'in' (x. 1)),a))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
Ex ((x. 2),(All ((x. 4),K209(((x. 4) 'in' (x. 2)),(Ex ((x. 3),K204(((x. 3) 'in' (x. 1)),a))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 1),(Ex ((x. 2),(All ((x. 4),K209(((x. 4) 'in' (x. 2)),(Ex ((x. 3),K204(((x. 3) 'in' (x. 1)),a))))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
K208((All ((x. 3),(Ex ((),(All ((x. 4),K209(a,((x. 4) '=' ())))))))),(All ((x. 1),(Ex ((x. 2),(All ((x. 4),K209(((x. 4) 'in' (x. 2)),(Ex ((x. 3),K204(((x. 3) 'in' (x. 1)),a))))))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
X is non empty set

Free W is V41() Element of bool VAR

K209(W,((x. 4) '=' ())) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 4),K209(W,((x. 4) '=' ()))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
Ex ((),(All ((x. 4),K209(W,((x. 4) '=' ()))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 3),(Ex ((),(All ((x. 4),K209(W,((x. 4) '=' ()))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

K204(((x. 3) 'in' (x. 1)),W) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
Ex ((x. 3),K204(((x. 3) 'in' (x. 1)),W)) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
K209(((x. 4) 'in' (x. 2)),(Ex ((x. 3),K204(((x. 3) 'in' (x. 1)),W)))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 4),K209(((x. 4) 'in' (x. 2)),(Ex ((x. 3),K204(((x. 3) 'in' (x. 1)),W))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
Ex ((x. 2),(All ((x. 4),K209(((x. 4) 'in' (x. 2)),(Ex ((x. 3),K204(((x. 3) 'in' (x. 1)),W))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
All ((x. 1),(Ex ((x. 2),(All ((x. 4),K209(((x. 4) 'in' (x. 2)),(Ex ((x. 3),K204(((x. 3) 'in' (x. 1)),W))))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
K208((All ((x. 3),(Ex ((),(All ((x. 4),K209(W,((x. 4) '=' ())))))))),(All ((x. 1),(Ex ((x. 2),(All ((x. 4),K209(((x. 4) 'in' (x. 2)),(Ex ((x. 3),K204(((x. 3) 'in' (x. 1)),W))))))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

Free a is V41() Element of bool VAR

the Element of Free a is Element of Free a
M is Element of VAR
{M} is non empty trivial 1 -element set

Free (All (M,a)) is V41() Element of bool VAR
(Free a) \ {M} is Element of bool VAR
(Free (All (M,a))) \/ {M} is non empty set
(Free a) \/ {M} is non empty set
card (Free (All (M,a))) is epsilon-transitive epsilon-connected ordinal natural V34() V37() V38() V41() cardinal Element of NAT
(card (Free (All (M,a)))) + 1 is epsilon-transitive epsilon-connected ordinal natural V34() V37() V38() V41() cardinal Element of NAT

Free c6 is V41() Element of bool VAR
M is non empty set
Free X is V41() Element of bool VAR

Free W is V41() Element of bool VAR

a is non empty set
b is non empty set
X is non empty set
W is non empty set

Free b is V41() Element of bool VAR

Free a is V41() Element of bool VAR
X is non empty set
W is non empty set
a is Element of bool WFF

Free M is V41() Element of bool VAR

Free M is V41() Element of bool VAR

Free a is V41() Element of bool VAR

b is Element of bool WFF

b is Element of bool WFF

X is non empty set
W is non empty set
[:VAR,X:] is non empty set
bool [:VAR,X:] is non empty set

Free a is V41() Element of bool VAR

[:VAR,W:] is non empty set
bool [:VAR,W:] is non empty set

c6 is Element of VAR
M . c6 is Element of W
() . c6 is Element of W
[:VAR,W:] is non empty set
bool [:VAR,W:] is non empty set

X is non empty set
W is non empty set

dom X is set
rng X is set

X .: (dom X) is set

X is set

bool X is non empty set

W is set

bool W is non empty set

{0,1} is non empty set
Funcs (X,{0,1}) is non empty FUNCTION_DOMAIN of X,{0,1}

Funcs (W,{0,1}) is non empty FUNCTION_DOMAIN of W,{0,1}

Funcs ((On X),(On X)) is non empty FUNCTION_DOMAIN of On X, On X

[:(On X),(On X):] is non empty set
bool [:(On X),(On X):] is non empty set

W is non empty set
[:W,(Funcs ((On X),(On X))):] is non empty set
bool [:W,(Funcs ((On X),(On X))):] is non empty set

a is Relation-like W -defined Funcs ((On X),(On X)) -valued Function-like quasi_total Element of bool [:W,(Funcs ((On X),(On X))):]
uncurry a is Relation-like [:W,(On X):] -defined On X -valued Function-like quasi_total Element of bool [:[:W,(On X):],(On X):]
[:W,(On X):] is non empty set
[:[:W,(On X):],(On X):] is non empty set
bool [:[:W,(On X):],(On X):] is non empty set

{M} is non empty trivial 1 -element set
M \/ {M} is non empty set

{(succ M)} is non empty trivial 1 -element Element of X
[:W,{(succ M)}:] is non empty set

() .: [:W,{(succ M)}:] is set

rng a is set
rng () is set

{c6} is non empty trivial 1 -element Element of X
{c6} \/ (() .: [:W,{(succ M)}:]) is non empty set
sup ({c6} \/ (() .: [:W,{(succ M)}:])) is epsilon-transitive epsilon-connected ordinal set

rng b is set

rng (b | M) is set
c6 is set
M is set
(b | M) . M is set

rng b is set
M is set
c6 is set
b . c6 is set

{u} is non empty trivial 1 -element set
u \/ {u} is non empty set

{(M . u)} is non empty trivial 1 -element Element of X
{(succ u)} is non empty trivial 1 -element Element of X
[:W,{(succ u)}:] is non empty set
() .: [:W,{(succ u)}:] is set
{(M . u)} \/ (() .: [:W,{(succ u)}:]) is non empty set

sup ({(M . u)} \/ (() .: [:W,{(succ u)}:])) is epsilon-transitive epsilon-connected ordinal set

rng M is set

rng (M | u) is set

rng M is set

rng (M | c6) is set

{c6} is non empty trivial 1 -element set
c6 \/ {c6} is non empty set

{(M . c6)} is non empty trivial 1 -element Element of X
{(succ c6)} is non empty trivial 1 -element Element of X
[:W,{(succ c6)}:] is non empty set
() .: [:W,{(succ c6)}:] is set
{(M . c6)} \/ (() .: [:W,{(succ c6)}:]) is non empty set
sup ({(M . c6)} \/ (() .: [:W,{(succ c6)}:])) is epsilon-transitive epsilon-connected ordinal set

rng M is set

rng (M | c6) is set

rng (X +^ a) is set

rng a is set

(dom a) /\ W is set

dom ((X +^ a) | W) is epsilon-transitive epsilon-connected ordinal set
(dom (X +^ a)) /\ W is set
b is set
((X +^ a) | W) . b is set

X +^ ((a | W) . M) is epsilon-transitive epsilon-connected ordinal set
(X +^ (a | W)) . b is set
dom (X +^ (a | W)) is epsilon-transitive epsilon-connected ordinal set

rng (X +^ W) is set

rng W is set

dom (X +^ (W | a)) is epsilon-transitive epsilon-connected ordinal set
sup (X +^ (W | a)) is epsilon-transitive epsilon-connected ordinal set
rng (X +^ (W | a)) is set
sup (rng (X +^ (W | a))) is epsilon-transitive epsilon-connected ordinal set

rng (W | a) is set

X is set

rng W is set

rng X is set

rng a is set

rng W is set

{X} is non empty trivial 1 -element set
X \/ {X} is non empty set

{W} is non empty trivial 1 -element set
W \/ {W} is non empty set

rng a is set

{b} is non empty trivial 1 -element set
b \/ {b} is non empty set

M is set
a . M is set

rng a is set

[:(On X),(On X):] is non empty set
bool [:(On X),(On X):] is non empty set

{W} is non empty trivial 1 -element set
W \/ {W} is non empty set

(succ W) +^ (a . c6) is epsilon-transitive epsilon-connected ordinal Element of X

(succ W) +^ (a . c6) is epsilon-transitive epsilon-connected ordinal Element of X

[:(On X),(On X):] is non empty set
bool [:(On X),(On X):] is non empty set

rng b is set

rng (b | NAT) is set

rng a is set

(b | NAT) . (u +^ u) is epsilon-transitive epsilon-connected ordinal set

(b | NAT) . (u +^ u) is epsilon-transitive epsilon-connected ordinal set

{u} is non empty trivial 1 -element set
u \/ {u} is non empty set

(b | NAT) . (u +^ (succ u)) is epsilon-transitive epsilon-connected ordinal set

{a} is non empty trivial 1 -element set
a \/ {a} is non empty set

succ (a . (b . a)) is epsilon-transitive epsilon-connected ordinal non empty Element of X
{(a . (b . a))} is non empty trivial 1 -element set
(a . (b . a)) \/ {(a . (b . a))} is non empty set

rng (a | M) is set

u is set
(a | M) . u is set

A is set
(b | NAT) . A is set

{e} is non empty trivial 1 -element set
e \/ {e} is non empty set

succ (a . (b . e)) is epsilon-transitive epsilon-connected ordinal non empty Element of X
{(a . (b . e))} is non empty trivial 1 -element set
(a . (b . e)) \/ {(a . (b . e))} is non empty set
u is set
u is set
(b | NAT) . u is set

[:(On X),(On X):] is non empty set
bool [:(On X),(On X):] is non empty set

Union W is non empty Element of bool X
bool X is non empty set
Funcs ((On X),(On X)) is non empty FUNCTION_DOMAIN of On X, On X
b is set

M is set

rng c6 is set

W . u is non empty Element of X
[:VAR,(W . u):] is non empty set
bool [:VAR,(W . u):] is non empty set

[:VAR,():] is non empty set
bool [:VAR,():] is non empty set

dom b is set
rng b is set
[:WFF,(Funcs ((On X),(On X))):] is non empty set
bool [:WFF,(Funcs ((On X),(On X))):] is non empty set
is non empty V41() set
bool is non empty V41() set

M is Relation-like WFF -defined Funcs ((On X),(On X)) -valued Function-like quasi_total Element of bool [:WFF,(Funcs ((On X),(On X))):]

[:WFF,(On X):] is non empty set
[:[:WFF,(On X):],(On X):] is non empty set
bool [:[:WFF,(On X):],(On X):] is non empty set

W . M is non empty Element of X
[:VAR,(W . M):] is non empty set
bool [:VAR,(W . M):] is non empty set

[:VAR,():] is non empty set
bool [:VAR,():] is non empty set
M . u is set

rng xi is set

rng (xi | a) is set

e is set
(xi | a) . e is set

{e} is non empty trivial 1 -element set
e \/ {e} is non empty set

rng c6 is set
rng (c6 | a) is set

{a} is non empty trivial 1 -element set
a \/ {a} is non empty set

{(succ a)} is non empty trivial 1 -element Element of X
[u,(succ a)] is set
{u,(succ a)} is non empty set

{{u,(succ a)},{u}} is non empty set
[:WFF,{(succ a)}:] is non empty set

() . (u,(succ a)) is set
() . [u,(succ a)] is set

() .: [:WFF,{(succ a)}:] is set

{(c6 . a)} is non empty trivial 1 -element Element of X
{(c6 . a)} \/ (() .: [:WFF,{(succ a)}:]) is non empty set
sup ({(c6 . a)} \/ (() .: [:WFF,{(succ a)}:])) is epsilon-transitive epsilon-connected ordinal set

a is non empty set

[:(On X),(On X):] is non empty set
bool [:(On X),(On X):] is non empty set

W . {} is set

W . a is set

{a} is non empty trivial 1 -element set
a \/ {a} is non empty set
W . (succ a) is set

W . a is set

{b} is non empty trivial 1 -element set
b \/ {b} is non empty set

{M} is non empty trivial 1 -element set
M \/ {M} is non empty set
W . (succ M) is set

{b} is non empty trivial 1 -element set
b \/ {b} is non empty set
rng W is set
a is set
b is set
W . b is set

rng a is set
b is set
a . b is set

a . M is set

Union b is non empty Element of bool X
bool X is non empty set
M is set
rng b is V72() set
union (rng b) is set

b . M is non empty Element of X

b . M is non empty Element of X

b . c6 is non empty Element of X

{M} is non empty trivial 1 -element set
M \/ {M} is non empty set

{()} is non empty trivial 1 -element set
() \/ {()} is non empty set

b . M is non empty Element of X

rng b is V72() set
Union (b | M) is set

c6 is set

{u} is non empty trivial 1 -element set
u \/ {u} is non empty set
rng (b | M) is set
union (rng (b | M)) is set
b . (succ u) is non empty Element of X

c6 is set
rng (b | M) is set
union (rng (b | M)) is set
M is set

u is set
(b | M) . u is set

b . u is set

b . u is non empty Element of X

M is non empty set
b . c6 is non empty Element of X

[:(On X),(On X):] is non empty set
bool [:(On X),(On X):] is non empty set

M is non empty set

[:(On X),(On X):] is non empty set
bool [:(On X),(On X):] is non empty set

M is non empty set

[:(On X),(On X):] is non empty set
bool [:(On X),(On X):] is non empty set

Union W is non empty Element of bool X
bool X is non empty set

W . b is non empty Element of X

[:(On X),(On X):] is non empty set
bool [:(On X),(On X):] is non empty set

b is non empty set

b is non empty set

a is non empty set

a is non empty set

X is set

M is non empty set

{a} is non empty trivial 1 -element set
a \/ {a} is non empty set