:: 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₆ is Relation-like VAR -defined b -valued Function-like quasi_total Element of bool [:VAR,b:]
M is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
b ! c₆ is Relation-like VAR -defined b -valued Function-like quasi_total Element of bool [:VAR,b:]
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₆ is Relation-like NAT -defined NAT -valued Function-like V49() ZF-formula-like M7( NAT )
Free c₆ is V41() Element of bool VAR
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₆ is Element of VAR
M . c₆ is Element of W
(W ! the Relation-like VAR -defined X -valued Function-like quasi_total Element of bool [:VAR,X:]) . c₆ is Element of W
[: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₆ is epsilon-transitive epsilon-connected ordinal Element of X
{c₆} is non empty trivial 1 -element Element of X
{c₆} \/ ((uncurry a) .: [:W,{(succ M)}:]) is non empty set
sup ({c₆} \/ ((uncurry a) .: [:W,{(succ M)}:])) 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
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₆ is set
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₆ is set
b . c₆ is set
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₆ is epsilon-transitive epsilon-connected ordinal set
dom M is epsilon-transitive epsilon-connected ordinal set
M . c₆ is epsilon-transitive epsilon-connected ordinal set
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₆ is epsilon-transitive epsilon-connected ordinal set
dom M is epsilon-transitive epsilon-connected ordinal set
M . c₆ is epsilon-transitive epsilon-connected ordinal set
M | c₆ is Relation-like rng M -valued T-Sequence-like Function-like Ordinal-yielding set
rng M is set
M is epsilon-transitive epsilon-connected ordinal set
dom (M | c₆) is epsilon-transitive epsilon-connected ordinal set
sup (M | c₆) is epsilon-transitive epsilon-connected ordinal set
rng (M | c₆) is set
sup (rng (M | c₆)) is epsilon-transitive epsilon-connected ordinal set
c₆ is epsilon-transitive epsilon-connected ordinal Element of X
succ c₆ is epsilon-transitive epsilon-connected ordinal non empty Element of X
{c₆} is non empty trivial 1 -element set
c₆ \/ {c₆} is non empty set
M . (succ c₆) is epsilon-transitive epsilon-connected ordinal Element of X
M . c₆ is epsilon-transitive epsilon-connected ordinal Element of X
{(M . c₆)} is non empty trivial 1 -element Element of X
{(succ c₆)} is non empty trivial 1 -element Element of X
[:W,{(succ c₆)}:] is non empty set
(uncurry a) .: [:W,{(succ c₆)}:] is set
{(M . c₆)} \/ ((uncurry a) .: [:W,{(succ c₆)}:]) is non empty set
sup ({(M . c₆)} \/ ((uncurry a) .: [:W,{(succ c₆)}:])) is epsilon-transitive epsilon-connected ordinal set
c₆ is epsilon-transitive epsilon-connected ordinal Element of X
M . c₆ is epsilon-transitive epsilon-connected ordinal Element of X
M | c₆ is Relation-like rng M -valued T-Sequence-like Function-like Ordinal-yielding set
rng M is set
sup (M | c₆) is epsilon-transitive epsilon-connected ordinal set
rng (M | c₆) is set
sup (rng (M | c₆)) 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
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₆ is epsilon-transitive epsilon-connected ordinal set
X +^ c₆ 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
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₆ is epsilon-transitive epsilon-connected ordinal set
X +^ c₆ is epsilon-transitive epsilon-connected ordinal set
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₆ is epsilon-transitive epsilon-connected ordinal set
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₆ is epsilon-transitive epsilon-connected ordinal Element of X
b . c₆ is epsilon-transitive epsilon-connected ordinal Element of X
a . c₆ is epsilon-transitive epsilon-connected ordinal Element of X
(succ W) +^ (a . c₆) is epsilon-transitive epsilon-connected ordinal Element of X
(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₆ is epsilon-transitive epsilon-connected ordinal Element of X
a . c₆ is epsilon-transitive epsilon-connected ordinal Element of X
(succ W) +^ (a . c₆) is epsilon-transitive epsilon-connected ordinal 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 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₆ 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 is set
dom c₆ is epsilon-transitive epsilon-connected ordinal set
rng c₆ is set
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 epsilon-transitive epsilon-connected ordinal Element of X
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₆ 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₆ . (0-element_of X) is epsilon-transitive epsilon-connected ordinal Element of X
M is epsilon-transitive epsilon-connected ordinal Element of X
c₆ . M is epsilon-transitive epsilon-connected ordinal Element of X
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₆ . a is epsilon-transitive epsilon-connected ordinal set
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₆ is epsilon-transitive epsilon-connected ordinal set
c₆ . (succ e) is epsilon-transitive epsilon-connected ordinal Element of X
c₆ | a is Relation-like rng c₆ -valued T-Sequence-like Function-like Ordinal-yielding set
rng c₆ is set
rng (c₆ | a) is set
c₆ . a is epsilon-transitive epsilon-connected ordinal Element of X
sup (c₆ | a) is epsilon-transitive epsilon-connected ordinal set
sup (rng (c₆ | a)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal Element of X
xi . a is epsilon-transitive epsilon-connected ordinal set
c₆ . a is epsilon-transitive epsilon-connected ordinal set
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 epsilon-transitive epsilon-connected ordinal 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} 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₆ . a is epsilon-transitive epsilon-connected ordinal Element of X
{(c₆ . a)} is non empty trivial 1 -element Element of X
{(c₆ . a)} \/ ((uncurry M) .: [:WFF,{(succ a)}:]) is non empty set
sup ({(c₆ . a)} \/ ((uncurry M) .: [:WFF,{(succ a)}:])) is epsilon-transitive epsilon-connected ordinal set
c₆ . (succ a) is epsilon-transitive epsilon-connected ordinal Element of X
xi . (0-element_of X) is epsilon-transitive epsilon-connected ordinal set
c₆ . (0-element_of X) is epsilon-transitive epsilon-connected ordinal 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
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₆ is epsilon-transitive epsilon-connected ordinal set
Rank c₆ is epsilon-transitive set
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₆ is epsilon-transitive epsilon-connected ordinal Element of X
b . c₆ is non empty Element of X
Rank M is epsilon-transitive set
Rank c₆ is epsilon-transitive 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
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₆ is set
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₆ is set
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₆ is epsilon-transitive epsilon-connected ordinal Element of X
M . c₆ is epsilon-transitive epsilon-connected ordinal Element of X
Rank c₆ is epsilon-transitive set
M is non empty set
b . c₆ is non empty Element of X
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