:: ZFREFLE1 semantic presentation

REAL is set

NAT is epsilon-transitive epsilon-connected ordinal non empty V41() cardinal limit_cardinal Element of bool REAL

bool REAL is non empty set

1 is epsilon-transitive epsilon-connected ordinal natural non empty V34() V37() V38() V41() cardinal Element of NAT

[: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

NAT is epsilon-transitive epsilon-connected ordinal non empty V41() cardinal limit_cardinal 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 epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V34() V37() V38() V41() cardinal {} -element set

the epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V34() V37() V38() V41() cardinal {} -element set is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V34() V37() V38() V41() cardinal {} -element set

0 is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V34() V37() V38() V41() cardinal {} -element Element of NAT

{{}} is non empty trivial 1 -element set

card {} is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V34() V37() V38() V41() cardinal {} -element set

Rank {} is epsilon-transitive set

WFF is non empty set

the_axiom_of_extensionality is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

x. 0 is Element of VAR

x. 1 is Element of VAR

2 is epsilon-transitive epsilon-connected ordinal natural non empty V34() V37() V38() V41() cardinal Element of NAT

x. 2 is Element of VAR

(x. 2) 'in' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

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

K209(((x. 2) 'in' (x. 0)),((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. 0)),((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

(x. 0) '=' (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. 0)),((x. 2) 'in' (x. 1))))),((x. 0) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

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

[:NAT,NAT:] is non empty V41() set

bool [:NAT,NAT:] is non empty V41() set

bool WFF is non empty set

b is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

Free b is V41() Element of bool VAR

a is non empty set

a is non empty set

b is non empty set

M is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

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

c

M is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

b ! c

u is Relation-like VAR -defined M -valued Function-like quasi_total Element of bool [:VAR,M:]

M ! u is Relation-like VAR -defined M -valued Function-like quasi_total Element of bool [:VAR,M:]

u is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

the_axiom_of_pairs is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

3 is epsilon-transitive epsilon-connected ordinal natural non empty V34() V37() V38() V41() cardinal Element of NAT

x. 3 is Element of VAR

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

(x. 3) '=' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

(x. 3) '=' (x. 1) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

K207(((x. 3) '=' (x. 0)),((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. 0)),((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. 0)),((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. 0)),((x. 3) '=' (x. 1))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

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

the_axiom_of_unions is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

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

(x. 3) 'in' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

K204(((x. 2) 'in' (x. 3)),((x. 3) 'in' (x. 0))) 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' (x. 0)))) 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' (x. 0)))))) 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' (x. 0))))))) 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' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

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

the_axiom_of_infinity is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

(x. 1) 'in' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

(x. 3) '=' (x. 2) 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' (x. 0)),K203(((x. 3) '=' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

4 is epsilon-transitive epsilon-connected ordinal natural non empty V34() V37() V38() V41() cardinal Element of NAT

x. 4 is Element of VAR

(x. 4) 'in' (x. 2) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

(x. 4) 'in' (x. 3) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

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' (x. 0)),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' (x. 0)),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' (x. 0)),(Ex ((x. 3),K204(K204(((x. 3) 'in' (x. 0)),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' (x. 0)),(Ex ((x. 3),K204(K204(((x. 3) 'in' (x. 0)),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' (x. 0)),(All ((x. 2),K208(((x. 2) 'in' (x. 0)),(Ex ((x. 3),K204(K204(((x. 3) 'in' (x. 0)),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. 0),(x. 1),K204(((x. 1) 'in' (x. 0)),(All ((x. 2),K208(((x. 2) 'in' (x. 0)),(Ex ((x. 3),K204(K204(((x. 3) 'in' (x. 0)),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 )

the_axiom_of_power_sets is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

K208(((x. 3) 'in' (x. 2)),((x. 3) 'in' (x. 0))) 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' (x. 0)))) 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' (x. 0)))))) 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' (x. 0))))))) 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' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

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

{(x. 0),(x. 1),(x. 2)} is non empty set

X is set

W is set

() is set

X is set

{} WFF is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty proper V34() V37() V38() V41() cardinal {} -element Element of bool WFF

X is non empty set

W is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

X is non empty set

W is Element of bool WFF

a is Element of bool WFF

b is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

X is non empty set

W is Element of bool WFF

a is Element of bool WFF

W \/ a is Element of bool WFF

b is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

() is Element of bool WFF

X is non empty set

W is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

a is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

Free a is V41() Element of bool VAR

the_axiom_of_substitution_for a is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

(x. 4) '=' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

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

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

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

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

(x. 3) 'in' (x. 1) 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 ((x. 0),(All ((x. 4),K209(a,((x. 4) '=' (x. 0))))))))),(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

W is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

Free W is V41() Element of bool VAR

the_axiom_of_substitution_for W is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

(x. 4) '=' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

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

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

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

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

(x. 3) 'in' (x. 1) 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 ((x. 0),(All ((x. 4),K209(W,((x. 4) '=' (x. 0))))))))),(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 )

X is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

W is epsilon-transitive epsilon-connected ordinal natural V34() V37() V38() V41() cardinal Element of NAT

W + 1 is epsilon-transitive epsilon-connected ordinal natural V34() V37() V38() V41() cardinal Element of NAT

a is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

Free a is V41() Element of bool VAR

card (Free a) is epsilon-transitive epsilon-connected ordinal natural V34() V37() V38() V41() cardinal Element of NAT

the Element of Free a is Element of Free a

M is Element of VAR

{M} is non empty trivial 1 -element set

All (M,a) is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

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

c

Free c

M is non empty set

Free X is V41() Element of bool VAR

card (Free X) is epsilon-transitive epsilon-connected ordinal natural V34() V37() V38() V41() cardinal Element of NAT

W is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

Free W is V41() Element of bool VAR

card (Free W) is epsilon-transitive epsilon-connected ordinal natural V34() V37() V38() V41() cardinal Element of NAT

a is non empty set

b is non empty set

X is non empty set

W is non empty set

a is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

b is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

Free b is V41() Element of bool VAR

a is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

Free a is V41() Element of bool VAR

X is non empty set

W is non empty set

a is Element of bool WFF

b is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

M is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

Free M is V41() Element of bool VAR

b is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

M is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

Free M is V41() Element of bool VAR

a is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

Free a is V41() Element of bool VAR

{a} is functional non empty trivial 1 -element set

b is Element of bool WFF

M is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

b is Element of bool WFF

M is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

X is non empty set

W is non empty set

[:VAR,X:] is non empty set

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

a is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

Free a is V41() Element of bool VAR

the Relation-like VAR -defined X -valued Function-like quasi_total Element of bool [:VAR,X:] is Relation-like VAR -defined X -valued Function-like quasi_total Element of bool [:VAR,X:]

W ! the Relation-like VAR -defined X -valued Function-like quasi_total Element of bool [:VAR,X:] is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]

[:VAR,W:] is non empty set

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

M is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]

c

M . c

(W ! the Relation-like VAR -defined X -valued Function-like quasi_total Element of bool [:VAR,X:]) . c

[:VAR,W:] is non empty set

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

b is Relation-like VAR -defined X -valued Function-like quasi_total Element of bool [:VAR,X:]

W ! b is Relation-like VAR -defined W -valued Function-like quasi_total Element of bool [:VAR,W:]

X is non empty set

W is non empty set

X is Relation-like Function-like set

dom X is set

rng X is set

W is epsilon-transitive non empty subset-closed Tarski universal set

X .: (dom X) is set

card (dom X) is epsilon-transitive epsilon-connected ordinal cardinal set

card W is epsilon-transitive epsilon-connected ordinal non empty cardinal set

card (rng X) is epsilon-transitive epsilon-connected ordinal cardinal set

X is set

card X is epsilon-transitive epsilon-connected ordinal cardinal set

bool X is non empty set

card (bool X) is epsilon-transitive epsilon-connected ordinal non empty cardinal set

W is set

card W is epsilon-transitive epsilon-connected ordinal cardinal set

bool W is non empty set

card (bool W) is epsilon-transitive epsilon-connected ordinal non empty cardinal set

{0,1} is non empty set

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

card (Funcs (X,{0,1})) is epsilon-transitive epsilon-connected ordinal non empty cardinal set

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

card (Funcs (W,{0,1})) is epsilon-transitive epsilon-connected ordinal non empty cardinal set

X is epsilon-transitive non empty subset-closed Tarski universal set

On X is epsilon-transitive epsilon-connected ordinal non empty set

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

card X is epsilon-transitive epsilon-connected ordinal non empty cardinal set

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

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

0-element_of X is epsilon-transitive epsilon-connected ordinal Element of X

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

card W is epsilon-transitive epsilon-connected ordinal non empty cardinal 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

b is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom b is epsilon-transitive epsilon-connected ordinal set

b . {} is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal Element of X

b . M is epsilon-transitive epsilon-connected ordinal set

succ M is epsilon-transitive epsilon-connected ordinal non empty Element of X

{M} is non empty trivial 1 -element set

M \/ {M} is non empty set

b . (succ M) is epsilon-transitive epsilon-connected ordinal set

{(succ M)} is non empty trivial 1 -element Element of X

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

card [:W,{(succ M)}:] is epsilon-transitive epsilon-connected ordinal non empty cardinal set

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

card ((uncurry a) .: [:W,{(succ M)}:]) is epsilon-transitive epsilon-connected ordinal cardinal set

rng a is set

rng (uncurry a) is set

c

{c

{c

sup ({c

M is epsilon-transitive epsilon-connected ordinal Element of X

b . M is epsilon-transitive epsilon-connected ordinal set

b | M is Relation-like rng b -valued T-Sequence-like Function-like Ordinal-yielding set

rng b is set

dom (b | M) is epsilon-transitive epsilon-connected ordinal set

rng (b | M) is set

c

M is set

(b | M) . M is set

u is epsilon-transitive epsilon-connected ordinal set

u is epsilon-transitive epsilon-connected ordinal Element of X

b . u is epsilon-transitive epsilon-connected ordinal set

sup (b | M) is epsilon-transitive epsilon-connected ordinal set

sup (rng (b | M)) is epsilon-transitive epsilon-connected ordinal set

b . (0-element_of X) is epsilon-transitive epsilon-connected ordinal set

rng b is set

M is set

c

b . c

M is epsilon-transitive epsilon-connected ordinal Element of X

b . M is epsilon-transitive epsilon-connected ordinal set

M is Relation-like On X -defined On X -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of bool [:(On X),(On X):]

M . (0-element_of X) is epsilon-transitive epsilon-connected ordinal Element of X

c

dom M is epsilon-transitive epsilon-connected ordinal set

M . c

M is epsilon-transitive epsilon-connected ordinal set

M . M is epsilon-transitive epsilon-connected ordinal set

u is epsilon-transitive epsilon-connected ordinal Element of X

M . u is epsilon-transitive epsilon-connected ordinal Element of X

u is epsilon-transitive epsilon-connected ordinal Element of X

M . u is epsilon-transitive epsilon-connected ordinal set

succ u is epsilon-transitive epsilon-connected ordinal non empty Element of X

{u} is non empty trivial 1 -element set

u \/ {u} is non empty set

M . (succ u) is epsilon-transitive epsilon-connected ordinal set

M . u is epsilon-transitive epsilon-connected ordinal Element of X

{(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

(uncurry a) .: [:W,{(succ u)}:] is set

{(M . u)} \/ ((uncurry a) .: [:W,{(succ u)}:]) is non empty set

M . (succ u) is epsilon-transitive epsilon-connected ordinal Element of X

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

u is epsilon-transitive epsilon-connected ordinal Element of X

M . u is epsilon-transitive epsilon-connected ordinal set

M . u is epsilon-transitive epsilon-connected ordinal Element of X

M | u is Relation-like rng M -valued T-Sequence-like Function-like Ordinal-yielding set

rng M is set

sup (M | u) is epsilon-transitive epsilon-connected ordinal set

rng (M | u) is set

sup (rng (M | u)) is epsilon-transitive epsilon-connected ordinal set

M . (0-element_of X) is epsilon-transitive epsilon-connected ordinal set

u is epsilon-transitive epsilon-connected ordinal Element of X

M . u is epsilon-transitive epsilon-connected ordinal Element of X

c

dom M is epsilon-transitive epsilon-connected ordinal set

M . c

M | c

rng M is set

M is epsilon-transitive epsilon-connected ordinal set

dom (M | c

sup (M | c

rng (M | c

sup (rng (M | c

c

succ c

{c

c

M . (succ c

M . c

{(M . c

{(succ c

[:W,{(succ c

(uncurry a) .: [:W,{(succ c

{(M . c

sup ({(M . c

c

M . c

M | c

rng M is set

sup (M | c

rng (M | c

sup (rng (M | c

X is epsilon-transitive epsilon-connected ordinal set

W is Relation-like T-Sequence-like Function-like Ordinal-yielding set

X +^ W is Relation-like T-Sequence-like Function-like Ordinal-yielding set

a is epsilon-transitive epsilon-connected ordinal set

dom (X +^ W) is epsilon-transitive epsilon-connected ordinal set

(X +^ W) . a is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

(X +^ W) . b is epsilon-transitive epsilon-connected ordinal set

W . a is epsilon-transitive epsilon-connected ordinal set

W . b is epsilon-transitive epsilon-connected ordinal set

dom W is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal set

X +^ M is epsilon-transitive epsilon-connected ordinal set

c

X +^ c

X is epsilon-transitive epsilon-connected ordinal set

W is epsilon-transitive epsilon-connected ordinal set

a is Relation-like T-Sequence-like Function-like Ordinal-yielding set

X +^ a is Relation-like T-Sequence-like Function-like Ordinal-yielding set

(X +^ a) | W is Relation-like rng (X +^ a) -valued T-Sequence-like Function-like Ordinal-yielding set

rng (X +^ a) is set

a | W is Relation-like rng a -valued T-Sequence-like Function-like Ordinal-yielding set

rng a is set

X +^ (a | W) is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom (a | W) is epsilon-transitive epsilon-connected ordinal set

dom a is epsilon-transitive epsilon-connected ordinal set

(dom a) /\ W is set

dom (X +^ a) is epsilon-transitive epsilon-connected ordinal 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

M is epsilon-transitive epsilon-connected ordinal set

(X +^ a) . M is epsilon-transitive epsilon-connected ordinal set

a . M is epsilon-transitive epsilon-connected ordinal set

X +^ (a . M) is epsilon-transitive epsilon-connected ordinal set

(a | W) . M is epsilon-transitive epsilon-connected ordinal 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

X is epsilon-transitive epsilon-connected ordinal set

W is Relation-like T-Sequence-like Function-like Ordinal-yielding set

X +^ W is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom W is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

dom (X +^ W) is epsilon-transitive epsilon-connected ordinal set

(X +^ W) . a is epsilon-transitive epsilon-connected ordinal set

(X +^ W) | a is Relation-like rng (X +^ W) -valued T-Sequence-like Function-like Ordinal-yielding set

rng (X +^ W) is set

b is epsilon-transitive epsilon-connected ordinal set

W | a is Relation-like rng W -valued T-Sequence-like Function-like Ordinal-yielding set

rng W is set

W . a is epsilon-transitive epsilon-connected ordinal set

c

X +^ c

lim (W | a) is epsilon-transitive epsilon-connected ordinal set

dom (W | a) is epsilon-transitive epsilon-connected ordinal set

X +^ (W | a) is Relation-like T-Sequence-like Function-like Ordinal-yielding 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

sup (W | a) is epsilon-transitive epsilon-connected ordinal set

rng (W | a) is set

sup (rng (W | a)) is epsilon-transitive epsilon-connected ordinal set

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

X is set

W is Relation-like T-Sequence-like Function-like Ordinal-yielding set

rng W is set

X is Relation-like T-Sequence-like Function-like Ordinal-yielding set

rng X is set

sup X is epsilon-transitive epsilon-connected ordinal set

sup (rng X) is epsilon-transitive epsilon-connected ordinal set

X is epsilon-transitive epsilon-connected ordinal set

W is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

X is epsilon-transitive epsilon-connected ordinal set

W is epsilon-transitive epsilon-connected ordinal set

a is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

rng a is set

sup a is epsilon-transitive epsilon-connected ordinal set

sup (rng a) is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

a . b is epsilon-transitive epsilon-connected ordinal set

X is epsilon-transitive epsilon-connected ordinal set

W is epsilon-transitive epsilon-connected ordinal set

X is epsilon-transitive epsilon-connected ordinal set

W is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom W is epsilon-transitive epsilon-connected ordinal set

rng W is set

sup W is epsilon-transitive epsilon-connected ordinal set

sup (rng W) is epsilon-transitive epsilon-connected ordinal set

lim W is epsilon-transitive epsilon-connected ordinal set

X is epsilon-transitive epsilon-connected ordinal set

succ X is epsilon-transitive epsilon-connected ordinal non empty set

{X} is non empty trivial 1 -element set

X \/ {X} is non empty set

X is epsilon-transitive epsilon-connected ordinal set

W is epsilon-transitive epsilon-connected ordinal set

succ W is epsilon-transitive epsilon-connected ordinal non empty set

{W} is non empty trivial 1 -element set

W \/ {W} is non empty set

a is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

rng a is set

sup a is epsilon-transitive epsilon-connected ordinal set

sup (rng a) is epsilon-transitive epsilon-connected ordinal set

a . W is epsilon-transitive epsilon-connected ordinal set

b is epsilon-transitive epsilon-connected ordinal set

succ b is epsilon-transitive epsilon-connected ordinal non empty set

{b} is non empty trivial 1 -element set

b \/ {b} is non empty set

M is epsilon-transitive epsilon-connected ordinal set

c

M is set

a . M is set

u is epsilon-transitive epsilon-connected ordinal set

X is epsilon-transitive epsilon-connected ordinal set

W is epsilon-transitive epsilon-connected ordinal set

X is epsilon-transitive epsilon-connected ordinal set

X is epsilon-transitive non empty subset-closed Tarski universal set

On X is epsilon-transitive epsilon-connected ordinal non empty set

W is epsilon-transitive epsilon-connected ordinal Element of X

a is Relation-like T-Sequence-like Function-like Ordinal-yielding set

dom a is epsilon-transitive epsilon-connected ordinal set

rng a is set

sup a is epsilon-transitive epsilon-connected ordinal set

sup (rng a) is epsilon-transitive epsilon-connected ordinal set

X is epsilon-transitive non empty subset-closed Tarski universal set

On X is epsilon-transitive epsilon-connected ordinal non empty set

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

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

W is epsilon-transitive epsilon-connected ordinal Element of X

a is Relation-like On X -defined On X -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of bool [:(On X),(On X):]

succ W is epsilon-transitive epsilon-connected ordinal non empty Element of X

{W} is non empty trivial 1 -element set

W \/ {W} is non empty set

b is Relation-like On X -defined On X -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of bool [:(On X),(On X):]

dom b is epsilon-transitive epsilon-connected ordinal set

dom a is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal set

b . M is epsilon-transitive epsilon-connected ordinal set

a . M is epsilon-transitive epsilon-connected ordinal set

(succ W) +^ (a . M) is epsilon-transitive epsilon-connected ordinal set

c

b . c

a . c

(succ W) +^ (a . c

(succ W) +^ a is Relation-like T-Sequence-like Function-like Ordinal-yielding set

M is epsilon-transitive epsilon-connected ordinal set

b . M is epsilon-transitive epsilon-connected ordinal set

c

a . c

(succ W) +^ (a . c

X is epsilon-transitive non empty subset-closed Tarski universal set

On X is epsilon-transitive epsilon-connected ordinal non empty set

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

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

W is epsilon-transitive epsilon-connected ordinal Element of X

a is Relation-like On X -defined On X -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of bool [:(On X),(On X):]

0-element_of X is epsilon-transitive epsilon-connected ordinal Element of X

b is Relation-like On X -defined On X -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of bool [:(On X),(On X):]

b . (0-element_of X) is epsilon-transitive epsilon-connected ordinal Element of X

b | NAT is Relation-like rng b -valued T-Sequence-like Function-like Ordinal-yielding set

rng b is set

sup (b | NAT) is epsilon-transitive epsilon-connected ordinal set

rng (b | NAT) is set

sup (rng (b | NAT)) is epsilon-transitive epsilon-connected ordinal set

dom b is epsilon-transitive epsilon-connected ordinal set

dom (b | NAT) is epsilon-transitive epsilon-connected ordinal set

M is epsilon-transitive epsilon-connected ordinal Element of X

dom a is epsilon-transitive epsilon-connected ordinal set

a | M is Relation-like rng a -valued T-Sequence-like Function-like Ordinal-yielding set

rng a is set

dom (a | M) is epsilon-transitive epsilon-connected ordinal set

u is epsilon-transitive epsilon-connected ordinal set

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

u is epsilon-transitive epsilon-connected ordinal set

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

u is epsilon-transitive epsilon-connected ordinal set

u +^ u is epsilon-transitive epsilon-connected ordinal set

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

u is epsilon-transitive epsilon-connected ordinal set

u +^ u is epsilon-transitive epsilon-connected ordinal set

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

succ u is epsilon-transitive epsilon-connected ordinal non empty set

{u} is non empty trivial 1 -element set

u \/ {u} is non empty set

u +^ (succ u) is epsilon-transitive epsilon-connected ordinal set

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

xi is epsilon-transitive epsilon-connected ordinal Element of X

a is epsilon-transitive epsilon-connected ordinal Element of X

b . a is epsilon-transitive epsilon-connected ordinal Element of X

a . (b . a) is epsilon-transitive epsilon-connected ordinal Element of X

succ a is epsilon-transitive epsilon-connected ordinal non empty Element of X

{a} is non empty trivial 1 -element set

a \/ {a} is non empty set

b . xi is epsilon-transitive epsilon-connected ordinal Element of X

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

(b | NAT) . a is epsilon-transitive epsilon-connected ordinal set

(b | NAT) . xi is epsilon-transitive epsilon-connected ordinal set

u +^ {} is epsilon-transitive epsilon-connected ordinal set

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

u is epsilon-transitive epsilon-connected ordinal set

u +^ u is epsilon-transitive epsilon-connected ordinal set

a . M is epsilon-transitive epsilon-connected ordinal Element of X

sup (a | M) is epsilon-transitive epsilon-connected ordinal set

rng (a | M) is set

sup (rng (a | M)) is epsilon-transitive epsilon-connected ordinal set

lim (a | M) is epsilon-transitive epsilon-connected ordinal set

u is epsilon-transitive epsilon-connected ordinal set

u is epsilon-transitive epsilon-connected ordinal set

u is set

(a | M) . u is set

xi is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal set

A is set

(b | NAT) . A is set

B is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal Element of X

succ e is epsilon-transitive epsilon-connected ordinal non empty Element of X

{e} is non empty trivial 1 -element set

e \/ {e} is non empty set

a . xi is epsilon-transitive epsilon-connected ordinal set

a . a is epsilon-transitive epsilon-connected ordinal set

b . (succ e) is epsilon-transitive epsilon-connected ordinal Element of X

b . e is epsilon-transitive epsilon-connected ordinal Element of X

a . (b . e) is epsilon-transitive epsilon-connected ordinal Element of X

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

X is epsilon-transitive non empty subset-closed Tarski universal set

On X is epsilon-transitive epsilon-connected ordinal non empty set

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

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

W is Relation-like non-empty X -valued T-Sequence-like Function-like DOMAIN-yielding 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 Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

c

M is set

dom c

rng c

u is epsilon-transitive epsilon-connected ordinal Element of X

W . u is non empty Element of X

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

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

c

u is Relation-like VAR -defined W . u -valued Function-like quasi_total Element of bool [:VAR,(W . u):]

(Union W) ! u is Relation-like VAR -defined Union W -valued Function-like quasi_total Element of bool [:VAR,(Union W):]

[:VAR,(Union W):] is non empty set

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

u is Relation-like VAR -defined W . u -valued Function-like quasi_total Element of bool [:VAR,(W . u):]

(Union W) ! u is Relation-like VAR -defined Union W -valued Function-like quasi_total Element of bool [:VAR,(Union W):]

b is Relation-like Function-like 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

[:NAT,NAT:] is non empty V41() set

bool [:NAT,NAT:] is non empty V41() set

card WFF is epsilon-transitive epsilon-connected ordinal non empty cardinal set

card (bool [:NAT,NAT:]) is epsilon-transitive epsilon-connected ordinal non empty V41() cardinal set

card X is epsilon-transitive epsilon-connected ordinal non empty cardinal set

0-element_of X is epsilon-transitive epsilon-connected ordinal Element of X

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))):]

uncurry M is Relation-like [:WFF,(On X):] -defined On X -valued Function-like quasi_total Element of bool [:[:WFF,(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

c

c

M is epsilon-transitive epsilon-connected ordinal Element of X

c

W . M is non empty Element of X

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

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

u is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

u is Relation-like VAR -defined W . M -valued Function-like quasi_total Element of bool [:VAR,(W . M):]

(Union W) ! u is Relation-like VAR -defined Union W -valued Function-like quasi_total Element of bool [:VAR,(Union W):]

[:VAR,(Union W):] is non empty set

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

M . u is set

u is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )

xi is Relation-like On X -defined On X -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of bool [:(On X),(On X):]

dom xi is epsilon-transitive epsilon-connected ordinal set

xi . M is epsilon-transitive epsilon-connected ordinal Element of X

a is epsilon-transitive epsilon-connected ordinal Element of X

xi . a is epsilon-transitive epsilon-connected ordinal set

c

xi . a is epsilon-transitive epsilon-connected ordinal Element of X

xi | a is Relation-like rng xi -valued T-Sequence-like Function-like Ordinal-yielding set

rng xi is set

lim (xi | a) is epsilon-transitive epsilon-connected ordinal set

A is epsilon-transitive epsilon-connected ordinal set

dom (xi | a) is epsilon-transitive epsilon-connected ordinal set

sup (xi | a) is epsilon-transitive epsilon-connected ordinal set

rng (xi | a) is set

sup (rng (xi | a)) is epsilon-transitive epsilon-connected ordinal set

B is epsilon-transitive epsilon-connected ordinal set

e is set

(xi | a) . e is set

e is epsilon-transitive epsilon-connected ordinal set

e is epsilon-transitive epsilon-connected ordinal Element of X

succ e is epsilon-transitive epsilon-connected ordinal non empty Element of X

{e} is non empty trivial 1 -element set

e \/ {e} is non empty set

xi . e is epsilon-transitive epsilon-connected ordinal Element of X

xi . (succ e) is epsilon-transitive epsilon-connected ordinal Element of X

dom c

c

c

rng c

rng (c

c

sup (c

sup (rng (c

a is epsilon-transitive epsilon-connected ordinal Element of X

xi . a is epsilon-transitive epsilon-connected ordinal set

c

succ a is epsilon-transitive epsilon-connected ordinal non empty Element of X

{a} is non empty trivial 1 -element set

a \/ {a} is non empty set

xi . (succ a) is epsilon-transitive epsilon-connected ordinal set

c

{(succ a)} is non empty trivial 1 -element Element of X

[u,(succ a)] is set

{u,(succ a)} is non empty set

{u} is functional non empty trivial 1 -element set

{{u,(succ a)},{u}} is non empty set

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

dom (uncurry M) is Relation-like set

(uncurry M) . (u,(succ a)) is set

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

xi . (succ a) is epsilon-transitive epsilon-connected ordinal Element of X

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

c

{(c

{(c

sup ({(c

c

xi . (0-element_of X) is epsilon-transitive epsilon-connected ordinal set

c

X is epsilon-transitive non empty subset-closed Tarski universal set

W is epsilon-transitive epsilon-connected ordinal Element of X

Rank W is epsilon-transitive set

On X is epsilon-transitive epsilon-connected ordinal non empty set

Rank (On X) is epsilon-transitive set

X is epsilon-transitive non empty subset-closed Tarski universal set

W is epsilon-transitive epsilon-connected ordinal Element of X

Rank W is epsilon-transitive set

a is non empty set

X is epsilon-transitive non empty subset-closed Tarski universal set

On X is epsilon-transitive epsilon-connected ordinal non empty set

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

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

1-element_of X is epsilon-transitive epsilon-connected ordinal non empty Element of X

Rank (1-element_of X) is epsilon-transitive set

W is Relation-like T-Sequence-like Function-like set

dom W is epsilon-transitive epsilon-connected ordinal set

W . {} is set

a is epsilon-transitive epsilon-connected ordinal Element of X

W . a is set

Rank a is epsilon-transitive set

a is epsilon-transitive epsilon-connected ordinal Element of X

succ a is epsilon-transitive epsilon-connected ordinal non empty Element of X

{a} is non empty trivial 1 -element set

a \/ {a} is non empty set

W . (succ a) is set

Rank (succ a) is epsilon-transitive set

a is epsilon-transitive epsilon-connected ordinal Element of X

W . a is set

Rank a is epsilon-transitive set

b is epsilon-transitive epsilon-connected ordinal set

succ b is epsilon-transitive epsilon-connected ordinal non empty set

{b} is non empty trivial 1 -element set

b \/ {b} is non empty set

M is epsilon-transitive epsilon-connected ordinal Element of X

succ M is epsilon-transitive epsilon-connected ordinal non empty Element of X

{M} is non empty trivial 1 -element set

M \/ {M} is non empty set

W . (succ M) is set

Rank (succ M) is epsilon-transitive set

b is epsilon-transitive epsilon-connected ordinal set

succ b is epsilon-transitive epsilon-connected ordinal non empty 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

M is epsilon-transitive epsilon-connected ordinal Element of X

Rank M is epsilon-transitive set

a is Relation-like X -valued T-Sequence-like Function-like set

rng a is set

b is set

a . b is set

M is epsilon-transitive epsilon-connected ordinal Element of X

a . M is set

Rank M is epsilon-transitive set

b is Relation-like non-empty X -valued T-Sequence-like Function-like DOMAIN-yielding 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

Rank (On X) is epsilon-transitive set

c

Rank c

M is epsilon-transitive epsilon-connected ordinal Element of X

b . M is non empty Element of X

Rank M is epsilon-transitive set

0-element_of X is epsilon-transitive epsilon-connected ordinal Element of X

M is epsilon-transitive epsilon-connected ordinal Element of X

b . M is non empty Element of X

c

b . c

Rank M is epsilon-transitive set

Rank c

succ M is epsilon-transitive epsilon-connected ordinal non empty Element of X

{M} is non empty trivial 1 -element set

M \/ {M} is non empty set

succ (0-element_of X) is epsilon-transitive epsilon-connected ordinal non empty Element of X

{(0-element_of X)} is non empty trivial 1 -element set

(0-element_of X) \/ {(0-element_of X)} is non empty set

M is epsilon-transitive epsilon-connected ordinal Element of X

b . M is non empty Element of X

b | M is Relation-like rng b -valued T-Sequence-like Function-like set

rng b is V72() set

Union (b | M) is set

Rank M is epsilon-transitive set

c

M is epsilon-transitive epsilon-connected ordinal set

Rank M is epsilon-transitive set

u is epsilon-transitive epsilon-connected ordinal Element of X

succ u is epsilon-transitive epsilon-connected ordinal non empty Element of X

{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

Rank (succ u) is epsilon-transitive set

Rank u is epsilon-transitive set

c

rng (b | M) is set

union (rng (b | M)) is set

M is set

dom (b | M) is epsilon-transitive epsilon-connected ordinal set

u is set

(b | M) . u is set

u is epsilon-transitive epsilon-connected ordinal set

b . u is set

u is epsilon-transitive epsilon-connected ordinal Element of X

b . u is non empty Element of X

M is Relation-like On X -defined On X -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of bool [:(On X),(On X):]

c

M . c

Rank c

M is non empty set

b . c

X is epsilon-transitive non empty subset-closed Tarski universal set

W is epsilon-transitive epsilon-connected ordinal Element of X

On X is epsilon-transitive epsilon-connected ordinal non empty set

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

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

a is Relation-like On X -defined On X -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of bool [:(On X),(On X):]

b is epsilon-transitive epsilon-connected ordinal Element of X

a . b is epsilon-transitive epsilon-connected ordinal Element of X

Rank b is epsilon-transitive set

M is non empty set

X is epsilon-transitive non empty subset-closed Tarski universal set

the epsilon-transitive epsilon-connected ordinal Element of X is epsilon-transitive epsilon-connected ordinal Element of X

On X is epsilon-transitive epsilon-connected ordinal non empty set

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

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

a is Relation-like On X -defined On X -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of bool [:(On X),(On X):]

b is epsilon-transitive epsilon-connected ordinal Element of X

a . b is epsilon-transitive epsilon-connected ordinal Element of X

Rank b is epsilon-transitive set

M is non empty set

X is epsilon-transitive non empty subset-closed Tarski universal set

On X is epsilon-transitive epsilon-connected ordinal non empty set

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

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

W is Relation-like non-empty X -valued T-Sequence-like Function-like DOMAIN-yielding set

Union W is non empty Element of bool X

bool X is non empty set

a is Relation-like On X -defined On X -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of bool [:(On X),(On X):]

b is epsilon-transitive epsilon-connected ordinal Element of X

a . b is epsilon-transitive epsilon-connected ordinal Element of X

W . b is non empty Element of X

X is epsilon-transitive non empty subset-closed Tarski universal set

On X is epsilon-transitive epsilon-connected ordinal non empty set

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

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

W is Relation-like On X -defined On X -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of bool [:(On X),(On X):]

a is epsilon-transitive epsilon-connected ordinal Element of X

W . a is epsilon-transitive epsilon-connected ordinal Element of X

Rank a is epsilon-transitive set

b is non empty set

X is epsilon-transitive non empty subset-closed Tarski universal set

W is epsilon-transitive epsilon-connected ordinal Element of X

a is epsilon-transitive epsilon-connected ordinal Element of X

b is non empty set

Rank a is epsilon-transitive set

X is epsilon-transitive non empty subset-closed Tarski universal set

W is epsilon-transitive epsilon-connected ordinal Element of X

a is non empty set

Rank W is epsilon-transitive set

X is epsilon-transitive non empty subset-closed Tarski universal set

W is epsilon-transitive epsilon-connected ordinal Element of X

a is non empty set

Rank W is epsilon-transitive set

X is set

W is epsilon-transitive non empty subset-closed Tarski universal set

On W is epsilon-transitive epsilon-connected ordinal non empty set

Rank (On W) is epsilon-transitive set

the_rank_of X is epsilon-transitive epsilon-connected ordinal set

the_rank_of W is epsilon-transitive epsilon-connected ordinal set

a is epsilon-transitive epsilon-connected ordinal Element of W

b is epsilon-transitive epsilon-connected ordinal Element of W

M is non empty set

Rank b is epsilon-transitive set

Rank a is epsilon-transitive set

succ a is epsilon-transitive epsilon-connected ordinal non empty Element of W

{a} is non empty trivial 1 -element set

a \/ {a} is non empty set

Rank (succ a) is epsilon-transitive set