:: ORDINAL2 semantic presentation

{n} is non empty set
n \/ {n} is non empty set

{n} is non empty set
n \/ {n} is non empty set

{n} is non empty set
n \/ {n} is non empty set

{n} is non empty set
n \/ {n} is non empty set

{n} is non empty set
n \/ {n} is non empty set

n is set
a is set

{n} is non empty set
n \/ {n} is non empty set
bool n is non empty Element of bool (bool n)
bool n is non empty set
bool (bool n) is non empty set
n is set

n is set
a is set

n . (union (dom n)) is set

{n} is non empty set
n \/ {n} is non empty set
(n) is set

n . (union (dom n)) is set
n . n is set
n is set
On n is set
n is set

On n is set
n is set
a is set
n is set
On n is set
n is set
On n is set
a is set
n is set
Lim n is set
n is set
n is set
Lim n is set
n is set
Lim n is set
a is set

n is set
Lim n is set
On n is set
n is set

n is set
meet n is set
the Element of n is Element of n

b is set
xi is set

n is set
On n is set
meet (On n) is set
n is set
n is set
union (On n) is set

{n} is non empty set
n \/ {n} is non empty set
a is set

n is set

On n is set
meet (On n) is set

n is set
On n is set

meet (On n) is set
a is set
b is set

n is set

On n is set
meet (On n) is set
a is set

On a is set
meet (On a) is set

n is set

On n is set
meet (On n) is set

b is set
xi is set

On n is set

n is set

On n is set

n is set

On n is set
a is set

n is set

n is set

n is set

On n is set
On n is set

{n} is non empty set

n \/ {n} is non empty set
On {n} is set
n is set

n is set

On n is set
meet (On n) is set

n is set
the Element of On n is Element of On n

dom n is set

a . b is set
F2(b) is set
{b} is non empty set
union {b} is set

F2((())) is set

F2((b)) is set

rng n is set

rng n is set

rng (n | n) is set

n . n is set
rng n is set

n . n is set

rng n is set

n is set
a is set
n . a is set

n . b is set

On (rng n) is set

F5() . {} is set
F2() is set

F6() . {} is set
n is set
n is set
n is set
F5() . n is set
F6() . n is set

rng F5() is set

rng F6() is set

F5() . a is set
F6() . a is set
a is set
(F5() | n) . a is set
F5() . a is set
(F6() | n) . a is set
F6() . a is set

{a} is non empty set
a \/ {a} is non empty set
F5() . a is set
(F5() | n) . a is set
F6() . a is set
(F6() | n) . a is set
F5() . n is set
F3(a,(F5() . a)) is set
F6() . n is set
F3(a,(F6() . a)) is set
F4(n,(F5() | n)) is set
F4(n,(F6() | n)) is set

{a} is non empty set
a \/ {a} is non empty set

F2() is set

n is set
a is set
b is set

B . C is set

rng B is set
F4(C,(B | C)) is set

{C} is non empty set
C \/ {C} is non empty set
B . (succ C) is set
B . C is set
F3(C,(B . C)) is set
B . {} is set

C . {} is set

{D} is non empty set
D \/ {D} is non empty set
C . (succ D) is set
C . D is set
F3(D,(C . D)) is set

C . D is set

rng C is set
F4(D,(C | D)) is set

dom n is set
a is set
b is set
[a,b] is set
{a,b} is non empty set
{a} is non empty set
{{a,b},{a}} is non empty set
a is set

xi . {} is set

C . {} is set

{D} is non empty set
D \/ {D} is non empty set
C . (succ D) is set
C . D is set
F3(D,(C . D)) is set

C . E is set

rng C is set
F4(E,(C | E)) is set
[b,xi] is set
{b,xi} is non empty set
{b} is non empty set
{{b,xi},{b}} is non empty set
a is set
n . a is set
xi is set
[a,xi] is set
{a,xi} is non empty set
{a} is non empty set
{{a,xi},{a}} is non empty set

{C} is non empty set
C \/ {C} is non empty set

B . C is set
F3(C,(B . C)) is set
F4(b,B) is set

F4(b,B) is set

{E} is non empty set
E \/ {E} is non empty set
D . E is set
F3(E,(D . E)) is set
F4(C,D) is set

L2 is set

{C} is non empty set
C \/ {C} is non empty set
C . C is set
F3(C,(C . C)) is set
F4(D,C) is set

{c14} is non empty set
c14 \/ {c14} is non empty set

{c17} is non empty set
c17 \/ {c17} is non empty set
c16 . c17 is set
F3(c17,(c16 . c17)) is set
F4(c15,c16) is set
a is set
n . a is set
b is set
xi is set

F4(B,C) is set

F4(D,E) is set

{L2} is non empty set
L2 \/ {L2} is non empty set

{D} is non empty set
D \/ {D} is non empty set
C . D is set
F3(D,(C . D)) is set

{D} is non empty set
D \/ {D} is non empty set
C . D is set
F3(D,(C . D)) is set

{C} is non empty set
C \/ {C} is non empty set
E . C is set
F3(C,(E . C)) is set

{C} is non empty set
C \/ {C} is non empty set
E . C is set
F3(C,(E . C)) is set

{L2} is non empty set
L2 \/ {L2} is non empty set
C . L2 is set
F3(L2,(C . L2)) is set

{D} is non empty set
D \/ {D} is non empty set
E . D is set
F3(D,(E . D)) is set

dom a is set

b . {} is set
n . {} is set
a . {} is set

{C} is non empty set
C \/ {C} is non empty set
B . C is set
F3(C,(B . C)) is set
F4(xi,B) is set

n . xi is set

rng b is set

[xi,B] is set
{xi,B} is non empty set
{xi} is non empty set
{{xi,B},{xi}} is non empty set

B . {} is set

{C} is non empty set
C \/ {C} is non empty set
B . (succ C) is set
B . C is set
F3(C,(B . C)) is set

B . D is set

rng B is set
F4(D,(B | D)) is set
C is set

n . D is set
b . D is set

F4(E,L2) is set

rng B is set

C . {} is set

{C} is non empty set
C \/ {C} is non empty set
C . (succ C) is set
C . C is set
F3(C,(C . C)) is set
(B | D) . C is set
B . C is set
(B | D) . (succ C) is set
B . (succ C) is set

C . C is set

rng C is set
F4(C,(C | C)) is set

B . C is set
[D,(B | D)] is set
{D,(B | D)} is non empty set
{D} is non empty set
{{D,(B | D)},{D}} is non empty set
(b | xi) . C is set
b . C is set

{D} is non empty set
D \/ {D} is non empty set
B . C is set
B . D is set
F3(D,(B . D)) is set

{C} is non empty set
C \/ {C} is non empty set
L2 . C is set
F3(C,(L2 . C)) is set

{C} is non empty set
C \/ {C} is non empty set
L2 . C is set
F3(C,(L2 . C)) is set

{D} is non empty set
D \/ {D} is non empty set
L2 . D is set
F3(D,(L2 . D)) is set

{xi} is non empty set
xi \/ {xi} is non empty set
b . (succ xi) is set
b . xi is set
F3(xi,(b . xi)) is set
n . (succ xi) is set
a . (succ xi) is set

F4(B,C) is set

rng b is set

{D} is non empty set
D \/ {D} is non empty set
C . D is set
F3(D,(C . D)) is set

{D} is non empty set
D \/ {D} is non empty set
C . D is set
F3(D,(C . D)) is set

b . xi is set

rng b is set
F4(xi,(b | xi)) is set
n . xi is set
a . xi is set

{D} is non empty set
D \/ {D} is non empty set
C . D is set
F3(D,(C . D)) is set
F4(B,C) is set
F4() is set

F1() . {} is set

F1() . n is set
F2(n) is set

{n} is non empty set
n \/ {n} is non empty set

rng F1() is set

{a} is non empty set
a \/ {a} is non empty set
(F1() | (succ n)) . (succ a) is set
(F1() | (succ n)) . a is set
F5(a,((F1() | (succ n)) . a)) is set
F1() . a is set
F1() . (succ a) is set

(F1() | (succ n)) . a is set
(F1() | (succ n)) | a is T-Sequence-like Relation-like rng (F1() | (succ n)) -valued Function-like set
rng (F1() | (succ n)) is set
F6(a,((F1() | (succ n)) | a)) is set

F1() . a is set
(F1() | (succ n)) . {} is set
dom (F1() | (succ n)) is epsilon-transitive epsilon-connected ordinal set
((F1() | (succ n))) is set
union (dom (F1() | (succ n))) is epsilon-transitive epsilon-connected ordinal set
(F1() | (succ n)) . (union (dom (F1() | (succ n)))) is set
(F1() | (succ n)) . n is set

{F1()} is non empty set
F1() \/ {F1()} is non empty set
F2() is set

n . {} is set
(n) is set

n . (union (dom n)) is set
n is set

{a} is non empty set
a \/ {a} is non empty set
n . (succ a) is set
n . a is set
F3(a,(n . a)) is set

n . b is set

rng n is set
F4(b,(n | b)) is set
n is set
a is set

(b) is set

b . (union (dom b)) is set
b . {} is set

(xi) is set

xi . (union (dom xi)) is set
xi . {} is set
F2() is set
F1({}) is set

is non empty set
{} \/ is non empty set

n . {} is set
(n) is set

n . (union (dom n)) is set
F1() is set

{n} is non empty set
n \/ {n} is non empty set
F4((succ n)) is set
F4(n) is set
F2(n,F4(n)) is set

{(succ n)} is non empty set
(succ n) \/ {(succ n)} is non empty set

n . {} is set
b is set

F4(a) is set

{a} is non empty set
a \/ {a} is non empty set
B is set

(C) is set

C . (union (dom C)) is set

{xi} is non empty set
xi \/ {xi} is non empty set
C . {} is set
F4(xi) is set
n . (succ n) is set
n . n is set
F4() is set

F3(F2()) is set
F6(F2(),F1()) is set

{F2()} is non empty set
F2() \/ {F2()} is non empty set

n . {} is set

rng n is set
b is set

F3(a) is set

{a} is non empty set
a \/ {a} is non empty set
B is set

(C) is set

C . (union (dom C)) is set

{xi} is non empty set
xi \/ {xi} is non empty set
C . {} is set
F3(xi) is set
a is set
(n | F2()) . a is set

n . b is set
F3(b) is set
F1() . a is set

n . F2() is set

n . {} is set
rng n is set

n is set
a is set
n . a is set

n . b is set

F4(b,(n | b)) is epsilon-transitive epsilon-connected ordinal set
On (rng n) is set

{xi} is non empty set
xi \/ {xi} is non empty set
n . xi is set
{(n . xi)} is non empty set
union {(n . xi)} is set
((union {(n . xi)})) is epsilon-transitive epsilon-connected ordinal set
F3(xi,((union {(n . xi)}))) is epsilon-transitive epsilon-connected ordinal set

{xi} is non empty set
xi \/ {xi} is non empty set

{b} is non empty set
b \/ {b} is non empty set

F3(b,(a . b)) is epsilon-transitive epsilon-connected ordinal set

{xi} is non empty set
union {xi} is set

rng a is set
F4(b,(a | b)) is epsilon-transitive epsilon-connected ordinal set

{n} is non empty set
n \/ {n} is non empty set
F1() | (succ n) is T-Sequence-like Relation-like rng F1() -valued Function-like () set
rng F1() is set

{a} is non empty set
a \/ {a} is non empty set
(F1() | (succ n)) . (succ a) is epsilon-transitive epsilon-connected ordinal set
(F1() | (succ n)) . a is epsilon-transitive epsilon-connected ordinal set
F5(a,((F1() | (succ n)) . a)) is epsilon-transitive epsilon-connected ordinal set

(F1() | (succ n)) . a is epsilon-transitive epsilon-connected ordinal set
(F1() | (succ n)) | a is T-Sequence-like Relation-like rng (F1() | (succ n)) -valued Function-like () set
rng (F1() | (succ n)) is set
F6(a,((F1() | (succ n)) | a)) is epsilon-transitive epsilon-connected ordinal set

(F1() | (succ n)) . {} is epsilon-transitive epsilon-connected ordinal set
dom (F1() | (succ n)) is epsilon-transitive epsilon-connected ordinal set
((F1() | (succ n))) is set
union (dom (F1() | (succ n))) is epsilon-transitive epsilon-connected ordinal set
(F1() | (succ n)) . (union (dom (F1() | (succ n)))) is epsilon-transitive epsilon-connected ordinal set
(F1() | (succ n)) . n is epsilon-transitive epsilon-connected ordinal set

{F1()} is non empty set
F1() \/ {F1()} is non empty set

(n) is set

{a} is non empty set
a \/ {a} is non empty set

F3(a,(n . a)) is epsilon-transitive epsilon-connected ordinal set

rng n is set
F4(b,(n | b)) is epsilon-transitive epsilon-connected ordinal set

(xi) is set

{B} is non empty set
B \/ {B} is non empty set

{(xi . B)} is non empty set
union {(xi . B)} is set
((union {(xi . B)})) is epsilon-transitive epsilon-connected ordinal set
F3(B,((union {(xi . B)}))) is epsilon-transitive epsilon-connected ordinal set

(B) is set

rng B is set
F4(C,(B | C)) is epsilon-transitive epsilon-connected ordinal set

rng xi is set
F4(C,(xi | C)) is epsilon-transitive epsilon-connected ordinal set

{C} is non empty set
C \/ {C} is non empty set

{(B . C)} is non empty set
union {(B . C)} is set
((union {(B . C)})) is epsilon-transitive epsilon-connected ordinal set
F3(C,((union {(B . C)}))) is epsilon-transitive epsilon-connected ordinal set

is non empty set
{} \/ is non empty set

(n) is set

{n} is non empty set
n \/ {n} is non empty set

F2(n,F4(n)) is epsilon-transitive epsilon-connected ordinal set

{(succ n)} is non empty set
(succ n) \/ {(succ n)} is non empty set

{a} is non empty set
a \/ {a} is non empty set

(C) is set

{xi} is non empty set
xi \/ {xi} is non empty set

F6(F2(),F1()) is epsilon-transitive epsilon-connected ordinal set

{F2()} is non empty set
F2() \/ {F2()} is non empty set

rng n is set

{a} is non empty set
a \/ {a} is non empty set

(C) is set

{xi} is non empty set
xi \/ {xi} is non empty set

a is set
(n | F2()) . a is set

F1() . a is set

rng n is set

On (rng n) is set
meet (On (rng n)) is set

rng n is set

rng n is set

On (rng n) is set
meet (On (rng n)) is set

rng n is set

On (rng n) is set
meet (On (rng n)) is set

(dom n) \ a is Element of bool (dom n)
bool (dom n) is non empty set
n | ((dom n) \ a) is Relation-like Function-like set
rng (n | ((dom n) \ a)) is set
((rng (n | ((dom n) \ a)))) is epsilon-transitive epsilon-connected ordinal set

rng b is set

On (rng b) is set
meet (On (rng b)) is set

rng xi is set

On (rng xi) is set
meet (On (rng xi)) is set

B is set

(dom n) \ C is Element of bool (dom n)
bool (dom n) is non empty set
n | ((dom n) \ C) is Relation-like Function-like set
rng (n | ((dom n) \ C)) is set
((rng (n | ((dom n) \ C)))) is epsilon-transitive epsilon-connected ordinal set
b . B is set
xi . B is set

rng n is set

(dom n) \ a is Element of bool (dom n)
bool (dom n) is non empty set
n | ((dom n) \ a) is Relation-like Function-like set
rng (n | ((dom n) \ a)) is set
((rng (n | ((dom n) \ a)))) is epsilon-transitive epsilon-connected ordinal set
On (rng (n | ((dom n) \ a))) is set
meet (On (rng (n | ((dom n) \ a)))) is set

rng b is set

rng xi is set

B is set

(dom n) \ C is Element of bool (dom n)
bool (dom n) is non empty set
n | ((dom n) \ C) is Relation-like Function-like set
rng (n | ((dom n) \ C)) is set
((rng (n | ((dom n) \ C)))) is epsilon-transitive epsilon-connected ordinal set
On (rng (n | ((dom n) \ C))) is set
meet (On (rng (n | ((dom n) \ C)))) is set
b . B is set
xi . B is set

{b} is non empty set
b \/ {b} is non empty set

{a} is non empty set
a \/ {a} is non empty set

rng n is set

{n} is non empty set
n \/ {n} is non empty set

(xi) is set

(B) is set

(D) is set

{n} is non empty set
n \/ {n} is non empty set

(xi) is set

(B) is set

(D) is set

{n} is non empty set
n \/ {n} is non empty set

(xi) is set

(B) is set

(D) is set

{n} is non empty set
n \/ {n} is non empty set

(B) is set

{b} is non empty set
b \/ {b} is non empty set

{n} is non empty set
n \/ {n} is non empty set

succ (n,n) is non empty epsilon-transitive epsilon-connected ordinal set
{(n,n)} is non empty set
(n,n) \/ {(n,n)} is non empty set

{a} is non empty set
a \/ {a} is non empty set

(C) is set

{xi} is non empty set
xi \/ {xi} is non empty set

rng a is set

{b} is non empty set
b \/ {b} is non empty set

(D) is set

{B} is non empty set
B \/ {B} is non empty set

{n} is non empty set
n \/ {n} is non empty set

rng a is set
b is set
xi is set
a . xi is set

b is set

is non empty set
{} \/ is non empty set

{n} is non empty set
n \/ {n} is non empty set

{(n,{})} is non empty set
(n,{}) \/ {(n,{})} is non empty set

{xi} is non empty set
xi \/ {xi} is non empty set

succ (a,xi) is non empty epsilon-transitive epsilon-connected ordinal set
{(a,xi)} is non empty set
(a,xi) \/ {(a,xi)} is non empty set

rng xi is set

{xi} is non empty set
xi \/ {xi} is non empty set

{xi} is non empty set
xi \/ {xi} is non empty set

succ (n,xi) is non empty epsilon-transitive epsilon-connected ordinal set
{(n,xi)} is non empty set
(n,xi) \/ {(n,xi)} is non empty set

succ (n,xi) is non empty epsilon-transitive epsilon-connected ordinal set
{(n,xi)} is non empty set
(n,xi) \/ {(n,xi)} is non empty set

rng xi is set
C is set
xi . C is set

{xi} is non empty set
xi \/ {xi} is non empty set

{n} is non empty set
n \/ {n} is non empty set

(B) is set

{b} is non empty set
b \/ {b} is non empty set

{n} is non empty set
n \/ {n} is non empty set

((n,n),n) is epsilon-transitive epsilon-connected ordinal set

{a} is non empty set
a \/ {a} is non empty set

(C) is set

{xi} is non empty set
xi \/ {xi} is non empty set

rng a is set

{b} is non empty set
b \/ {b} is non empty set

(D) is set

{B} is non empty set
B \/ {B} is non empty set

{n} is non empty set
n \/ {n} is non empty set

rng a is set
b is set
xi is set
a . xi is set

b is set

a . b is set

rng a is set
b is set

a . b is set
b is set
xi is set
a . xi is set

{a} is non empty set
a \/ {a} is non empty set

((a,()),()) is epsilon-transitive epsilon-connected ordinal set

{(a,{})} is non empty set
(a,{}) \/ {(a,{})} is non empty set

{a} is non empty set
a \/ {a} is non empty set

{xi} is non empty set
xi \/ {xi} is non empty set

((xi,n),{}) is epsilon-transitive epsilon-connected ordinal set
((xi,n),n) is epsilon-transitive epsilon-connected ordinal set

((n,n),n) is epsilon-transitive epsilon-connected ordinal set

{n} is non empty set
n \/ {n} is non empty set

rng xi is set

{xi} is non empty set
xi \/ {xi} is non empty set

{xi} is non empty set
xi \/ {xi} is non empty set

((xi,n),n) is epsilon-transitive epsilon-connected ordinal set
((xi,n),n) is epsilon-transitive epsilon-connected ordinal set
((xi,n),n) is epsilon-transitive epsilon-connected ordinal set

rng xi is set
C is set
xi . C is set

{xi} is non empty set
xi \/ {xi} is non empty set

{n} is non empty set
n \/ {n} is non empty set

(B) is set

{b} is non empty set
b \/ {b} is non empty set

{n} is non empty set
n \/ {n} is non empty set

(n,(n,n)) is epsilon-transitive epsilon-connected ordinal set

{a} is non empty set
a \/ {a} is non empty set