:: ZF_REFLE semantic presentation

REAL is set
NAT is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty V35() cardinal limit_cardinal countable denumerable Element of K40(REAL)
K40(REAL) is non empty set
NAT is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty V35() cardinal limit_cardinal countable denumerable set
K40(NAT) is non empty V35() set
K40(NAT) is non empty V35() set
VAR is non empty countable Element of K40(NAT)
5 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() non empty V20() V35() cardinal countable Element of NAT
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT : 5 <= b₁ } is set
K40(VAR) is non empty set
{} is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real V16() empty V20() Function-like one-to-one constant functional V35() cardinal {} -element Cardinal-yielding countable set
the Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real V16() empty V20() Function-like one-to-one constant functional V35() cardinal {} -element Cardinal-yielding countable set is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real V16() empty V20() Function-like one-to-one constant functional V35() cardinal {} -element Cardinal-yielding countable set
1 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() non empty V20() V35() cardinal countable Element of NAT
0 is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real V16() empty V20() Function-like one-to-one constant functional V35() cardinal {} -element Cardinal-yielding countable Element of NAT
the_axiom_of_pairs is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
x. 0 is Element of VAR
5 + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
x. 1 is Element of VAR
5 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
2 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() non empty V20() V35() cardinal countable Element of NAT
x. 2 is Element of VAR
5 + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() non empty V20() V35() cardinal countable Element of NAT
x. 3 is Element of VAR
5 + 3 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
(x. 3) 'in' (x. 2) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K210(NAT,1) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K219((x. 3)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,1),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K219((x. 2)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 3))),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 3) '=' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K210(NAT,0) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,0),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K219((x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,0),K219((x. 3))),K219((x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 3) '=' (x. 1) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K219((x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,0),K219((x. 3))),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 3) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K210(NAT,2) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,2),((x. 3) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((x. 3) '=' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
('not' ((x. 3) '=' (x. 0))) '&' ('not' ((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K210(NAT,3) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,3),('not' ((x. 3) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),('not' ((x. 3) '=' (x. 0)))),('not' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (('not' ((x. 3) '=' (x. 0))) '&' ('not' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(('not' ((x. 3) '=' (x. 0))) '&' ('not' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
((x. 3) 'in' (x. 2)) => (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' (x. 2)) '&' ('not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 2))),('not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 3) 'in' (x. 2)) '&' ('not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 3) 'in' (x. 2)) '&' ('not' (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) => ((x. 3) 'in' (x. 2)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 3) 'in' (x. 2)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 3) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) '&' ('not' ((x. 3) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))),('not' ((x. 3) 'in' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) '&' ('not' ((x. 3) 'in' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) '&' ('not' ((x. 3) 'in' (x. 2))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 3) 'in' (x. 2)) => (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))) '&' ((((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) => ((x. 3) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 3) 'in' (x. 2)) => (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(((x. 3) 'in' (x. 2)) => (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))),((((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))) => ((x. 3) 'in' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
4 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() non empty V20() V35() cardinal countable Element of NAT
K210(NAT,4) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,4),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 2),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,4),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 2))),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 2),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 2),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),(x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,4),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 1))),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),(All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,4),K219((x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 0))),(All ((x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
the_axiom_of_unions is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
(x. 2) 'in' (x. 1) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,1),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 2))),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 2) 'in' (x. 3) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 2))),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 3) 'in' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 3))),K219((x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 3))),((x. 3) 'in' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 3),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 3),('not' (((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
((x. 2) 'in' (x. 1)) => (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 1)) '&' ('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 1))),('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 2) 'in' (x. 1)) '&' ('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 2) 'in' (x. 1)) '&' ('not' (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 2) 'in' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))),('not' ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 2) 'in' (x. 1)) => (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))) '&' ((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 2) 'in' (x. 1)) => (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(((x. 2) 'in' (x. 1)) => (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))),((Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 2))),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 1))),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 0))),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
the_axiom_of_infinity is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
(x. 1) 'in' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,1),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 1))),K219((x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 2) 'in' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 2))),K219((x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 3) '=' (x. 2) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,0),K219((x. 3))),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((x. 3) '=' (x. 2)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 3) '=' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 0))),('not' ((x. 3) '=' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
x. 4 is Element of VAR
5 + 4 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
(x. 4) 'in' (x. 2) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K219((x. 4)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,1),K219((x. 4))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 4))),K219((x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 4) 'in' (x. 3) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 4))),K219((x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 4) 'in' (x. 3)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 4) 'in' (x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) 'in' (x. 2)) '&' ('not' ((x. 4) 'in' (x. 3))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 4) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 4) 'in' (x. 2))),('not' ((x. 4) 'in' (x. 3)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 4) 'in' (x. 2)) '&' ('not' ((x. 4) 'in' (x. 3)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 4) 'in' (x. 2)) '&' ('not' ((x. 4) 'in' (x. 3))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,4),K219((x. 4))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 4))),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2))))),(All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),('not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),('not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 3),('not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 3),('not' ((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 0)) '&' ('not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 0))),('not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 2) 'in' (x. 0)) '&' ('not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 2) 'in' (x. 0)) '&' ('not' (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 2))),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 1) 'in' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 1) 'in' (x. 0))),(All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 0),(x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 1),('not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 1))),('not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 1),('not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 1),('not' (((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 0),(Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),('not' (Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 0))),('not' (Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 0),('not' (Ex ((x. 1),(((x. 1) 'in' (x. 0)) '&' (All ((x. 2),(((x. 2) 'in' (x. 0)) => (Ex ((x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All ((x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
the_axiom_of_power_sets is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 3) 'in' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 3) 'in' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' (x. 2)) '&' ('not' ((x. 3) 'in' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 2))),('not' ((x. 3) 'in' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 3) 'in' (x. 2)) '&' ('not' ((x. 3) 'in' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 3) 'in' (x. 2)) '&' ('not' ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
((x. 2) 'in' (x. 1)) => (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 2) 'in' (x. 1)) '&' ('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 2) 'in' (x. 1))),('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 2) 'in' (x. 1)) '&' ('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 2) 'in' (x. 1)) '&' ('not' (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))),('not' ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) '&' ('not' ((x. 2) 'in' (x. 1))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 2) 'in' (x. 1)) => (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))) '&' ((All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 2) 'in' (x. 1)) => (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(((x. 2) 'in' (x. 1)) => (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))),((All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))) => ((x. 2) 'in' (x. 1)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 2))),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 1))),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 1),('not' (All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 0))),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (All ((x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
{(x. 0),(x. 1),(x. 2)} is non empty set
(x. 4) '=' (x. 0) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,0),K219((x. 4))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,0),K219((x. 4))),K219((x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
M is epsilon-transitive non empty subset-closed Tarski universal set
L is Element of M
M is Element of M
{L,M} is non empty Element of M
M is epsilon-transitive non empty subset-closed Tarski universal set
L is Element of M
union L is Element of M
M is epsilon-transitive non empty subset-closed Tarski universal set
L is Element of M
M is Element of M
H is Element of M
phi is epsilon-transitive epsilon-connected ordinal set
succ phi is epsilon-transitive epsilon-connected ordinal non empty set
{phi} is non empty trivial 1 -element set
phi \/ {phi} is non empty set
a is Element of M
f is Element of M
M is Element of M
M is epsilon-transitive non empty subset-closed Tarski universal set
L is Element of M
bool L is non empty Element of M
M /\ (bool L) is set
M is epsilon-transitive non empty subset-closed Tarski universal set
K41(VAR,M) is Relation-like non empty set
K40(K41(VAR,M)) is non empty set
L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
Free L is V35() countable Element of K40(VAR)
L <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
L => ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
L '&' ('not' ((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),L) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),L),('not' ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (L '&' ('not' ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(L '&' ('not' ((x. 4) '=' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) '=' (x. 0)) => L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),L) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) '=' (x. 0)) '&' ('not' L) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 4) '=' (x. 0))),('not' L)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 4) '=' (x. 0)) '&' ('not' L)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 4) '=' (x. 0)) '&' ('not' L))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(L => ((x. 4) '=' (x. 0))) '&' (((x. 4) '=' (x. 0)) => L) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(L => ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(L => ((x. 4) '=' (x. 0)))),(((x. 4) '=' (x. 0)) => L)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 4))),(L <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 0))),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
M is Relation-like VAR -defined M -valued Function-like quasi_total Element of K40(K41(VAR,M))
def_func' (L,M) is Relation-like M -defined M -valued Function-like quasi_total Element of K40(K41(M,M))
K41(M,M) is Relation-like non empty set
K40(K41(M,M)) is non empty set
H is Element of M
(def_func' (L,M)) .: H is Element of K40(M)
K40(M) is non empty set
card H is epsilon-transitive epsilon-connected ordinal cardinal set
card M is epsilon-transitive epsilon-connected ordinal non empty cardinal set
card ((def_func' (L,M)) .: H) is epsilon-transitive epsilon-connected ordinal cardinal set
L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
Free L is V35() countable Element of K40(VAR)
the_axiom_of_substitution_for L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
L <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
L => ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
L '&' ('not' ((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),L) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),L),('not' ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (L '&' ('not' ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(L '&' ('not' ((x. 4) '=' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) '=' (x. 0)) => L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),L) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) '=' (x. 0)) '&' ('not' L) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 4) '=' (x. 0))),('not' L)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 4) '=' (x. 0)) '&' ('not' L)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 4) '=' (x. 0)) '&' ('not' L))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(L => ((x. 4) '=' (x. 0))) '&' (((x. 4) '=' (x. 0)) => L) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(L => ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(L => ((x. 4) '=' (x. 0)))),(((x. 4) '=' (x. 0)) => L)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 4))),(L <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 0))),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 3) 'in' (x. 1) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 3))),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' (x. 1)) '&' L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 1))),L) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (((x. 3) 'in' (x. 1)) '&' L) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 3) 'in' (x. 1)) '&' L)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),('not' (((x. 3) 'in' (x. 1)) '&' L))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),('not' (((x. 3) 'in' (x. 1)) '&' L))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 3),('not' (((x. 3) 'in' (x. 1)) '&' L)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 3),('not' (((x. 3) 'in' (x. 1)) '&' L))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
((x. 4) 'in' (x. 2)) => (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) 'in' (x. 2)) '&' ('not' (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 4) 'in' (x. 2))),('not' (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 4) 'in' (x. 2)) '&' ('not' (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 4) 'in' (x. 2)) '&' ('not' (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) => ((x. 4) 'in' (x. 2)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 4) 'in' (x. 2)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 4) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) '&' ('not' ((x. 4) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))),('not' ((x. 4) 'in' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) '&' ('not' ((x. 4) 'in' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) '&' ('not' ((x. 4) 'in' (x. 2))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 4) 'in' (x. 2)) => (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))) '&' ((Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) => ((x. 4) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 4) 'in' (x. 2)) => (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(((x. 4) 'in' (x. 2)) => (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))),((Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) => ((x. 4) 'in' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 4))),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 2),('not' (All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 2))),('not' (All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 2),('not' (All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 2),('not' (All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 1))),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))))) => (All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))))) '&' ('not' (All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))))),('not' (All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))))) '&' ('not' (All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))))) '&' ('not' (All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
M is epsilon-transitive non empty subset-closed Tarski universal set
L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
Free L is V35() countable Element of K40(VAR)
the_axiom_of_substitution_for L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
L <=> ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
L => ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 4) '=' (x. 0)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
L '&' ('not' ((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),L) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),L),('not' ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (L '&' ('not' ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(L '&' ('not' ((x. 4) '=' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) '=' (x. 0)) => L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),L) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) '=' (x. 0)) '&' ('not' L) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 4) '=' (x. 0))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 4) '=' (x. 0))),('not' L)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 4) '=' (x. 0)) '&' ('not' L)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 4) '=' (x. 0)) '&' ('not' L))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(L => ((x. 4) '=' (x. 0))) '&' (((x. 4) '=' (x. 0)) => L) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(L => ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(L => ((x. 4) '=' (x. 0)))),(((x. 4) '=' (x. 0)) => L)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 4))),(L <=> ((x. 4) '=' (x. 0)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 0))),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 0),('not' (All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(x. 3) 'in' (x. 1) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((x. 3))),K219((x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 3) 'in' (x. 1)) '&' L is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 1))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 3) 'in' (x. 1))),L) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (((x. 3) 'in' (x. 1)) '&' L) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 3) 'in' (x. 1)) '&' L)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 3),('not' (((x. 3) 'in' (x. 1)) '&' L))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 3))),('not' (((x. 3) 'in' (x. 1)) '&' L))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 3),('not' (((x. 3) 'in' (x. 1)) '&' L)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 3),('not' (((x. 3) 'in' (x. 1)) '&' L))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
((x. 4) 'in' (x. 2)) => (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((x. 4) 'in' (x. 2)) '&' ('not' (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),((x. 4) 'in' (x. 2))),('not' (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (((x. 4) 'in' (x. 2)) '&' ('not' (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(((x. 4) 'in' (x. 2)) '&' ('not' (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) => ((x. 4) 'in' (x. 2)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' ((x. 4) 'in' (x. 2)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((x. 4) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) '&' ('not' ((x. 4) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))),('not' ((x. 4) 'in' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) '&' ('not' ((x. 4) 'in' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) '&' ('not' ((x. 4) 'in' (x. 2))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(((x. 4) 'in' (x. 2)) => (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))) '&' ((Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) => ((x. 4) 'in' (x. 2))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(((x. 4) 'in' (x. 2)) => (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(((x. 4) 'in' (x. 2)) => (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))),((Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))) => ((x. 4) 'in' (x. 2)))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 4))),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 2),('not' (All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 2))),('not' (All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' (All ((x. 2),('not' (All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 2),('not' (All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((x. 1))),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))))) => (All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
(All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))))) '&' ('not' (All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0)))))))))),('not' (All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
'not' ((All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))))) '&' ('not' (All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L)))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),((All ((x. 3),(Ex ((x. 0),(All ((x. 4),(L <=> ((x. 4) '=' (x. 0))))))))) '&' ('not' (All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' L))))))))))))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
F₂() is non empty set
F₁() is epsilon-transitive non empty subset-closed Tarski universal set
M is Element of F₂()
L is epsilon-transitive epsilon-connected ordinal Element of F₁()
M is epsilon-transitive epsilon-connected ordinal set
M is Relation-like Function-like set
dom M is set
L is Element of F₂()
M . L is set
M is epsilon-transitive epsilon-connected ordinal set
H is epsilon-transitive epsilon-connected ordinal Element of F₁()
phi is epsilon-transitive epsilon-connected ordinal Element of F₁()
a is epsilon-transitive epsilon-connected ordinal Element of F₁()
L is set
M is epsilon-transitive non empty subset-closed Tarski universal set
On M is epsilon-transitive epsilon-connected ordinal non empty set
H is set
M is epsilon-transitive non empty subset-closed Tarski universal set
On M is epsilon-transitive epsilon-connected ordinal non empty set
F₁() is epsilon-transitive non empty subset-closed Tarski universal set
On F₁() is epsilon-transitive epsilon-connected ordinal non empty set
K41((On F₁()),(On F₁())) is Relation-like non empty set
K40(K41((On F₁()),(On F₁()))) is non empty set
M is set
L is epsilon-transitive epsilon-connected ordinal Element of F₁()
M is epsilon-transitive epsilon-connected ordinal Element of F₁()
H is set
M is Relation-like Function-like set
dom M is set
L is Relation-like T-Sequence-like Function-like set
rng L is set
M is set
dom L is epsilon-transitive epsilon-connected ordinal set
phi is set
L . phi is set
H is epsilon-transitive epsilon-connected ordinal Element of F₁()
M is Relation-like T-Sequence-like Function-like Ordinal-yielding set
H is Relation-like On F₁() -defined On F₁() -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On F₁()),(On F₁())))
phi is epsilon-transitive epsilon-connected ordinal Element of F₁()
H . phi is epsilon-transitive epsilon-connected ordinal Element of F₁()
F₁() is epsilon-transitive non empty subset-closed Tarski universal set
On F₁() is epsilon-transitive epsilon-connected ordinal non empty set
K41((On F₁()),(On F₁())) is Relation-like non empty set
K40(K41((On F₁()),(On F₁()))) is non empty set
0-element_of F₁() is epsilon-transitive epsilon-connected ordinal Element of F₁()
F₂() is epsilon-transitive epsilon-connected ordinal Element of F₁()
M is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom M is epsilon-transitive epsilon-connected ordinal set
M . {} is epsilon-transitive epsilon-connected ordinal set
rng M is set
L is set
M is set
M . M is set
H is epsilon-transitive epsilon-connected ordinal Element of F₁()
M | H is Relation-like rng M -valued T-Sequence-like Function-like Ordinal-yielding set
F₄(H,(M | H)) is epsilon-transitive epsilon-connected ordinal Element of F₁()
phi is epsilon-transitive epsilon-connected ordinal set
succ phi is epsilon-transitive epsilon-connected ordinal non empty set
{phi} is non empty trivial 1 -element set
phi \/ {phi} is non empty set
M . phi is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
F₃(phi,a) is epsilon-transitive epsilon-connected ordinal Element of F₁()
phi is epsilon-transitive epsilon-connected ordinal set
succ phi is epsilon-transitive epsilon-connected ordinal non empty set
{phi} is non empty trivial 1 -element set
phi \/ {phi} is non empty set
L is Relation-like On F₁() -defined On F₁() -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On F₁()),(On F₁())))
L . (0-element_of F₁()) is epsilon-transitive epsilon-connected ordinal Element of F₁()
dom L is epsilon-transitive epsilon-connected ordinal Element of K40((On F₁()))
K40((On F₁())) is non empty set
M is epsilon-transitive epsilon-connected ordinal Element of F₁()
succ M is epsilon-transitive epsilon-connected ordinal non empty Element of F₁()
{M} is non empty trivial 1 -element set
M \/ {M} is non empty set
L . (succ M) is epsilon-transitive epsilon-connected ordinal Element of F₁()
L . M is epsilon-transitive epsilon-connected ordinal Element of F₁()
F₃(M,(L . M)) is epsilon-transitive epsilon-connected ordinal Element of F₁()
M is epsilon-transitive epsilon-connected ordinal Element of F₁()
L . M is epsilon-transitive epsilon-connected ordinal Element of F₁()
L | M is Relation-like On F₁() -defined M -defined On F₁() -defined On F₁() -valued rng L -valued T-Sequence-like Function-like Ordinal-yielding Element of K40(K41((On F₁()),(On F₁())))
rng L is set
F₄(M,(L | M)) is epsilon-transitive epsilon-connected ordinal Element of F₁()
F₁() is epsilon-transitive non empty subset-closed Tarski universal set
0-element_of F₁() is epsilon-transitive epsilon-connected ordinal Element of F₁()
M is epsilon-transitive epsilon-connected ordinal set
L is epsilon-transitive epsilon-connected ordinal Element of F₁()
M is epsilon-transitive epsilon-connected ordinal Element of F₁()
M is epsilon-transitive epsilon-connected ordinal set
succ M is epsilon-transitive epsilon-connected ordinal non empty set
{M} is non empty trivial 1 -element set
M \/ {M} is non empty set
On F₁() is epsilon-transitive epsilon-connected ordinal non empty set
L is epsilon-transitive epsilon-connected ordinal Element of F₁()
succ L is epsilon-transitive epsilon-connected ordinal non empty Element of F₁()
{L} is non empty trivial 1 -element set
L \/ {L} is non empty set
M is epsilon-transitive epsilon-connected ordinal Element of F₁()
L is epsilon-transitive non empty subset-closed Tarski universal set
M is Relation-like Function-like set
M is epsilon-transitive epsilon-connected ordinal Element of L
Rank M is epsilon-transitive set
M | (Rank M) is Relation-like Function-like set
L |` (M | (Rank M)) is Relation-like Function-like set
Union (L |` (M | (Rank M))) is set
M is Relation-like T-Sequence-like Function-like set
L is epsilon-transitive epsilon-connected ordinal set
Rank L is epsilon-transitive set
M | (Rank L) is Relation-like Function-like set
dom (M | (Rank L)) is set
dom M is epsilon-transitive epsilon-connected ordinal set
(dom M) /\ (Rank L) is set
M is set
M is Relation-like T-Sequence-like Function-like Ordinal-yielding set
L is epsilon-transitive epsilon-connected ordinal set
Rank L is epsilon-transitive set
M | (Rank L) is Relation-like Function-like set
rng M is set
H is epsilon-transitive epsilon-connected ordinal set
M is Relation-like T-Sequence-like Function-like set
rng M is set
M is Relation-like T-Sequence-like Function-like Ordinal-yielding set
Union M is epsilon-transitive epsilon-connected ordinal set
M is set
L is Relation-like T-Sequence-like Function-like Ordinal-yielding set
M |` L is Relation-like Function-like set
Union (M |` L) is set
rng L is set
M is epsilon-transitive epsilon-connected ordinal set
rng (M |` L) is set
H is set
union (rng (M |` L)) is set
M is epsilon-transitive epsilon-connected ordinal set
Rank M is epsilon-transitive set
On (Rank M) is set
L is set
M is epsilon-transitive epsilon-connected ordinal set
the_rank_of M is epsilon-transitive epsilon-connected ordinal set
On M is set
M is epsilon-transitive epsilon-connected ordinal set
Rank M is epsilon-transitive set
L is Relation-like T-Sequence-like Function-like Ordinal-yielding set
L | (Rank M) is Relation-like Function-like set
L | M is Relation-like rng L -valued T-Sequence-like Function-like Ordinal-yielding set
rng L is set
dom (L | (Rank M)) is set
dom L is epsilon-transitive epsilon-connected ordinal set
On (dom (L | (Rank M))) is set
On (Rank M) is set
(L | (Rank M)) | M is Relation-like Function-like set
L is epsilon-transitive non empty subset-closed Tarski universal set
M is Relation-like T-Sequence-like Function-like Ordinal-yielding set
M is epsilon-transitive epsilon-connected ordinal Element of L
(M,L,M) is set
Rank M is epsilon-transitive set
M | (Rank M) is Relation-like Function-like set
L |` (M | (Rank M)) is Relation-like Function-like set
Union (L |` (M | (Rank M))) is set
H is Relation-like T-Sequence-like Function-like Ordinal-yielding set
L |` H is Relation-like Function-like set
Union (L |` H) is set
On L is epsilon-transitive epsilon-connected ordinal non empty set
dom H is epsilon-transitive epsilon-connected ordinal set
dom (L |` H) is set
card (dom (L |` H)) is epsilon-transitive epsilon-connected ordinal cardinal set
card L is epsilon-transitive epsilon-connected ordinal non empty cardinal set
(L |` H) .: (dom (L |` H)) is set
rng (L |` H) is set
card (rng (L |` H)) is epsilon-transitive epsilon-connected ordinal cardinal set
union (rng (L |` H)) is set
phi is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive non empty subset-closed Tarski universal set
On M is epsilon-transitive epsilon-connected ordinal non empty set
K41((On M),(On M)) is Relation-like non empty set
K40(K41((On M),(On M))) is non empty set
L is epsilon-transitive epsilon-connected ordinal Element of M
M is Relation-like On M -defined On M -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On M),(On M)))
(M,M,L) is epsilon-transitive epsilon-connected ordinal Element of M
Rank L is epsilon-transitive set
M | (Rank L) is Relation-like Rank L -defined On M -defined On M -valued Function-like set
M |` (M | (Rank L)) is Relation-like On M -defined M -valued On M -valued Function-like set
Union (M |` (M | (Rank L))) is set
M | L is Relation-like On M -defined L -defined On M -defined On M -valued rng M -valued T-Sequence-like Function-like Ordinal-yielding Element of K40(K41((On M),(On M)))
rng M is set
Union (M | L) is epsilon-transitive epsilon-connected ordinal set
((M | L),M,L) is epsilon-transitive epsilon-connected ordinal Element of M
(M | L) | (Rank L) is Relation-like Rank L -defined On M -defined On M -valued Function-like set
M |` ((M | L) | (Rank L)) is Relation-like On M -defined M -valued On M -valued Function-like set
Union (M |` ((M | L) | (Rank L))) is set
rng (M | L) is Element of K40((On M))
K40((On M)) is non empty set
rng M is Element of K40((On M))
M |` (M | L) is Relation-like On M -defined M -valued On M -valued Function-like Element of K40(K41((On M),(On M)))
M is epsilon-transitive non empty subset-closed Tarski universal set
L is epsilon-transitive epsilon-connected ordinal Element of M
M is epsilon-transitive epsilon-connected ordinal Element of M
L \/ M is set
M is epsilon-transitive non empty subset-closed Tarski universal set
the Element of M is Element of M
{ the Element of M} is non empty trivial 1 -element Element of M
M is epsilon-transitive non empty subset-closed Tarski universal set
M is epsilon-transitive non empty subset-closed Tarski universal set
the non empty Element of M is non empty Element of M
On M is epsilon-transitive epsilon-connected ordinal non empty set
M is Relation-like T-Sequence-like Function-like set
dom M is epsilon-transitive epsilon-connected ordinal set
rng M is set
H is set
phi is set
M . phi is set
a is epsilon-transitive epsilon-connected ordinal set
M | a is Relation-like rng M -valued T-Sequence-like Function-like set
H is Relation-like M -valued T-Sequence-like Function-like set
dom H is epsilon-transitive epsilon-connected ordinal set
rng H is Element of K40(M)
K40(M) is non empty set
phi is set
H . phi is set
a is epsilon-transitive epsilon-connected ordinal set
H | a is Relation-like M -valued rng H -valued T-Sequence-like Function-like set
rng H is set
M is epsilon-transitive non empty subset-closed Tarski universal set
L is Relation-like non-empty M -valued T-Sequence-like Function-like (M) set
Union L is set
K40(M) is non empty set
the epsilon-transitive epsilon-connected ordinal Element of M is epsilon-transitive epsilon-connected ordinal Element of M
On M is epsilon-transitive epsilon-connected ordinal non empty set
dom L is epsilon-transitive epsilon-connected ordinal set
L . the epsilon-transitive epsilon-connected ordinal Element of M is set
rng L is V51() Element of K40(M)
union (rng L) is set
union M is set
H is non empty set
phi is set
a is set
M is epsilon-transitive epsilon-connected ordinal Element of M
L . M is set
On M is epsilon-transitive epsilon-connected ordinal non empty set
dom L is epsilon-transitive epsilon-connected ordinal set
rng L is V51() Element of K40(M)
M is epsilon-transitive non empty subset-closed Tarski universal set
L is epsilon-transitive epsilon-connected ordinal Element of M
M is Relation-like non-empty M -valued T-Sequence-like Function-like (M) set
dom M is epsilon-transitive epsilon-connected ordinal set
On M is epsilon-transitive epsilon-connected ordinal non empty set
M is epsilon-transitive non empty subset-closed Tarski universal set
L is epsilon-transitive epsilon-connected ordinal Element of M
M is Relation-like non-empty M -valued T-Sequence-like Function-like (M) set
(M,M,L) is non empty Element of M
(M,M) is non empty Element of K40(M)
K40(M) is non empty set
dom M is epsilon-transitive epsilon-connected ordinal set
rng M is V51() Element of K40(M)
union (rng M) is set
K41(NAT,NAT) is Relation-like non empty V35() set
K40(K41(NAT,NAT)) is non empty V35() set
M is Relation-like NAT -defined NAT -valued Function-like quasi_total Element of K40(K41(NAT,NAT))
M . 0 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
L is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
M . L is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
5 + L is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
M is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable set
M + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
dom M is countable Element of K40(NAT)
L is Relation-like Function-like set
dom L is set
rng L is set
M is set
L . M is set
H is set
L . H is set
phi is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
M . phi is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
5 + phi is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
a is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
M . a is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
5 + a is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
M is set
H is set
M . H is set
phi is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
5 + phi is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
M is set
H is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
H is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable set
5 + H is epsilon-transitive epsilon-connected ordinal natural ext-real V16() V20() V35() cardinal countable Element of NAT
M . H is set
M is set
sup M is epsilon-transitive epsilon-connected ordinal set
On M is set
union (On M) is set
succ (union (On M)) is non empty set
{(union (On M))} is non empty trivial 1 -element set
(union (On M)) \/ {(union (On M))} is non empty set
M is epsilon-transitive non empty subset-closed Tarski universal set
L is set
sup L is epsilon-transitive epsilon-connected ordinal set
On L is set
union (On L) is set
M is epsilon-transitive epsilon-connected ordinal set
H is epsilon-transitive epsilon-connected ordinal Element of M
succ H is epsilon-transitive epsilon-connected ordinal non empty Element of M
{H} is non empty trivial 1 -element set
H \/ {H} is non empty set
M is epsilon-transitive non empty subset-closed Tarski universal set
On M is epsilon-transitive epsilon-connected ordinal non empty set
K41((On M),(On M)) is Relation-like non empty set
K40(K41((On M),(On M))) is non empty set
L is Relation-like non-empty M -valued T-Sequence-like Function-like (M) set
(M,L) is non empty Element of K40(M)
K40(M) is non empty set
rng L is V51() Element of K40(M)
union (rng L) is set
dom L is epsilon-transitive epsilon-connected ordinal set
H is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
the_scope_of H is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
bound_in H is Element of VAR
K41(VAR,(M,L)) is Relation-like non empty set
K40(K41(VAR,(M,L))) is non empty set
'not' (the_scope_of H) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(the_scope_of H)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
0-element_of M is epsilon-transitive epsilon-connected ordinal Element of M
All ((bound_in H),(the_scope_of H)) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K219((bound_in H)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,4),K219((bound_in H))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,4),K219((bound_in H))),(the_scope_of H)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Funcs (VAR,(M,L)) is non empty FUNCTION_DOMAIN of VAR ,(M,L)
f is Element of Funcs (VAR,(M,L))
a is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of Funcs (VAR,(M,L))
f is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
f is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
phi is Element of (M,L)
f / ((bound_in H),phi) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
phi is Element of (M,L)
f / ((bound_in H),phi) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
a is set
f is set
L . f is set
f is epsilon-transitive epsilon-connected ordinal set
m is epsilon-transitive epsilon-connected ordinal Element of M
L . m is set
h is Element of (M,L)
f / ((bound_in H),h) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
f is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
phi is Element of (M,L)
f / ((bound_in H),phi) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
a is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
f is Element of (M,L)
phi is epsilon-transitive epsilon-connected ordinal Element of M
L . phi is set
a / ((bound_in H),f) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
f is Relation-like Function-like set
dom f is set
a is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,a) is non empty Element of M
Funcs (VAR,(M,L,a)) is non empty FUNCTION_DOMAIN of VAR ,(M,L,a)
f .: (Funcs (VAR,(M,L,a))) is set
sup (f .: (Funcs (VAR,(M,L,a)))) is epsilon-transitive epsilon-connected ordinal set
phi is set
a is set
f . a is set
f is Element of Funcs (VAR,(M,L))
f . f is set
f is epsilon-transitive epsilon-connected ordinal Element of M
m is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
h is Element of (M,L)
(M,L,f) is non empty Element of M
m / ((bound_in H),h) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
Funcs (NAT,(M,L,a)) is non empty FUNCTION_DOMAIN of NAT ,(M,L,a)
card (Funcs (NAT,(M,L,a))) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
card M is epsilon-transitive epsilon-connected ordinal non empty cardinal set
card VAR is epsilon-transitive epsilon-connected ordinal non empty cardinal set
card NAT is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty V35() cardinal set
card (M,L,a) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
card (Funcs (VAR,(M,L,a))) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
card (f .: (Funcs (VAR,(M,L,a)))) is epsilon-transitive epsilon-connected ordinal cardinal set
phi is epsilon-transitive epsilon-connected ordinal Element of M
a is Relation-like On M -defined On M -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On M),(On M)))
a . (0-element_of M) is epsilon-transitive epsilon-connected ordinal Element of M
f is Relation-like On M -defined On M -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On M),(On M)))
f . (0-element_of M) is epsilon-transitive epsilon-connected ordinal Element of M
phi is Relation-like On M -defined On M -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On M),(On M)))
a is epsilon-transitive epsilon-connected ordinal set
dom f is epsilon-transitive epsilon-connected ordinal set
f . a is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
f . f is epsilon-transitive epsilon-connected ordinal set
dom f is epsilon-transitive epsilon-connected ordinal Element of K40((On M))
K40((On M)) is non empty set
f is epsilon-transitive epsilon-connected ordinal Element of M
f . f is epsilon-transitive epsilon-connected ordinal Element of M
h is epsilon-transitive epsilon-connected ordinal Element of M
f . h is epsilon-transitive epsilon-connected ordinal Element of M
succ h is epsilon-transitive epsilon-connected ordinal non empty Element of M
{h} is non empty trivial 1 -element set
h \/ {h} is non empty set
f . (succ h) is epsilon-transitive epsilon-connected ordinal Element of M
a . (succ h) is epsilon-transitive epsilon-connected ordinal Element of M
(M,(a . (succ h)),(f . h)) is epsilon-transitive epsilon-connected ordinal Element of M
succ (M,(a . (succ h)),(f . h)) is epsilon-transitive epsilon-connected ordinal non empty Element of M
{(M,(a . (succ h)),(f . h))} is non empty trivial 1 -element set
(M,(a . (succ h)),(f . h)) \/ {(M,(a . (succ h)),(f . h))} is non empty set
succ f is epsilon-transitive epsilon-connected ordinal non empty Element of M
{f} is non empty trivial 1 -element set
f \/ {f} is non empty set
f . (succ f) is epsilon-transitive epsilon-connected ordinal Element of M
a . (succ f) is epsilon-transitive epsilon-connected ordinal Element of M
(M,(a . (succ f)),(f . f)) is epsilon-transitive epsilon-connected ordinal Element of M
succ (M,(a . (succ f)),(f . f)) is epsilon-transitive epsilon-connected ordinal non empty Element of M
{(M,(a . (succ f)),(f . f))} is non empty trivial 1 -element set
(M,(a . (succ f)),(f . f)) \/ {(M,(a . (succ f)),(f . f))} is non empty set
h is epsilon-transitive epsilon-connected ordinal Element of M
f . h is epsilon-transitive epsilon-connected ordinal Element of M
f | h is Relation-like On M -defined h -defined On M -defined On M -valued rng f -valued T-Sequence-like Function-like Ordinal-yielding Element of K40(K41((On M),(On M)))
rng f is set
rng (f | h) is Element of K40((On M))
((f | h),M,h) is epsilon-transitive epsilon-connected ordinal Element of M
Rank h is epsilon-transitive set
(f | h) | (Rank h) is Relation-like Rank h -defined On M -defined On M -valued Function-like set
M |` ((f | h) | (Rank h)) is Relation-like On M -defined M -valued On M -valued Function-like set
Union (M |` ((f | h) | (Rank h))) is set
Union (f | h) is epsilon-transitive epsilon-connected ordinal set
union (rng (f | h)) is set
m is epsilon-transitive epsilon-connected ordinal Element of M
f . m is epsilon-transitive epsilon-connected ordinal Element of M
a is epsilon-transitive epsilon-connected ordinal set
dom f is epsilon-transitive epsilon-connected ordinal set
f . a is epsilon-transitive epsilon-connected ordinal set
f | a is Relation-like a -defined On M -defined On M -valued rng f -valued T-Sequence-like Function-like Ordinal-yielding set
rng f is set
f is epsilon-transitive epsilon-connected ordinal set
dom f is epsilon-transitive epsilon-connected ordinal Element of K40((On M))
K40((On M)) is non empty set
f | a is Relation-like On M -defined a -defined On M -defined On M -valued rng f -valued T-Sequence-like Function-like Ordinal-yielding Element of K40(K41((On M),(On M)))
dom (f | a) is epsilon-transitive epsilon-connected ordinal Element of K40(a)
K40(a) is non empty set
f is epsilon-transitive epsilon-connected ordinal Element of M
f | f is Relation-like On M -defined f -defined On M -defined On M -valued rng f -valued T-Sequence-like Function-like Ordinal-yielding Element of K40(K41((On M),(On M)))
((f | f),M,f) is epsilon-transitive epsilon-connected ordinal Element of M
Rank f is epsilon-transitive set
(f | f) | (Rank f) is Relation-like Rank f -defined On M -defined On M -valued Function-like set
M |` ((f | f) | (Rank f)) is Relation-like On M -defined M -valued On M -valued Function-like set
Union (M |` ((f | f) | (Rank f))) is set
Union (f | f) is epsilon-transitive epsilon-connected ordinal set
rng (f | f) is Element of K40((On M))
union (rng (f | f)) is set
sup (f | a) is epsilon-transitive epsilon-connected ordinal set
rng (f | a) is set
sup (rng (f | a)) is epsilon-transitive epsilon-connected ordinal set
m is epsilon-transitive epsilon-connected ordinal set
rng (f | a) is Element of K40((On M))
h is set
rng f is Element of K40((On M))
a1 is epsilon-transitive epsilon-connected ordinal set
m is epsilon-transitive epsilon-connected ordinal set
rng (f | a) is Element of K40((On M))
h is epsilon-transitive epsilon-connected ordinal set
a1 is set
(f | a) . a1 is set
m is epsilon-transitive epsilon-connected ordinal set
succ m is epsilon-transitive epsilon-connected ordinal non empty set
{m} is non empty trivial 1 -element set
m \/ {m} is non empty set
(f | a) . (succ m) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal Element of M
a . a is epsilon-transitive epsilon-connected ordinal Element of M
a | a is Relation-like On M -defined a -defined On M -defined On M -valued rng a -valued T-Sequence-like Function-like Ordinal-yielding Element of K40(K41((On M),(On M)))
rng a is set
sup (a | a) is epsilon-transitive epsilon-connected ordinal set
rng (a | a) is set
sup (rng (a | a)) is epsilon-transitive epsilon-connected ordinal set
Free ('not' (the_scope_of H)) is V35() countable Element of K40(VAR)
(M,L,a) is non empty Element of M
Funcs (VAR,(M,L,a)) is non empty FUNCTION_DOMAIN of VAR ,(M,L,a)
f .: (Funcs (VAR,(M,L,a))) is set
sup (f .: (Funcs (VAR,(M,L,a)))) is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
m is set
f . m is set
h is Element of Funcs (VAR,(M,L))
f . h is set
a1 is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,a1) is non empty Element of M
m is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
m9 is Element of (M,L)
m / ((bound_in H),m9) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
m is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
m9 is set
m . m9 is set
e is set
m . e is set
v is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,v) is non empty Element of M
v is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,v) is non empty Element of M
L | a is Relation-like M -valued rng L -valued T-Sequence-like Function-like set
rng L is V51() set
Union (L | a) is set
rng (L | a) is Element of K40(M)
union (rng (L | a)) is set
m9 is set
m . m9 is set
e is set
m . e is set
v is set
m . v is set
v is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,v) is non empty Element of M
m9 is set
m . m9 is set
dom (L | a) is epsilon-transitive epsilon-connected ordinal set
e is Element of VAR
m . e is Element of (M,L)
rng m is Element of K40((M,L))
K40((M,L)) is non empty set
v is Relation-like Function-like set
dom v is set
rng v is set
v is Relation-like Function-like set
dom v is set
rng v is set
v is set
v is set
(L | a) . v is set
L . v is set
v9 is epsilon-transitive epsilon-connected ordinal set
a2 is epsilon-transitive epsilon-connected ordinal Element of M
f9 is epsilon-transitive epsilon-connected ordinal Element of M
m is Element of VAR
m . m is Element of (M,L)
(M,L,f9) is non empty Element of M
m9 is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,m9) is non empty Element of M
e is Element of VAR
m . e is Element of (M,L)
m9 is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,m9) is non empty Element of M
e is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,e) is non empty Element of M
m9 is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,m9) is non empty Element of M
a . m9 is epsilon-transitive epsilon-connected ordinal Element of M
Funcs (VAR,(M,L,m9)) is non empty FUNCTION_DOMAIN of VAR ,(M,L,m9)
f .: (Funcs (VAR,(M,L,m9))) is set
sup (f .: (Funcs (VAR,(M,L,m9)))) is epsilon-transitive epsilon-connected ordinal set
dom a is epsilon-transitive epsilon-connected ordinal Element of K40((On M))
K40((On M)) is non empty set
dom (a | a) is epsilon-transitive epsilon-connected ordinal Element of K40(a)
K40(a) is non empty set
(dom a) /\ a is Element of K40((On M))
(a | a) . m9 is epsilon-transitive epsilon-connected ordinal set
rng (a | a) is Element of K40((On M))
the Element of (M,L,m9) is Element of (M,L,m9)
v is Relation-like Function-like set
dom v is set
rng v is set
v is set
v9 is set
v . v9 is set
a2 is Element of VAR
m . a2 is Element of (M,L)
K41(VAR,(M,L,m9)) is Relation-like non empty set
K40(K41(VAR,(M,L,m9))) is non empty set
v is Relation-like VAR -defined (M,L,m9) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L,m9)))
v9 is Element of Funcs (VAR,(M,L))
f . v9 is set
a2 is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,a2) is non empty Element of M
f9 is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
m is Element of (M,L)
f9 / ((bound_in H),m) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
f9 is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
(M,L) ! v is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
m is Element of (M,L)
m / ((bound_in H),m) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
(m / ((bound_in H),m)) . (bound_in H) is Element of (M,L)
x1 is Element of VAR
(m / ((bound_in H),m)) . x1 is Element of (M,L)
m . x1 is Element of (M,L)
((M,L) ! v) / ((bound_in H),m) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
(((M,L) ! v) / ((bound_in H),m)) . x1 is Element of (M,L)
((M,L) ! v) . x1 is Element of (M,L)
x1 is Element of (M,L)
f9 / ((bound_in H),x1) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
x1 is Element of (M,L)
f9 / ((bound_in H),x1) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
m / ((bound_in H),x1) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
(m / ((bound_in H),x1)) . (bound_in H) is Element of (M,L)
x1 is Element of VAR
(m / ((bound_in H),x1)) . x1 is Element of (M,L)
m . x1 is Element of (M,L)
((M,L) ! v) / ((bound_in H),x1) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
(((M,L) ! v) / ((bound_in H),x1)) . x1 is Element of (M,L)
((M,L) ! v) . x1 is Element of (M,L)
(f9 / ((bound_in H),x1)) . x1 is Element of (M,L)
m is Element of (M,L)
m / ((bound_in H),m) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
(m / ((bound_in H),m)) . (bound_in H) is Element of (M,L)
x1 is Element of VAR
(m / ((bound_in H),m)) . x1 is Element of (M,L)
m . x1 is Element of (M,L)
((M,L) ! v) / ((bound_in H),m) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
(((M,L) ! v) / ((bound_in H),m)) . x1 is Element of (M,L)
((M,L) ! v) . x1 is Element of (M,L)
m is Element of (M,L)
m / ((bound_in H),m) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
x1 is Element of (M,L)
f9 / ((bound_in H),x1) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
m is Element of (M,L)
m / ((bound_in H),m) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
x1 is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
x1 is Element of (M,L)
x1 / ((bound_in H),x1) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
a is epsilon-transitive epsilon-connected ordinal Element of M
a . a is epsilon-transitive epsilon-connected ordinal set
f . a is epsilon-transitive epsilon-connected ordinal set
a . a is epsilon-transitive epsilon-connected ordinal Element of M
f . a is epsilon-transitive epsilon-connected ordinal Element of M
a | a is Relation-like On M -defined a -defined On M -defined On M -valued rng a -valued T-Sequence-like Function-like Ordinal-yielding Element of K40(K41((On M),(On M)))
rng a is set
sup (a | a) is epsilon-transitive epsilon-connected ordinal set
rng (a | a) is set
sup (rng (a | a)) is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
rng (a | a) is Element of K40((On M))
K40((On M)) is non empty set
f is epsilon-transitive epsilon-connected ordinal set
dom (a | a) is epsilon-transitive epsilon-connected ordinal Element of K40(a)
K40(a) is non empty set
m is set
(a | a) . m is set
h is epsilon-transitive epsilon-connected ordinal set
dom a is epsilon-transitive epsilon-connected ordinal Element of K40((On M))
a1 is epsilon-transitive epsilon-connected ordinal Element of M
a . a1 is epsilon-transitive epsilon-connected ordinal Element of M
f . a1 is epsilon-transitive epsilon-connected ordinal Element of M
dom f is epsilon-transitive epsilon-connected ordinal Element of K40((On M))
a is epsilon-transitive epsilon-connected ordinal Element of M
a . a is epsilon-transitive epsilon-connected ordinal set
f . a is epsilon-transitive epsilon-connected ordinal set
succ a is epsilon-transitive epsilon-connected ordinal non empty Element of M
{a} is non empty trivial 1 -element set
a \/ {a} is non empty set
a . (succ a) is epsilon-transitive epsilon-connected ordinal set
f . (succ a) is epsilon-transitive epsilon-connected ordinal set
a . a is epsilon-transitive epsilon-connected ordinal Element of M
f . a is epsilon-transitive epsilon-connected ordinal Element of M
f . (succ a) is epsilon-transitive epsilon-connected ordinal Element of M
a . (succ a) is epsilon-transitive epsilon-connected ordinal Element of M
(M,(a . (succ a)),(f . a)) is epsilon-transitive epsilon-connected ordinal Element of M
succ (M,(a . (succ a)),(f . a)) is epsilon-transitive epsilon-connected ordinal non empty Element of M
{(M,(a . (succ a)),(f . a))} is non empty trivial 1 -element set
(M,(a . (succ a)),(f . a)) \/ {(M,(a . (succ a)),(f . a))} is non empty set
a . (0-element_of M) is epsilon-transitive epsilon-connected ordinal set
f . (0-element_of M) is epsilon-transitive epsilon-connected ordinal set
Free (the_scope_of H) is V35() countable Element of K40(VAR)
phi * f is Relation-like On M -defined On M -defined On M -valued On M -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On M),(On M)))
a is Relation-like On M -defined On M -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On M),(On M)))
f is Relation-like T-Sequence-like Function-like Ordinal-yielding set
f is epsilon-transitive epsilon-connected ordinal Element of M
a . f is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,f) is non empty Element of M
K41(VAR,(M,L,f)) is Relation-like non empty set
K40(K41(VAR,(M,L,f))) is non empty set
f is Relation-like VAR -defined (M,L,f) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L,f)))
(M,L) ! f is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
dom a is epsilon-transitive epsilon-connected ordinal Element of K40((On M))
K40((On M)) is non empty set
f . f is epsilon-transitive epsilon-connected ordinal Element of M
phi . (f . f) is epsilon-transitive epsilon-connected ordinal Element of M
dom f is epsilon-transitive epsilon-connected ordinal Element of K40((On M))
dom phi is epsilon-transitive epsilon-connected ordinal Element of K40((On M))
phi . f is epsilon-transitive epsilon-connected ordinal Element of M
m is Relation-like VAR -defined (M,L,f) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L,f)))
(M,L) ! m is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
h is Element of VAR
((M,L) ! m) . h is Element of (M,L)
((M,L) ! f) . h is Element of (M,L)
m is Element of (M,L)
((M,L) ! f) / ((bound_in H),m) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
a . f is epsilon-transitive epsilon-connected ordinal Element of M
Funcs (VAR,(M,L,f)) is non empty FUNCTION_DOMAIN of VAR ,(M,L,f)
f .: (Funcs (VAR,(M,L,f))) is set
sup (f .: (Funcs (VAR,(M,L,f)))) is epsilon-transitive epsilon-connected ordinal set
h is Element of Funcs (VAR,(M,L))
f . h is set
a1 is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,a1) is non empty Element of M
m is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
m9 is Element of (M,L)
m / ((bound_in H),m9) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
m is Element of (M,L)
((M,L) ! f) / ((bound_in H),m) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
m9 is Element of (M,L,f)
f / ((bound_in H),m9) is Relation-like VAR -defined (M,L,f) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L,f)))
(M,L) ! (f / ((bound_in H),m9)) is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
a is epsilon-transitive epsilon-connected ordinal Element of M
phi . a is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,a) is non empty Element of M
K41(VAR,(M,L,a)) is Relation-like non empty set
K40(K41(VAR,(M,L,a))) is non empty set
f is Relation-like VAR -defined (M,L,a) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L,a)))
(M,L) ! f is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
f is Element of VAR
((M,L) ! f) . f is Element of (M,L)
f is Element of VAR
f . f is Element of (M,L,a)
a is Relation-like On M -defined On M -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On M),(On M)))
f is Relation-like On M -defined On M -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On M),(On M)))
H is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
the_left_argument_of H is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
the_right_argument_of H is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
(the_left_argument_of H) '&' (the_right_argument_of H) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,3),(the_left_argument_of H)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,3),(the_left_argument_of H)),(the_right_argument_of H)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
phi is Relation-like On M -defined On M -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On M),(On M)))
a is Relation-like On M -defined On M -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On M),(On M)))
a * phi is Relation-like On M -defined On M -defined On M -valued On M -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On M),(On M)))
f is Relation-like On M -defined On M -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On M),(On M)))
a is Relation-like T-Sequence-like Function-like Ordinal-yielding set
a is epsilon-transitive epsilon-connected ordinal Element of M
f . a is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,a) is non empty Element of M
K41(VAR,(M,L,a)) is Relation-like non empty set
K40(K41(VAR,(M,L,a))) is non empty set
dom phi is epsilon-transitive epsilon-connected ordinal Element of K40((On M))
K40((On M)) is non empty set
phi . a is epsilon-transitive epsilon-connected ordinal Element of M
f is Relation-like VAR -defined (M,L,a) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L,a)))
(M,L) ! f is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
K41(VAR,(M,L)) is Relation-like non empty set
K40(K41(VAR,(M,L))) is non empty set
dom f is epsilon-transitive epsilon-connected ordinal Element of K40((On M))
dom a is epsilon-transitive epsilon-connected ordinal Element of K40((On M))
a . (phi . a) is epsilon-transitive epsilon-connected ordinal Element of M
a . a is epsilon-transitive epsilon-connected ordinal Element of M
id (On M) is Relation-like On M -defined On M -valued non empty Function-like one-to-one set
dom (id (On M)) is non empty Element of K40((On M))
K40((On M)) is non empty set
rng (id (On M)) is non empty Element of K40((On M))
H is Relation-like T-Sequence-like Function-like set
phi is Relation-like T-Sequence-like Function-like Ordinal-yielding set
f is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
a is Relation-like On M -defined On M -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On M),(On M)))
a is epsilon-transitive epsilon-connected ordinal set
dom a is epsilon-transitive epsilon-connected ordinal set
a . a is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
a . f is epsilon-transitive epsilon-connected ordinal set
dom a is epsilon-transitive epsilon-connected ordinal Element of K40((On M))
a is epsilon-transitive epsilon-connected ordinal set
dom a is epsilon-transitive epsilon-connected ordinal set
a . a is epsilon-transitive epsilon-connected ordinal set
a | a is Relation-like a -defined On M -defined On M -valued rng a -valued T-Sequence-like Function-like Ordinal-yielding set
rng a is set
f is epsilon-transitive epsilon-connected ordinal set
dom a is epsilon-transitive epsilon-connected ordinal Element of K40((On M))
a | a is Relation-like On M -defined a -defined On M -defined On M -valued rng a -valued T-Sequence-like Function-like Ordinal-yielding Element of K40(K41((On M),(On M)))
id a is Relation-like a -defined a -valued Function-like one-to-one set
(id a) * a is Relation-like a -defined On M -valued Function-like set
(dom a) /\ a is Element of K40((On M))
id ((dom a) /\ a) is Relation-like (dom a) /\ a -defined (dom a) /\ a -valued Function-like one-to-one set
rng (a | a) is Element of K40((On M))
sup (a | a) is epsilon-transitive epsilon-connected ordinal set
rng (a | a) is set
sup (rng (a | a)) is epsilon-transitive epsilon-connected ordinal set
dom (a | a) is epsilon-transitive epsilon-connected ordinal Element of K40(a)
K40(a) is non empty set
a is epsilon-transitive epsilon-connected ordinal Element of M
a . a is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,a) is non empty Element of M
K41(VAR,(M,L,a)) is Relation-like non empty set
K40(K41(VAR,(M,L,a))) is non empty set
f is Relation-like VAR -defined (M,L,a) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L,a)))
(M,L) ! f is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
K41(VAR,(M,L)) is Relation-like non empty set
K40(K41(VAR,(M,L))) is non empty set
Var1 f is Element of VAR
Var2 f is Element of VAR
(Var1 f) 'in' (Var2 f) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K219((Var1 f)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,1),K219((Var1 f))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K219((Var2 f)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((Var1 f))),K219((Var2 f))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
((M,L) ! f) . (Var1 f) is Element of (M,L)
((M,L) ! f) . (Var2 f) is Element of (M,L)
(Var1 f) '=' (Var2 f) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,0),K219((Var1 f))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,0),K219((Var1 f))),K219((Var2 f))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
Var1 f is Element of VAR
Var2 f is Element of VAR
(Var1 f) 'in' (Var2 f) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K219((Var1 f)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K210(NAT,1),K219((Var1 f))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K219((Var2 f)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,1),K219((Var1 f))),K219((Var2 f))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
f . (Var1 f) is Element of (M,L,a)
f . (Var2 f) is Element of (M,L,a)
(Var1 f) '=' (Var2 f) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,0),K219((Var1 f))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
K206(NAT,K206(NAT,K210(NAT,0),K219((Var1 f))),K219((Var2 f))) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
H is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
the_argument_of H is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
'not' (the_argument_of H) is Relation-like NAT -defined NAT -valued Function-like V55() ZF-formula-like M8( NAT )
K206(NAT,K210(NAT,2),(the_argument_of H)) is Relation-like NAT -defined NAT -valued Function-like V55() M8( NAT )
phi is Relation-like On M -defined On M -valued T-Sequence-like Function-like quasi_total Ordinal-yielding Element of K40(K41((On M),(On M)))
a is epsilon-transitive epsilon-connected ordinal Element of M
phi . a is epsilon-transitive epsilon-connected ordinal Element of M
(M,L,a) is non empty Element of M
K41(VAR,(M,L,a)) is Relation-like non empty set
K40(K41(VAR,(M,L,a))) is non empty set
f is Relation-like VAR -defined (M,L,a) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L,a)))
(M,L) ! f is Relation-like VAR -defined (M,L) -valued Function-like quasi_total Element of K40(K41(VAR,(M,L)))
K41(VAR,(M,L)) is Relation-like non empty set
K40(K41(VAR,(M,L))) is non empty set
M is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty V35() cardinal non countable set
Rank M is epsilon-transitive non empty set