K115() is set
K119() is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool K115()
bool K115() is set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
bool omega is non empty non trivial non finite set
bool K119() is non empty non trivial non finite set
{} is V6() V9() empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element complex set
the V6() V9() empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element complex set is V6() V9() empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element complex set
1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex Element of K119()
{{}} is non empty trivial finite V36() 1 -element set
2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex Element of K119()
{{},1} is non empty finite V36() set
({}) is () ()
S is () ()
the of S is set
({{}}) is () ()
the of ({{}}) is set
S is () ()
the of S is set
S is () ()
the of S is set
S is ()
the of S is set
bool the of S is set
{} the of S is Element of bool the of S
[#] the of S is Element of bool the of S
S is ()
(S) is Element of bool the of S
the of S is set
bool the of S is set
S is () ()
(S) is V9() c=-linear finite V36() Element of bool the of S
the of S is V6() V9() empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element complex set
bool the of S is finite V36() set
S is () ()
(S) is Element of bool the of S
the of S is non empty set
bool the of S is set
S is () ()
the of S is non empty set
bool the of S is set
(S) is non empty Element of bool the of S
S is ()
the of S is set
id the of S is Relation-like the of S -defined the of S -valued V6() V7() total V18( the of S, the of S) Element of bool [: the of S, the of S:]
[: the of S, the of S:] is set
bool [: the of S, the of S:] is set
the non empty set is non empty set
the Element of the non empty set is Element of the non empty set
( the non empty set , the Element of the non empty set ) is () ()
the of ( the non empty set , the Element of the non empty set ) is set
S is ()
the of S is Element of the of S
the of S is set
S is ()
the of S is Element of the of S
the of S is set
S is ()
the of S is set
S is ()
S is ()
the of S is set
y is Element of the of S
A is Element of the of S
y is set
A is set
y is Element of the of S
A is Element of the of S
y is Element of the of S
A is Element of the of S
S is ()
(S) is Element of the of S
the of S is set
the of S is Element of the of S
(S) is Element of the of S
the of S is Element of the of S
(1) is () ()
(2) is () ()
S is () ()
the of S is set
X is Element of the of S
y is Element of the of S
S is () () ()
the of S is non empty set
S is () ()
the of S is set
({{}}) is () ()
S is () ()
the of S is set
S is () () ()
the of S is V6() V9() empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element complex set
the non empty non trivial non finite set is non empty non trivial non finite set
( the non empty non trivial non finite set ) is () ()
S is () ()
the of S is set
S is () ()
the of S is set
S is () ()
S is ()
the of S is set
X is trivial finite set
S is ()
S is ()
the of S is set
S is ()
(S) is Element of the of S
the of S is set
the of S is Element of the of S
In ({},2) is epsilon-transitive epsilon-connected ordinal Element of 2
In (1,2) is epsilon-transitive epsilon-connected ordinal Element of 2
(2,(In ({},2)),(In (1,2))) is () ()
S is () ()
(S) is (S) Element of the of S
the of S is set
the of S is Element of the of S
(S) is Element of the of S
the of S is Element of the of S
S is () () () ()
(S) is Element of the of S
the of S is non empty non trivial set
the of S is Element of the of S
(S) is (S) Element of the of S
the of S is Element of the of S
S is ()
the of S is set
(S) is Element of bool the of S
bool the of S is set
({},{}) is () ()
S is () ()
the of S is set
the of S is set
S is () ()
the of S is set
(1,1) is () ()
S is () ()
the of S is set
the of S is set
S is () ()
the of S is set
X is () ()
the of X is non empty set
S is ()
the of S is set
y is Element of the of X
the of S --> y is Relation-like the of S -defined the of X -valued V6() total V18( the of S, the of X) Element of bool [: the of S, the of X:]
[: the of S, the of X:] is set
bool [: the of S, the of X:] is set
S is ()
the of S is set
(S) is (S) Element of the of S
the of S is Element of the of S
In ({},2) is epsilon-transitive epsilon-connected ordinal Element of 2
(2,(In ({},2))) is () ()
S is () () ()
the of S is non empty non trivial set
X is Element of the of S
y is Element of the of S
(S) is (S) Element of the of S
the of S is Element of the of S
(S) is (S) Element of the of S
the of S is Element of the of S
(S) is (S) Element of the of S
the of S is Element of the of S
S is set
X is ()
the of X is set
[:S, the of X:] is set
bool [:S, the of X:] is set
S is ()
the of S is set
card the of S is epsilon-transitive epsilon-connected ordinal cardinal set
S is ()
the of S is set
(S) is non proper Element of bool the of S
bool the of S is set
(S) is (S) Element of the of S
the of S is Element of the of S
{(S)} is non empty trivial finite 1 -element set
(S) \ {(S)} is Element of bool the of S
S is () ()
the of S is non empty set
(S) is Element of bool the of S
bool the of S is set
(S) is non empty non proper Element of bool the of S
(S) is (S) Element of the of S
the of S is Element of the of S
{(S)} is non empty trivial finite 1 -element set
(S) \ {(S)} is Element of bool the of S
X is Element of the of S
S is () ()
the of S is non empty set
(S) is (S) Element of the of S
the of S is Element of the of S
X is Element of the of S
X is Element of the of S
y is Element of the of S
S is () () ()
(S) is Element of bool the of S
the of S is non empty non trivial set
bool the of S is set
(S) is non empty non proper Element of bool the of S
(S) is (S) Element of the of S
the of S is Element of the of S
{(S)} is non empty trivial finite 1 -element set
(S) \ {(S)} is Element of bool the of S
X is Element of the of S
In ({},1) is epsilon-transitive epsilon-connected ordinal Element of 1
(1,(In ({},1))) is () ()
S is () () () ()
(S) is finite Element of bool the of S
the of S is non empty trivial finite 1 -element set
bool the of S is finite V36() set
(S) is non empty non proper finite Element of bool the of S
(S) is (S) Element of the of S
the of S is Element of the of S
{(S)} is non empty trivial finite 1 -element set
(S) \ {(S)} is finite Element of bool the of S
X is Element of the of S
{(S)} is non empty trivial finite 1 -element Element of bool the of S
S is () ()
the of S is non empty set
bool the of S is set
the Element of the of S is Element of the of S
{ the Element of the of S} is non empty trivial finite 1 -element Element of bool the of S
S is () () () ()
(S) is (S) Element of the of S
the of S is non empty non trivial set
the of S is Element of the of S
(S) is non empty Element of bool the of S
bool the of S is set
(S) is non empty non proper Element of bool the of S
(S) is (S) Element of the of S
the of S is Element of the of S
{(S)} is non empty trivial finite 1 -element set
(S) \ {(S)} is Element of bool the of S
{(S)} is non empty trivial finite 1 -element Element of bool the of S
S is () ()
(S) is epsilon-transitive epsilon-connected ordinal cardinal set
the of S is finite set
card the of S is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex set
S is () () ()
(S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex set
the of S is non empty finite set
card the of S is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex set
X is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex set
S is () () ()
the of S is non empty non trivial set
bool the of S is set
X is Element of the of S
y is Element of the of S
{X,y} is non empty finite Element of bool the of S
A is Element of bool the of S
S is ()
(S) is (S) Element of the of S
the of S is set
the of S is Element of the of S
(S) is Element of bool the of S
bool the of S is set
(S) is non proper Element of bool the of S
{(S)} is non empty trivial finite 1 -element set
(S) \ {(S)} is Element of bool the of S
S is () ()
the of S is non empty set
(S) is (S) Element of the of S
the of S is Element of the of S
{(S)} is non empty trivial finite 1 -element Element of bool the of S
bool the of S is set
(S) is Element of bool the of S
(S) is non empty non proper Element of bool the of S
{(S)} is non empty trivial finite 1 -element set
(S) \ {(S)} is Element of bool the of S
{(S)} \/ (S) is non empty Element of bool the of S
S is epsilon-transitive epsilon-connected ordinal cardinal set
the S -element set is S -element set
( the S -element set ) is () ()
X is () ()
the of X is set
S is epsilon-transitive epsilon-connected ordinal cardinal set
X is (S) ()
the of X is set
S is ()
the of S is set
S is ()
the of S is set
S is ()
the of S is set
S is ()
the of S is set
S is ()
the of S is set
S is ()
the of S is set
S is ()
the of S is set
the of S is set
S is ()
(1,1) is () ()
S is () ()
the of S is set
S is () ()
the of S is set
(1,{{},1}) is () ()
S is () ()
S is () ()
the of S is set
S is ()
the of S is set
S is ()