K28() is V32() V33() V34() V38() set
K32() is non empty epsilon-transitive epsilon-connected ordinal V32() V33() V34() V35() V36() V37() V38() Element of K6(K28())
K6(K28()) is set
omega is non empty epsilon-transitive epsilon-connected ordinal V32() V33() V34() V35() V36() V37() V38() set
K6(omega) is set
K6(K32()) is set
VAR is non empty V32() V33() V34() V35() V36() V37() Element of K6(K32())
K6(VAR) is set
5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() V32() V33() V34() V35() V36() V37() Element of K32()
the_axiom_of_extensionality is Relation-like K32() -defined K32() -valued Function-like V47() ZF-formula-like M7(K32())
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Function-like functional V32() V33() V34() V35() V36() V37() V38() Element of K32()
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional V32() V33() V34() V35() V36() V37() V38() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional V32() V33() V34() V35() V36() V37() V38() set
x. 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() Element of VAR
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() V32() V33() V34() V35() V36() V37() Element of K32()
x. 1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() Element of VAR
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() V32() V33() V34() V35() V36() V37() Element of K32()
x. 2 is epsilon-transitive epsilon-connected ordinal natural V11() V12() Element of VAR
(x. 2) 'in' (x. 0) is Relation-like K32() -defined K32() -valued Function-like V47() ZF-formula-like M7(K32())
(x. 2) 'in' (x. 1) is Relation-like K32() -defined K32() -valued Function-like V47() ZF-formula-like M7(K32())
((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)) is Relation-like K32() -defined K32() -valued Function-like V47() ZF-formula-like M7(K32())
All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) is Relation-like K32() -defined K32() -valued Function-like V47() ZF-formula-like M7(K32())
(x. 0) '=' (x. 1) is Relation-like K32() -defined K32() -valued Function-like V47() ZF-formula-like M7(K32())
(All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)) is Relation-like K32() -defined K32() -valued Function-like V47() ZF-formula-like M7(K32())
All ((x. 0),(x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))) is Relation-like K32() -defined K32() -valued Function-like V47() ZF-formula-like M7(K32())
E is non empty set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in dom a1 & b2 in union {(a1 . b3)} ) ) } is set
f is epsilon-transitive epsilon-connected ordinal set
X is T-Sequence-like Relation-like Function-like set
dom X is epsilon-transitive epsilon-connected ordinal set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in dom X & b2 in union {(X . b3)} ) ) } is set
a is set
b is epsilon-transitive epsilon-connected ordinal set
X . b is set
X | b is T-Sequence-like Relation-like rng X -valued Function-like set
rng X is set
dom (X | b) is epsilon-transitive epsilon-connected ordinal set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in dom (X | b) & b2 in union {((X | b) . b3)} ) ) } is set
X is set
a is set
b is T-Sequence-like Relation-like Function-like set
dom b is epsilon-transitive epsilon-connected ordinal set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in dom b & b2 in union {(b . b3)} ) ) } is set
d2 is epsilon-transitive epsilon-connected ordinal set
Z is T-Sequence-like Relation-like Function-like set
b | d2 is T-Sequence-like Relation-like rng b -valued Function-like set
rng b is set
b . d2 is set
dom Z is epsilon-transitive epsilon-connected ordinal set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in dom Z & b2 in union {(Z . b3)} ) ) } is set
d2 is T-Sequence-like Relation-like Function-like set
dom d2 is epsilon-transitive epsilon-connected ordinal set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in dom d2 & b2 in union {(d2 . b3)} ) ) } is set
Z is epsilon-transitive epsilon-connected ordinal set
c is T-Sequence-like Relation-like Function-like set
d2 | Z is T-Sequence-like Relation-like rng d2 -valued Function-like set
rng d2 is set
d2 . Z is set
dom c is epsilon-transitive epsilon-connected ordinal set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in dom c & b2 in union {(c . b3)} ) ) } is set
E is non empty set
f is epsilon-transitive epsilon-connected ordinal set
(E,f) is set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in f & b2 in (E,b3) ) ) } is set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in dom a1 & b2 in union {(a1 . b3)} ) ) } is set
X is set
a is epsilon-transitive epsilon-connected ordinal set
(E,a) is set
X is Relation-like Function-like set
dom X is set
b is epsilon-transitive epsilon-connected ordinal set
a is T-Sequence-like Relation-like Function-like set
dom a is epsilon-transitive epsilon-connected ordinal set
a . b is set
(E,b) is set
d2 is epsilon-transitive epsilon-connected ordinal set
(E,d2) is set
d2 is set
b is epsilon-transitive epsilon-connected ordinal set
(E,b) is set
c is set
A is T-Sequence-like Relation-like Function-like set
dom A is epsilon-transitive epsilon-connected ordinal set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in dom A & b2 in union {(A . b3)} ) ) } is set
Z is epsilon-transitive epsilon-connected ordinal set
(E,Z) is set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in dom a & b2 in union {(a . b3)} ) ) } is set
b is set
d2 is Element of E
Z is Element of E
c is epsilon-transitive epsilon-connected ordinal set
a . c is set
{(a . c)} is non empty set
union {(a . c)} is set
(E,c) is set
b is set
d2 is Element of E
Z is Element of E
c is epsilon-transitive epsilon-connected ordinal set
(E,c) is set
a . c is set
{(a . c)} is non empty set
union {(a . c)} is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional V32() V33() V34() V35() V36() V37() V38() set
E is non empty set
(E,{}) is set
f is Element of E
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in {} & b2 in (E,b3) ) ) } is set
X is Element of E
X is Element of E
a is Element of E
a is epsilon-transitive epsilon-connected ordinal set
(E,a) is set
E is non empty set
f is epsilon-transitive epsilon-connected ordinal set
(E,f) is set
succ f is non empty epsilon-transitive epsilon-connected ordinal set
{f} is non empty set
f \/ {f} is non empty set
(E,(succ f)) is set
X is Element of E
X /\ E is set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in succ f & b2 in (E,b3) ) ) } is set
a is Element of E
a is set
b is Element of E
d2 is Element of E
d2 is epsilon-transitive epsilon-connected ordinal set
(E,d2) is set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in d2 & b2 in (E,b3) ) ) } is set
Z is Element of E
c is Element of E
c is epsilon-transitive epsilon-connected ordinal set
(E,c) is set
A is epsilon-transitive epsilon-connected ordinal set
(E,A) is set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in f & b2 in (E,b3) ) ) } is set
E is non empty set
f is epsilon-transitive epsilon-connected ordinal set
(E,f) is set
X is epsilon-transitive epsilon-connected ordinal set
(E,X) is set
a is set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in f & b2 in (E,b3) ) ) } is set
b is Element of E
d2 is Element of E
Z is epsilon-transitive epsilon-connected ordinal set
(E,Z) is set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in X & b2 in (E,b3) ) ) } is set
E is non empty set
f is Element of E
X is set
a is set
b is set
Z is set
d2 is Element of E
d2 /\ E is set
c is epsilon-transitive epsilon-connected ordinal set
(E,c) is set
Z is Relation-like Function-like set
dom Z is set
rng Z is set
c is set
A is set
Z . A is set
d1 is epsilon-transitive epsilon-connected ordinal set
(E,d1) is set
c is epsilon-transitive epsilon-connected ordinal set
A is Element of E
Z . A is set
d1 is epsilon-transitive epsilon-connected ordinal set
(E,d1) is set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in c & b2 in (E,b3) ) ) } is set
(E,c) is set
E is non empty set
f is epsilon-transitive epsilon-connected ordinal set
(E,f) is set
X is Element of E
a is Element of E
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in f & b2 in (E,b3) ) ) } is set
b is Element of E
b is epsilon-transitive epsilon-connected ordinal set
(E,b) is set
E is non empty set
f is epsilon-transitive epsilon-connected ordinal set
(E,f) is set
X is set
{ b1 where b1 is Element of E : for b2 being Element of E holds
( not b2 in b1 or ex b3 being epsilon-transitive epsilon-connected ordinal set st
( b3 in f & b2 in (E,b3) ) ) } is set
a is Element of E
E is non empty set
f is set
X is Element of E
a is epsilon-transitive epsilon-connected ordinal set
(E,a) is set
f is Relation-like Function-like set
dom f is set
rng f is set
X is set
a is set
f . a is set
b is epsilon-transitive epsilon-connected ordinal set
(E,b) is set
X is epsilon-transitive epsilon-connected ordinal set
(E,X) is set
a is set
f . a is set
b is epsilon-transitive epsilon-connected ordinal set
(E,b) is set
E is non empty set
f is epsilon-transitive epsilon-connected ordinal set
(E,f) is set
X is epsilon-transitive epsilon-connected ordinal set
(E,X) is set
a is Relation-like Function-like set
dom a is set
a | (E,f) is Relation-like Function-like set
dom (a | (E,f)) is set
b is Element of E
(a | (E,f)) . b is set
(a | (E,f)) .: b is set
a .: b is set
d2 is set
Z is set
a . Z is set
c is Element of E
(a | (E,f)) . Z is set
a . b is set
f is epsilon-transitive epsilon-connected ordinal set
(E,f) is set
X is Relation-like Function-like set
dom X is set
a is Relation-like Function-like set
dom a is set
b is set
d2 is Element of E
X .: d2 is set
a .: d2 is set
Z is set
c is set
X . c is set
A is Element of E
d1 is epsilon-transitive epsilon-connected ordinal set
(E,d1) is set
X | (E,d1) is Relation-like Function-like set
dom (X | (E,d1)) is set
a | (E,d1) is Relation-like Function-like set
dom (a | (E,d1)) is set
d2 is Element of E
(X | (E,d1)) . d2 is set
(X | (E,d1)) .: d2 is set
w is Element of E
(a | (E,d1)) . w is set
(a | (E,d1)) .: w is set
X . A is set
(X | (E,d1)) . A is set
a . A is set
Z is set
c is set
a . c is set
A is Element of E
d1 is epsilon-transitive epsilon-connected ordinal set
(E,d1) is set
X | (E,d1) is Relation-like Function-like set
dom (X | (E,d1)) is set
a | (E,d1) is Relation-like Function-like set
dom (a | (E,d1)) is set
d2 is Element of E
(X | (E,d1)) . d2 is set
(X | (E,d1)) .: d2 is set
w is Element of E
(a | (E,d1)) . w is set
(a | (E,d1)) .: w is set
X . A is set
(X | (E,d1)) . A is set
a . A is set
X . d2 is set
X . b is set
a . b is set
f is epsilon-transitive epsilon-connected ordinal set
(E,f) is set
X is set
b is set
d2 is set
Z is set
c is epsilon-transitive epsilon-connected ordinal set
(E,c) is set
A is Relation-like Function-like set
dom A is set
A . b is set
d1 is epsilon-transitive epsilon-connected ordinal set
(E,d1) is set
d2 is Relation-like Function-like set
dom d2 is set
d2 . b is set
A | (E,d1) is Relation-like Function-like set
dom (A | (E,d1)) is set
w is Element of E
(A | (E,d1)) . w is set
(A | (E,d1)) .: w is set
d2 | (E,c) is Relation-like Function-like set
dom (d2 | (E,c)) is set
w is Element of E
(d2 | (E,c)) . w is set
(d2 | (E,c)) .: w is set
a is Element of E
b is set
d2 is set
Z is set
c is set
A is epsilon-transitive epsilon-connected ordinal set
(E,A) is set
d1 is Relation-like Function-like set
dom d1 is set
d1 . c is set
A is epsilon-transitive epsilon-connected ordinal set
(E,A) is set
d1 is Relation-like Function-like set
dom d1 is set
d1 . c is set
d2 is Element of E
d1 . d2 is set
w is Element of E
d1 . w is set
d1 .: w is set
c is Element of E
A is epsilon-transitive epsilon-connected ordinal set
(E,A) is set
d1 is Relation-like Function-like set
dom d1 is set
d1 . c is set
X is Relation-like Function-like set
dom X is set
a is epsilon-transitive epsilon-connected ordinal set
(E,a) is set
X | (E,a) is Relation-like Function-like set
dom (X | (E,a)) is set
b is Element of E
(X | (E,a)) . b is set
(X | (E,a)) .: b is set
X . b is set
d2 is Element of E
c is set
A is Element of E
d1 is epsilon-transitive epsilon-connected ordinal set
(E,d1) is set
d2 is Relation-like Function-like set
dom d2 is set
d2 . A is set
w is epsilon-transitive epsilon-connected ordinal set
(E,w) is set
A1 is epsilon-transitive epsilon-connected ordinal set
(E,A1) is set
a is Relation-like Function-like set
dom a is set
a . A is set
X | (E,A1) is Relation-like Function-like set
dom (X | (E,A1)) is set
v is Element of E
(X | (E,A1)) . v is set
(X | (E,A1)) .: v is set
(X | (E,a)) | (E,A1) is Relation-like Function-like set
(X | (E,a)) . A is set
d2 | (E,w) is Relation-like Function-like set
dom (d2 | (E,w)) is set
A1 is Element of E
(d2 | (E,w)) . A1 is set
(d2 | (E,w)) .: A1 is set
(d2 | (E,w)) . A is set
c is set
A is set
(X | (E,a)) . A is set
d1 is Element of E
d2 is epsilon-transitive epsilon-connected ordinal set
(E,d2) is set
(X | (E,a)) | (E,d2) is Relation-like Function-like set
X | (E,d2) is Relation-like Function-like set
(X | (E,d2)) . A is set
dom (X | (E,d2)) is set
w is Element of E
(X | (E,d2)) . w is set
(X | (E,d2)) .: w is set
X | (dom X) is Relation-like Function-like set
a is Element of E
X . a is set
X .: a is set
f is epsilon-transitive epsilon-connected ordinal set
(E,f) is set
X is Relation-like Function-like set
dom X is set
a is Element of E
X . a is set
X .: a is set
E is non empty set
f is Relation-like Function-like set
dom f is set
rng f is set
X is set
a is set
f . a is set
b is Element of E
f . b is set
f .: b is set
d2 is set
Z is set
f . Z is set
E is non empty set
All ((x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))) is Relation-like K32() -defined K32() -valued Function-like V47() ZF-formula-like M7(K32())
All ((x. 0),(All ((x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1)))))) is Relation-like K32() -defined K32() -valued Function-like V47() ZF-formula-like M7(K32())
K7(VAR,E) is set
K6(K7(VAR,E)) is set
f is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of K6(K7(VAR,E))
f . (x. 0) is Element of E
f . (x. 1) is Element of E
X is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of K6(K7(VAR,E))
X . (x. 2) is Element of E
X . (x. 1) is Element of E
X . (x. 0) is Element of E
the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of K6(K7(VAR,E)) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of K6(K7(VAR,E))
X is Element of E
a is Element of E
the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of K6(K7(VAR,E)) +* ((x. 0),X) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of K6(K7(VAR,E))
( the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of K6(K7(VAR,E)) +* ((x. 0),X)) . (x. 0) is Element of E
5 + 0 is set
5 + 1 is set
( the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of K6(K7(VAR,E)) +* ((x. 0),X)) +* ((x. 1),a) is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of K6(K7(VAR,E))
5 + 2 is set
Z is Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of K6(K7(VAR,E))
Z . (x. 2) is Element of E
Z . (x. 0) is Element of E
Z . (x. 1) is Element of E
(( the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of K6(K7(VAR,E)) +* ((x. 0),X)) +* ((x. 1),a)) . (x. 0) is Element of E
(( the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of K6(K7(VAR,E)) +* ((x. 0),X)) +* ((x. 1),a)) . (x. 1) is Element of E
(( the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of K6(K7(VAR,E)) +* ((x. 0),X)) +* ((x. 1),a)) . (x. 1) is Element of E
(( the Relation-like VAR -defined E -valued Function-like V29( VAR ,E) Element of K6(K7(VAR,E)) +* ((x. 0),X)) +* ((x. 1),a)) . (x. 0) is Element of E
f is Element of E
X is Element of E
E is non empty set
f is Relation-like Function-like set
dom f is set
X is set
a is set
f . X is set
f . a is set
b is Element of E
Z is epsilon-transitive epsilon-connected ordinal set
(E,Z) is set
d2 is Element of E
c is epsilon-transitive epsilon-connected ordinal set
(E,c) is set
A is epsilon-transitive epsilon-connected ordinal set
(E,A) is set
d1 is Element of E
d2 is Element of E
f . d1 is set
f . d2 is set
d1 is Element of E
d2 is Element of E
f . d1 is set
f . d2 is set
w is Element of E
f .: d1 is set
f .: d2 is set
A1 is epsilon-transitive epsilon-connected ordinal set
(E,A1) is set
f . w is set
a is set
f . a is set
v is Element of E
A2 is epsilon-transitive epsilon-connected ordinal set
(E,A2) is set
c17 is Element of E
c18 is Element of E
f . c17 is set
f . c18 is set
A1 is epsilon-transitive epsilon-connected ordinal set
(E,A1) is set
a is set
f . a is set
v is Element of E
A2 is epsilon-transitive epsilon-connected ordinal set
(E,A2) is set
c17 is Element of E
c18 is Element of E
f . c17 is set
f . c18 is set
rng f is set
X is set
a is set
f . a is set
b is set
f . b is set
Z is set
d2 is Element of E
f . d2 is set
f .: d2 is set
Z is set
d2 is Element of E
f . d2 is set
f .: d2 is set
c is set
f . c is set