:: ZF_COLLA semantic presentation

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

{ b

( not b

( b

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

{ b

( not b

( b

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

{ b

( not b

( b

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

{ b

( not b

( b

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

{ b

( not b

( b

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

dom d2 is epsilon-transitive epsilon-connected ordinal set

{ b

( not b

( b

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

{ b

( not b

( b

E is non empty set

f is epsilon-transitive epsilon-connected ordinal set

(E,f) is set

{ b

( not b

( b

{ b

( not b

( b

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

{ b

( not b

( b

Z is epsilon-transitive epsilon-connected ordinal set

(E,Z) is set

{ b

( not b

( b

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

{ b

( not b

( b

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

{ b

( not b

( b

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

{ b

( not b

( b

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

{ b

( not b

( b

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

{ b

( not b

( b

b is Element of E

d2 is Element of E

Z is epsilon-transitive epsilon-connected ordinal set

(E,Z) is set

{ b

( not b

( b

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

{ b

( not b

( b

(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

{ b

( not b

( b

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

{ b

( not b

( b

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

c

c

f . c

f . c

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

c

c

f . c

f . c

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