:: ORDINAL2 semantic presentation

omega is non empty epsilon-transitive epsilon-connected ordinal set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional set
meet {} is set
union {} is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
union (succ n) is epsilon-transitive epsilon-connected ordinal set
n is set
a is set
b is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal 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
a is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
union n is epsilon-transitive epsilon-connected ordinal set
n is set
a is set
n is T-Sequence-like Relation-like Function-like set
dom n is epsilon-transitive epsilon-connected ordinal set
union (dom n) is epsilon-transitive epsilon-connected ordinal set
n . (union (dom n)) is set
n is T-Sequence-like Relation-like Function-like set
dom n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
(n) is set
union (dom n) is epsilon-transitive epsilon-connected ordinal set
n . (union (dom n)) is set
n . n is set
n is set
On n is set
n is set
n is epsilon-transitive epsilon-connected ordinal 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
b is epsilon-transitive epsilon-connected ordinal set
n is set
Lim n is set
On n is set
n is set
a is epsilon-transitive epsilon-connected ordinal set
n is set
meet n is set
the Element of n is Element of n
a is epsilon-transitive epsilon-connected ordinal set
b is set
xi is set
B is epsilon-transitive epsilon-connected ordinal 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 epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
a is set
b is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
n is set
(n) is epsilon-transitive epsilon-connected ordinal set
On n is set
meet (On n) is set
n is epsilon-transitive epsilon-connected ordinal set
n is set
On n is set
(n) is epsilon-transitive epsilon-connected ordinal set
meet (On n) is set
a is set
b is set
xi is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
n is set
(n) is epsilon-transitive epsilon-connected ordinal set
On n is set
meet (On n) is set
a is set
(a) is epsilon-transitive epsilon-connected ordinal set
On a is set
meet (On a) is set
n is epsilon-transitive epsilon-connected ordinal set
n is set
(n) is epsilon-transitive epsilon-connected ordinal set
On n is set
meet (On n) is set
a is epsilon-transitive epsilon-connected ordinal set
b is set
xi is set
B is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(n) is epsilon-transitive epsilon-connected ordinal set
On n is set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
n is set
(n) is epsilon-transitive epsilon-connected ordinal set
On n is set
n is epsilon-transitive epsilon-connected ordinal set
n is set
(n) is epsilon-transitive epsilon-connected ordinal set
On n is set
a is set
b is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
n is set
(n) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
n is set
(n) is epsilon-transitive epsilon-connected ordinal set
n is set
(n) is epsilon-transitive epsilon-connected ordinal set
On n is set
On n is set
n is epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
({n}) is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
n \/ {n} is non empty set
On {n} is set
n is set
n is epsilon-transitive epsilon-connected ordinal set
n is set
(n) is epsilon-transitive epsilon-connected ordinal set
On n is set
meet (On n) is set
(n) is epsilon-transitive epsilon-connected ordinal set
n is set
the Element of On n is Element of On n
b is epsilon-transitive epsilon-connected ordinal set
F₁() is epsilon-transitive epsilon-connected ordinal set
n is Relation-like Function-like set
dom n is set
n is T-Sequence-like Relation-like Function-like set
a is T-Sequence-like Relation-like Function-like set
dom a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a . b is set
F₂(b) is set
{b} is non empty set
union {b} is set
((union {b})) is epsilon-transitive epsilon-connected ordinal set
F₂(((union {b}))) is set
(b) is epsilon-transitive epsilon-connected ordinal set
F₂((b)) is set
the epsilon-transitive epsilon-connected ordinal set is epsilon-transitive epsilon-connected ordinal set
the T-Sequence-like Relation-like the epsilon-transitive epsilon-connected ordinal set -valued Function-like set is T-Sequence-like Relation-like the epsilon-transitive epsilon-connected ordinal set -valued Function-like set
rng the T-Sequence-like Relation-like the epsilon-transitive epsilon-connected ordinal set -valued Function-like set is set
n is epsilon-transitive epsilon-connected ordinal set
n is T-Sequence-like Relation-like n -valued Function-like set
rng n is set
n is T-Sequence-like Relation-like Function-like () set
n is epsilon-transitive epsilon-connected ordinal set
n | n is T-Sequence-like Relation-like rng n -valued Function-like set
rng n is set
a is epsilon-transitive epsilon-connected ordinal set
rng (n | n) is set
n is epsilon-transitive epsilon-connected ordinal set
n is T-Sequence-like Relation-like Function-like () set
dom n is epsilon-transitive epsilon-connected ordinal set
n . n is set
rng n is set
a is epsilon-transitive epsilon-connected ordinal set
n is T-Sequence-like Relation-like Function-like () set
n is epsilon-transitive epsilon-connected ordinal set
n . n is set
dom n is epsilon-transitive epsilon-connected ordinal set
F₁() is epsilon-transitive epsilon-connected ordinal set
n is T-Sequence-like Relation-like Function-like set
dom n is epsilon-transitive epsilon-connected ordinal set
rng n is set
((rng n)) is epsilon-transitive epsilon-connected ordinal set
n is set
a is set
n . a is set
b is epsilon-transitive epsilon-connected ordinal set
n . b is set
F₂(b) is epsilon-transitive epsilon-connected ordinal set
On (rng n) is set
n is T-Sequence-like Relation-like Function-like () set
a is T-Sequence-like Relation-like Function-like () set
dom a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a . b is epsilon-transitive epsilon-connected ordinal set
F₂(b) is epsilon-transitive epsilon-connected ordinal set
F₅() is T-Sequence-like Relation-like Function-like set
dom F₅() is epsilon-transitive epsilon-connected ordinal set
F₁() is epsilon-transitive epsilon-connected ordinal set
F₅() . {} is set
F₂() is set
F₆() is T-Sequence-like Relation-like Function-like set
dom F₆() is epsilon-transitive epsilon-connected ordinal set
F₆() . {} is set
n is set
n is set
n is set
F₅() . n is set
F₆() . n is set
n is epsilon-transitive epsilon-connected ordinal set
F₅() | n is T-Sequence-like Relation-like rng F₅() -valued Function-like set
rng F₅() is set
dom (F₅() | n) is epsilon-transitive epsilon-connected ordinal set
F₆() | n is T-Sequence-like Relation-like rng F₆() -valued Function-like set
rng F₆() is set
dom (F₆() | n) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
F₅() . a is set
F₆() . a is set
a is set
(F₅() | n) . a is set
F₅() . a is set
(F₆() | n) . a is set
F₆() . a is set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
F₅() . a is set
(F₅() | n) . a is set
F₆() . a is set
(F₆() | n) . a is set
F₅() . n is set
F₃(a,(F₅() . a)) is set
F₆() . n is set
F₃(a,(F₆() . a)) is set
F₄(n,(F₅() | n)) is set
F₄(n,(F₆() | n)) is set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
F₁() is epsilon-transitive epsilon-connected ordinal set
F₂() is set
n is epsilon-transitive epsilon-connected ordinal set
n is set
a is set
b is set
B is T-Sequence-like Relation-like Function-like set
dom B is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
B . C is set
B | C is T-Sequence-like Relation-like rng B -valued Function-like set
rng B is set
F₄(C,(B | C)) is set
C is epsilon-transitive epsilon-connected ordinal set
succ C is non empty epsilon-transitive epsilon-connected ordinal set
{C} is non empty set
C \/ {C} is non empty set
B . (succ C) is set
B . C is set
F₃(C,(B . C)) is set
B . {} is set
C is T-Sequence-like Relation-like Function-like set
C . {} is set
D is epsilon-transitive epsilon-connected ordinal set
succ D is non empty epsilon-transitive epsilon-connected ordinal set
{D} is non empty set
D \/ {D} is non empty set
C . (succ D) is set
C . D is set
F₃(D,(C . D)) is set
D is epsilon-transitive epsilon-connected ordinal set
C . D is set
C | D is T-Sequence-like Relation-like rng C -valued Function-like set
rng C is set
F₄(D,(C | D)) is set
dom C is epsilon-transitive epsilon-connected ordinal set
n is Relation-like Function-like 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
b is epsilon-transitive epsilon-connected ordinal set
xi is T-Sequence-like Relation-like Function-like set
dom xi is epsilon-transitive epsilon-connected ordinal set
xi . {} is set
B is epsilon-transitive epsilon-connected ordinal set
C is T-Sequence-like Relation-like Function-like set
dom C is epsilon-transitive epsilon-connected ordinal set
C . {} is set
D is epsilon-transitive epsilon-connected ordinal set
succ D is non empty epsilon-transitive epsilon-connected ordinal set
{D} is non empty set
D \/ {D} is non empty set
C . (succ D) is set
C . D is set
F₃(D,(C . D)) is set
E is epsilon-transitive epsilon-connected ordinal set
C . E is set
C | E is T-Sequence-like Relation-like rng C -valued Function-like set
rng C is set
F₄(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
b is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
succ C is non empty epsilon-transitive epsilon-connected ordinal set
{C} is non empty set
C \/ {C} is non empty set
B is T-Sequence-like Relation-like Function-like set
B . C is set
F₃(C,(B . C)) is set
F₄(b,B) is set
B is T-Sequence-like Relation-like Function-like set
F₄(b,B) is set
C is epsilon-transitive epsilon-connected ordinal set
D is T-Sequence-like Relation-like Function-like set
E is epsilon-transitive epsilon-connected ordinal set
succ E is non empty epsilon-transitive epsilon-connected ordinal set
{E} is non empty set
E \/ {E} is non empty set
D . E is set
F₃(E,(D . E)) is set
F₄(C,D) is set
D is epsilon-transitive epsilon-connected ordinal set
C is T-Sequence-like Relation-like Function-like set
L2 is set
C is epsilon-transitive epsilon-connected ordinal set
succ C is non empty epsilon-transitive epsilon-connected ordinal set
{C} is non empty set
C \/ {C} is non empty set
C . C is set
F₃(C,(C . C)) is set
F₄(D,C) is set
c₁₄ is epsilon-transitive epsilon-connected ordinal set
succ c₁₄ is non empty epsilon-transitive epsilon-connected ordinal set
{c₁₄} is non empty set
c₁₄ \/ {c₁₄} is non empty set
c₁₅ is epsilon-transitive epsilon-connected ordinal set
c₁₆ is T-Sequence-like Relation-like Function-like set
c₁₇ is epsilon-transitive epsilon-connected ordinal set
succ c₁₇ is non empty epsilon-transitive epsilon-connected ordinal set
{c₁₇} is non empty set
c₁₇ \/ {c₁₇} is non empty set
c₁₆ . c₁₇ is set
F₃(c₁₇,(c₁₆ . c₁₇)) is set
F₄(c₁₅,c₁₆) is set
a is set
n . a is set
b is set
xi is set
B is epsilon-transitive epsilon-connected ordinal set
C is T-Sequence-like Relation-like Function-like set
F₄(B,C) is set
D is epsilon-transitive epsilon-connected ordinal set
E is T-Sequence-like Relation-like Function-like set
F₄(D,E) is set
L2 is epsilon-transitive epsilon-connected ordinal set
succ L2 is non empty epsilon-transitive epsilon-connected ordinal set
{L2} is non empty set
L2 \/ {L2} is non empty set
D is epsilon-transitive epsilon-connected ordinal set
succ D is non empty epsilon-transitive epsilon-connected ordinal set
{D} is non empty set
D \/ {D} is non empty set
C . D is set
F₃(D,(C . D)) is set
D is epsilon-transitive epsilon-connected ordinal set
succ D is non empty epsilon-transitive epsilon-connected ordinal set
{D} is non empty set
D \/ {D} is non empty set
C . D is set
F₃(D,(C . D)) is set
C is epsilon-transitive epsilon-connected ordinal set
succ C is non empty epsilon-transitive epsilon-connected ordinal set
{C} is non empty set
C \/ {C} is non empty set
E . C is set
F₃(C,(E . C)) is set
C is epsilon-transitive epsilon-connected ordinal set
succ C is non empty epsilon-transitive epsilon-connected ordinal set
{C} is non empty set
C \/ {C} is non empty set
E . C is set
F₃(C,(E . C)) is set
L2 is epsilon-transitive epsilon-connected ordinal set
succ L2 is non empty epsilon-transitive epsilon-connected ordinal set
{L2} is non empty set
L2 \/ {L2} is non empty set
C . L2 is set
F₃(L2,(C . L2)) is set
D is epsilon-transitive epsilon-connected ordinal set
succ D is non empty epsilon-transitive epsilon-connected ordinal set
{D} is non empty set
D \/ {D} is non empty set
E . D is set
F₃(D,(E . D)) is set
a is Relation-like Function-like set
dom a is set
b is T-Sequence-like Relation-like Function-like set
dom b is epsilon-transitive epsilon-connected ordinal set
b . {} is set
n . {} is set
a . {} is set
xi is epsilon-transitive epsilon-connected ordinal set
B is T-Sequence-like Relation-like Function-like set
C is epsilon-transitive epsilon-connected ordinal set
succ C is non empty epsilon-transitive epsilon-connected ordinal set
{C} is non empty set
C \/ {C} is non empty set
B . C is set
F₃(C,(B . C)) is set
F₄(xi,B) is set
xi is epsilon-transitive epsilon-connected ordinal set
n . xi is set
b | xi is T-Sequence-like Relation-like rng b -valued Function-like set
rng b is set
B is T-Sequence-like Relation-like Function-like set
[xi,B] is set
{xi,B} is non empty set
{xi} is non empty set
{{xi,B},{xi}} is non empty set
dom B is epsilon-transitive epsilon-connected ordinal set
B . {} is set
C is epsilon-transitive epsilon-connected ordinal set
succ C is non empty epsilon-transitive epsilon-connected ordinal set
{C} is non empty set
C \/ {C} is non empty set
B . (succ C) is set
B . C is set
F₃(C,(B . C)) is set
D is epsilon-transitive epsilon-connected ordinal set
B . D is set
B | D is T-Sequence-like Relation-like rng B -valued Function-like set
rng B is set
F₄(D,(B | D)) is set
C is set
D is epsilon-transitive epsilon-connected ordinal set
n . D is set
b . D is set
E is epsilon-transitive epsilon-connected ordinal set
L2 is T-Sequence-like Relation-like Function-like set
F₄(E,L2) is set
B | D is T-Sequence-like Relation-like rng B -valued Function-like set
rng B is set
D is epsilon-transitive epsilon-connected ordinal set
C is T-Sequence-like Relation-like Function-like set
dom C is epsilon-transitive epsilon-connected ordinal set
C . {} is set
C is epsilon-transitive epsilon-connected ordinal set
succ C is non empty epsilon-transitive epsilon-connected ordinal set
{C} is non empty set
C \/ {C} is non empty set
C . (succ C) is set
C . C is set
F₃(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 is epsilon-transitive epsilon-connected ordinal set
C . C is set
C | C is T-Sequence-like Relation-like rng C -valued Function-like set
rng C is set
F₄(C,(C | C)) is set
B | C is T-Sequence-like Relation-like rng B -valued Function-like 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 epsilon-transitive epsilon-connected ordinal set
succ D is non empty epsilon-transitive epsilon-connected ordinal set
{D} is non empty set
D \/ {D} is non empty set
B . C is set
B . D is set
F₃(D,(B . D)) is set
C is epsilon-transitive epsilon-connected ordinal set
succ C is non empty epsilon-transitive epsilon-connected ordinal set
{C} is non empty set
C \/ {C} is non empty set
L2 . C is set
F₃(C,(L2 . C)) is set
C is epsilon-transitive epsilon-connected ordinal set
succ C is non empty epsilon-transitive epsilon-connected ordinal set
{C} is non empty set
C \/ {C} is non empty set
L2 . C is set
F₃(C,(L2 . C)) is set
D is epsilon-transitive epsilon-connected ordinal set
succ D is non empty epsilon-transitive epsilon-connected ordinal set
{D} is non empty set
D \/ {D} is non empty set
L2 . D is set
F₃(D,(L2 . D)) is set
dom (b | xi) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
b . (succ xi) is set
b . xi is set
F₃(xi,(b . xi)) is set
n . (succ xi) is set
a . (succ xi) is set
B is epsilon-transitive epsilon-connected ordinal set
C is T-Sequence-like Relation-like Function-like set
F₄(B,C) is set
b | (succ xi) is T-Sequence-like Relation-like rng b -valued Function-like set
rng b is set
D is epsilon-transitive epsilon-connected ordinal set
succ D is non empty epsilon-transitive epsilon-connected ordinal set
{D} is non empty set
D \/ {D} is non empty set
C . D is set
F₃(D,(C . D)) is set
D is epsilon-transitive epsilon-connected ordinal set
succ D is non empty epsilon-transitive epsilon-connected ordinal set
{D} is non empty set
D \/ {D} is non empty set
C . D is set
F₃(D,(C . D)) is set
xi is epsilon-transitive epsilon-connected ordinal set
b . xi is set
b | xi is T-Sequence-like Relation-like rng b -valued Function-like set
rng b is set
F₄(xi,(b | xi)) is set
n . xi is set
a . xi is set
B is epsilon-transitive epsilon-connected ordinal set
C is T-Sequence-like Relation-like Function-like set
D is epsilon-transitive epsilon-connected ordinal set
succ D is non empty epsilon-transitive epsilon-connected ordinal set
{D} is non empty set
D \/ {D} is non empty set
C . D is set
F₃(D,(C . D)) is set
F₄(B,C) is set
F₄() is set
F₁() is T-Sequence-like Relation-like Function-like set
dom F₁() is epsilon-transitive epsilon-connected ordinal set
F₃() is epsilon-transitive epsilon-connected ordinal set
F₁() . {} is set
n is epsilon-transitive epsilon-connected ordinal set
F₁() . n is set
F₂(n) is set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
F₁() | (succ n) is T-Sequence-like Relation-like rng F₁() -valued Function-like set
rng F₁() is set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
(F₁() | (succ n)) . (succ a) is set
(F₁() | (succ n)) . a is set
F₅(a,((F₁() | (succ n)) . a)) is set
F₁() . a is set
F₁() . (succ a) is set
a is epsilon-transitive epsilon-connected ordinal set
(F₁() | (succ n)) . a is set
(F₁() | (succ n)) | a is T-Sequence-like Relation-like rng (F₁() | (succ n)) -valued Function-like set
rng (F₁() | (succ n)) is set
F₆(a,((F₁() | (succ n)) | a)) is set
F₁() | a is T-Sequence-like Relation-like rng F₁() -valued Function-like set
F₁() . a is set
(F₁() | (succ n)) . {} is set
dom (F₁() | (succ n)) is epsilon-transitive epsilon-connected ordinal set
((F₁() | (succ n))) is set
union (dom (F₁() | (succ n))) is epsilon-transitive epsilon-connected ordinal set
(F₁() | (succ n)) . (union (dom (F₁() | (succ n)))) is set
(F₁() | (succ n)) . n is set
F₁() is epsilon-transitive epsilon-connected ordinal set
succ F₁() is non empty epsilon-transitive epsilon-connected ordinal set
{F₁()} is non empty set
F₁() \/ {F₁()} is non empty set
F₂() is set
n is T-Sequence-like Relation-like Function-like set
dom n is epsilon-transitive epsilon-connected ordinal set
n . {} is set
(n) is set
union (dom n) is epsilon-transitive epsilon-connected ordinal set
n . (union (dom n)) is set
n is set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
n . (succ a) is set
n . a is set
F₃(a,(n . a)) is set
b is epsilon-transitive epsilon-connected ordinal set
n . b is set
n | b is T-Sequence-like Relation-like rng n -valued Function-like set
rng n is set
F₄(b,(n | b)) is set
n is set
a is set
b is T-Sequence-like Relation-like Function-like set
(b) is set
dom b is epsilon-transitive epsilon-connected ordinal set
union (dom b) is epsilon-transitive epsilon-connected ordinal set
b . (union (dom b)) is set
b . {} is set
xi is T-Sequence-like Relation-like Function-like set
(xi) is set
dom xi is epsilon-transitive epsilon-connected ordinal set
union (dom xi) is epsilon-transitive epsilon-connected ordinal set
xi . (union (dom xi)) is set
xi . {} is set
F₂() is set
F₁({}) is set
succ {} is non empty epsilon-transitive epsilon-connected ordinal natural set
{{}} is non empty set
{} \/ {{}} is non empty set
n is T-Sequence-like Relation-like Function-like set
dom n is epsilon-transitive epsilon-connected ordinal set
n . {} is set
(n) is set
union (dom n) is epsilon-transitive epsilon-connected ordinal set
n . (union (dom n)) is set
F₁() is set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
F₄((succ n)) is set
F₄(n) is set
F₂(n,F₄(n)) is set
succ (succ n) is non empty epsilon-transitive epsilon-connected ordinal set
{(succ n)} is non empty set
(succ n) \/ {(succ n)} is non empty set
n is T-Sequence-like Relation-like Function-like set
dom n is epsilon-transitive epsilon-connected ordinal set
n . {} is set
b is set
a is epsilon-transitive epsilon-connected ordinal set
F₄(a) is set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
B is set
C is T-Sequence-like Relation-like Function-like set
(C) is set
dom C is epsilon-transitive epsilon-connected ordinal set
union (dom C) is epsilon-transitive epsilon-connected ordinal set
C . (union (dom C)) is set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
C . {} is set
F₄(xi) is set
n . (succ n) is set
n . n is set
F₄() is set
F₂() is epsilon-transitive epsilon-connected ordinal set
F₁() is T-Sequence-like Relation-like Function-like set
dom F₁() is epsilon-transitive epsilon-connected ordinal set
F₃(F₂()) is set
F₆(F₂(),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
n is T-Sequence-like Relation-like Function-like set
dom n is epsilon-transitive epsilon-connected ordinal set
n . {} is set
n | F₂() is T-Sequence-like Relation-like rng n -valued Function-like set
rng n is set
b is set
a is epsilon-transitive epsilon-connected ordinal set
F₃(a) is set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
B is set
C is T-Sequence-like Relation-like Function-like set
(C) is set
dom C is epsilon-transitive epsilon-connected ordinal set
union (dom C) is epsilon-transitive epsilon-connected ordinal set
C . (union (dom C)) is set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
C . {} is set
F₃(xi) is set
a is set
(n | F₂()) . a is set
b is epsilon-transitive epsilon-connected ordinal set
n . b is set
F₃(b) is set
F₁() . a is set
dom (n | F₂()) is epsilon-transitive epsilon-connected ordinal set
n . F₂() is set
F₁() is epsilon-transitive epsilon-connected ordinal set
F₂() is epsilon-transitive epsilon-connected ordinal set
n is T-Sequence-like Relation-like Function-like set
dom n is epsilon-transitive epsilon-connected ordinal set
n . {} is set
rng n is set
((rng n)) is epsilon-transitive epsilon-connected ordinal set
n is set
a is set
n . a is set
b is epsilon-transitive epsilon-connected ordinal set
n . b is set
n | b is T-Sequence-like Relation-like rng n -valued Function-like set
F₄(b,(n | b)) is epsilon-transitive epsilon-connected ordinal set
On (rng n) is set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal 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
F₃(xi,((union {(n . xi)}))) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
n is T-Sequence-like Relation-like Function-like () set
a is T-Sequence-like Relation-like Function-like () set
dom a is epsilon-transitive epsilon-connected ordinal set
a . {} is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
a . (succ b) is epsilon-transitive epsilon-connected ordinal set
a . b is epsilon-transitive epsilon-connected ordinal set
F₃(b,(a . b)) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
union {xi} is set
((union {xi})) is epsilon-transitive epsilon-connected ordinal set
(xi) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a . b is epsilon-transitive epsilon-connected ordinal set
a | b is T-Sequence-like Relation-like rng a -valued Function-like () set
rng a is set
F₄(b,(a | b)) is epsilon-transitive epsilon-connected ordinal set
F₄() is epsilon-transitive epsilon-connected ordinal set
F₁() is T-Sequence-like Relation-like Function-like () set
dom F₁() is epsilon-transitive epsilon-connected ordinal set
F₃() is epsilon-transitive epsilon-connected ordinal set
F₁() . {} is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
F₁() . n is epsilon-transitive epsilon-connected ordinal set
F₂(n) is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
F₁() | (succ n) is T-Sequence-like Relation-like rng F₁() -valued Function-like () set
rng F₁() is set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
(F₁() | (succ n)) . (succ a) is epsilon-transitive epsilon-connected ordinal set
(F₁() | (succ n)) . a is epsilon-transitive epsilon-connected ordinal set
F₅(a,((F₁() | (succ n)) . a)) is epsilon-transitive epsilon-connected ordinal set
F₁() . a is epsilon-transitive epsilon-connected ordinal set
F₁() . (succ a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(F₁() | (succ n)) . a is epsilon-transitive epsilon-connected ordinal set
(F₁() | (succ n)) | a is T-Sequence-like Relation-like rng (F₁() | (succ n)) -valued Function-like () set
rng (F₁() | (succ n)) is set
F₆(a,((F₁() | (succ n)) | a)) is epsilon-transitive epsilon-connected ordinal set
F₁() | a is T-Sequence-like Relation-like rng F₁() -valued Function-like () set
F₁() . a is epsilon-transitive epsilon-connected ordinal set
(F₁() | (succ n)) . {} is epsilon-transitive epsilon-connected ordinal set
dom (F₁() | (succ n)) is epsilon-transitive epsilon-connected ordinal set
((F₁() | (succ n))) is set
union (dom (F₁() | (succ n))) is epsilon-transitive epsilon-connected ordinal set
(F₁() | (succ n)) . (union (dom (F₁() | (succ n)))) is epsilon-transitive epsilon-connected ordinal set
(F₁() | (succ n)) . n is epsilon-transitive epsilon-connected ordinal set
F₁() is epsilon-transitive epsilon-connected ordinal set
succ F₁() is non empty epsilon-transitive epsilon-connected ordinal set
{F₁()} is non empty set
F₁() \/ {F₁()} is non empty set
F₂() is epsilon-transitive epsilon-connected ordinal set
n is T-Sequence-like Relation-like Function-like () set
dom n is epsilon-transitive epsilon-connected ordinal set
n . {} is epsilon-transitive epsilon-connected ordinal set
(n) is set
union (dom n) is epsilon-transitive epsilon-connected ordinal set
n . (union (dom n)) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
n . (succ a) is epsilon-transitive epsilon-connected ordinal set
n . a is epsilon-transitive epsilon-connected ordinal set
F₃(a,(n . a)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
n . b is epsilon-transitive epsilon-connected ordinal set
n | b is T-Sequence-like Relation-like rng n -valued Function-like () set
rng n is set
F₄(b,(n | b)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
xi is T-Sequence-like Relation-like Function-like () set
(xi) is set
dom xi is epsilon-transitive epsilon-connected ordinal set
union (dom xi) is epsilon-transitive epsilon-connected ordinal set
xi . (union (dom xi)) is epsilon-transitive epsilon-connected ordinal set
xi . {} is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
succ B is non empty epsilon-transitive epsilon-connected ordinal set
{B} is non empty set
B \/ {B} is non empty set
xi . (succ B) is epsilon-transitive epsilon-connected ordinal set
xi . B is epsilon-transitive epsilon-connected ordinal set
{(xi . B)} is non empty set
union {(xi . B)} is set
((union {(xi . B)})) is epsilon-transitive epsilon-connected ordinal set
F₃(B,((union {(xi . B)}))) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
(C) is epsilon-transitive epsilon-connected ordinal set
B is T-Sequence-like Relation-like Function-like () set
(B) is set
dom B is epsilon-transitive epsilon-connected ordinal set
union (dom B) is epsilon-transitive epsilon-connected ordinal set
B . (union (dom B)) is epsilon-transitive epsilon-connected ordinal set
B . {} is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
B . C is epsilon-transitive epsilon-connected ordinal set
B | C is T-Sequence-like Relation-like rng B -valued Function-like () set
rng B is set
F₄(C,(B | C)) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
xi . C is epsilon-transitive epsilon-connected ordinal set
xi | C is T-Sequence-like Relation-like rng xi -valued Function-like () set
rng xi is set
F₄(C,(xi | C)) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
succ C is non empty epsilon-transitive epsilon-connected ordinal set
{C} is non empty set
C \/ {C} is non empty set
B . (succ C) is epsilon-transitive epsilon-connected ordinal set
B . C is epsilon-transitive epsilon-connected ordinal set
{(B . C)} is non empty set
union {(B . C)} is set
((union {(B . C)})) is epsilon-transitive epsilon-connected ordinal set
F₃(C,((union {(B . C)}))) is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
(D) is epsilon-transitive epsilon-connected ordinal set
F₂() is epsilon-transitive epsilon-connected ordinal set
F₁({}) is epsilon-transitive epsilon-connected ordinal set
succ {} is non empty epsilon-transitive epsilon-connected ordinal natural set
{{}} is non empty set
{} \/ {{}} is non empty set
n is T-Sequence-like Relation-like Function-like () set
dom n is epsilon-transitive epsilon-connected ordinal set
n . {} is epsilon-transitive epsilon-connected ordinal set
(n) is set
union (dom n) is epsilon-transitive epsilon-connected ordinal set
n . (union (dom n)) is epsilon-transitive epsilon-connected ordinal set
F₁() is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
F₄((succ n)) is epsilon-transitive epsilon-connected ordinal set
F₄(n) is epsilon-transitive epsilon-connected ordinal set
F₂(n,F₄(n)) is epsilon-transitive epsilon-connected ordinal set
succ (succ n) is non empty epsilon-transitive epsilon-connected ordinal set
{(succ n)} is non empty set
(succ n) \/ {(succ n)} is non empty set
n is T-Sequence-like Relation-like Function-like () set
dom n is epsilon-transitive epsilon-connected ordinal set
n . {} is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
F₄(a) is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
B is epsilon-transitive epsilon-connected ordinal set
C is T-Sequence-like Relation-like Function-like () set
(C) is set
dom C is epsilon-transitive epsilon-connected ordinal set
union (dom C) is epsilon-transitive epsilon-connected ordinal set
C . (union (dom C)) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
C . {} is epsilon-transitive epsilon-connected ordinal set
F₄(xi) is epsilon-transitive epsilon-connected ordinal set
n . (succ n) is epsilon-transitive epsilon-connected ordinal set
n . n is epsilon-transitive epsilon-connected ordinal set
F₄() is epsilon-transitive epsilon-connected ordinal set
F₂() is epsilon-transitive epsilon-connected ordinal set
F₁() is T-Sequence-like Relation-like Function-like () set
dom F₁() is epsilon-transitive epsilon-connected ordinal set
F₃(F₂()) is epsilon-transitive epsilon-connected ordinal set
F₆(F₂(),F₁()) is epsilon-transitive epsilon-connected ordinal set
succ F₂() is non empty epsilon-transitive epsilon-connected ordinal set
{F₂()} is non empty set
F₂() \/ {F₂()} is non empty set
n is T-Sequence-like Relation-like Function-like () set
dom n is epsilon-transitive epsilon-connected ordinal set
n . {} is epsilon-transitive epsilon-connected ordinal set
n | F₂() is T-Sequence-like Relation-like rng n -valued Function-like () set
rng n is set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
F₃(a) is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
B is epsilon-transitive epsilon-connected ordinal set
C is T-Sequence-like Relation-like Function-like () set
(C) is set
dom C is epsilon-transitive epsilon-connected ordinal set
union (dom C) is epsilon-transitive epsilon-connected ordinal set
C . (union (dom C)) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
C . {} is epsilon-transitive epsilon-connected ordinal set
F₃(xi) is epsilon-transitive epsilon-connected ordinal set
a is set
(n | F₂()) . a is set
b is epsilon-transitive epsilon-connected ordinal set
n . b is epsilon-transitive epsilon-connected ordinal set
F₃(b) is epsilon-transitive epsilon-connected ordinal set
F₁() . a is set
dom (n | F₂()) is epsilon-transitive epsilon-connected ordinal set
n . F₂() is epsilon-transitive epsilon-connected ordinal set
n is T-Sequence-like Relation-like Function-like set
rng n is set
((rng n)) is epsilon-transitive epsilon-connected ordinal set
((rng n)) is epsilon-transitive epsilon-connected ordinal set
On (rng n) is set
meet (On (rng n)) is set
n is T-Sequence-like Relation-like Function-like set
(n) is epsilon-transitive epsilon-connected ordinal set
rng n is set
((rng n)) is epsilon-transitive epsilon-connected ordinal set
n is T-Sequence-like Relation-like Function-like set
(n) is epsilon-transitive epsilon-connected ordinal set
rng n is set
((rng n)) is epsilon-transitive epsilon-connected ordinal set
On (rng n) is set
meet (On (rng n)) is set
n is T-Sequence-like Relation-like Function-like set
dom n is epsilon-transitive epsilon-connected ordinal set
n is T-Sequence-like Relation-like Function-like () set
dom n is epsilon-transitive epsilon-connected ordinal set
(n) is epsilon-transitive epsilon-connected ordinal set
rng n is set
((rng n)) is epsilon-transitive epsilon-connected ordinal set
On (rng n) is set
meet (On (rng n)) is set
a is epsilon-transitive epsilon-connected ordinal set
n . a is epsilon-transitive epsilon-connected ordinal 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
n is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is T-Sequence-like Relation-like Function-like () set
(b) is epsilon-transitive epsilon-connected ordinal set
rng b is set
((rng b)) is epsilon-transitive epsilon-connected ordinal set
On (rng b) is set
meet (On (rng b)) is set
dom b is epsilon-transitive epsilon-connected ordinal set
xi is T-Sequence-like Relation-like Function-like () set
(xi) is epsilon-transitive epsilon-connected ordinal set
rng xi is set
((rng xi)) is epsilon-transitive epsilon-connected ordinal set
On (rng xi) is set
meet (On (rng xi)) is set
dom xi is epsilon-transitive epsilon-connected ordinal set
B is set
C is epsilon-transitive epsilon-connected ordinal set
b . C is epsilon-transitive epsilon-connected ordinal 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
n is T-Sequence-like Relation-like Function-like () set
dom n is epsilon-transitive epsilon-connected ordinal set
(n) is epsilon-transitive epsilon-connected ordinal set
rng n is set
((rng n)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
n . a is epsilon-transitive epsilon-connected ordinal 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
n is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is T-Sequence-like Relation-like Function-like () set
(b) is epsilon-transitive epsilon-connected ordinal set
rng b is set
((rng b)) is epsilon-transitive epsilon-connected ordinal set
dom b is epsilon-transitive epsilon-connected ordinal set
xi is T-Sequence-like Relation-like Function-like () set
(xi) is epsilon-transitive epsilon-connected ordinal set
rng xi is set
((rng xi)) is epsilon-transitive epsilon-connected ordinal set
dom xi is epsilon-transitive epsilon-connected ordinal set
B is set
C is epsilon-transitive epsilon-connected ordinal set
b . C is epsilon-transitive epsilon-connected ordinal 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
n is T-Sequence-like Relation-like Function-like () set
n is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
dom n is epsilon-transitive epsilon-connected ordinal set
the epsilon-transitive epsilon-connected ordinal Element of a is epsilon-transitive epsilon-connected ordinal Element of a
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
C is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
E is epsilon-transitive epsilon-connected ordinal set
n . E is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
D is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
E is epsilon-transitive epsilon-connected ordinal set
n . E is epsilon-transitive epsilon-connected ordinal set
the epsilon-transitive epsilon-connected ordinal Element of b is epsilon-transitive epsilon-connected ordinal Element of b
C is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
E is epsilon-transitive epsilon-connected ordinal set
n . E is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
E is epsilon-transitive epsilon-connected ordinal set
n . E is epsilon-transitive epsilon-connected ordinal set
n is T-Sequence-like Relation-like Function-like () set
n is epsilon-transitive epsilon-connected ordinal set
n | n is T-Sequence-like Relation-like rng n -valued Function-like () set
rng n is set
((n | n)) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
xi is T-Sequence-like Relation-like Function-like () set
(xi) is set
dom xi is epsilon-transitive epsilon-connected ordinal set
union (dom xi) is epsilon-transitive epsilon-connected ordinal set
xi . (union (dom xi)) is epsilon-transitive epsilon-connected ordinal set
xi . {} is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
B is T-Sequence-like Relation-like Function-like () set
(B) is set
dom B is epsilon-transitive epsilon-connected ordinal set
union (dom B) is epsilon-transitive epsilon-connected ordinal set
B . (union (dom B)) is epsilon-transitive epsilon-connected ordinal set
B . {} is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
D is T-Sequence-like Relation-like Function-like () set
(D) is set
dom D is epsilon-transitive epsilon-connected ordinal set
union (dom D) is epsilon-transitive epsilon-connected ordinal set
D . (union (dom D)) is epsilon-transitive epsilon-connected ordinal set
D . {} is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
xi is T-Sequence-like Relation-like Function-like () set
(xi) is set
dom xi is epsilon-transitive epsilon-connected ordinal set
union (dom xi) is epsilon-transitive epsilon-connected ordinal set
xi . (union (dom xi)) is epsilon-transitive epsilon-connected ordinal set
xi . {} is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
B is T-Sequence-like Relation-like Function-like () set
(B) is set
dom B is epsilon-transitive epsilon-connected ordinal set
union (dom B) is epsilon-transitive epsilon-connected ordinal set
B . (union (dom B)) is epsilon-transitive epsilon-connected ordinal set
B . {} is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
D is T-Sequence-like Relation-like Function-like () set
(D) is set
dom D is epsilon-transitive epsilon-connected ordinal set
union (dom D) is epsilon-transitive epsilon-connected ordinal set
D . (union (dom D)) is epsilon-transitive epsilon-connected ordinal set
D . {} is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal Element of n
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
1 is non empty epsilon-transitive epsilon-connected ordinal natural Element of omega
n is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
xi is T-Sequence-like Relation-like Function-like () set
(xi) is set
dom xi is epsilon-transitive epsilon-connected ordinal set
union (dom xi) is epsilon-transitive epsilon-connected ordinal set
xi . (union (dom xi)) is epsilon-transitive epsilon-connected ordinal set
xi . {} is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
B is T-Sequence-like Relation-like Function-like () set
(B) is set
dom B is epsilon-transitive epsilon-connected ordinal set
union (dom B) is epsilon-transitive epsilon-connected ordinal set
B . (union (dom B)) is epsilon-transitive epsilon-connected ordinal set
B . {} is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
D is T-Sequence-like Relation-like Function-like () set
(D) is set
dom D is epsilon-transitive epsilon-connected ordinal set
union (dom D) is epsilon-transitive epsilon-connected ordinal set
D . (union (dom D)) is epsilon-transitive epsilon-connected ordinal set
D . {} is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(n,{}) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(n,n) is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
xi is epsilon-transitive epsilon-connected ordinal set
B is T-Sequence-like Relation-like Function-like () set
(B) is set
dom B is epsilon-transitive epsilon-connected ordinal set
union (dom B) is epsilon-transitive epsilon-connected ordinal set
B . (union (dom B)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
B . {} is epsilon-transitive epsilon-connected ordinal set
(n,b) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
(n,(succ n)) is epsilon-transitive epsilon-connected ordinal set
(n,n) is epsilon-transitive epsilon-connected ordinal 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
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(n,a) is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
B is epsilon-transitive epsilon-connected ordinal set
C is T-Sequence-like Relation-like Function-like () set
(C) is set
dom C is epsilon-transitive epsilon-connected ordinal set
union (dom C) is epsilon-transitive epsilon-connected ordinal set
C . (union (dom C)) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
C . {} is epsilon-transitive epsilon-connected ordinal set
(n,xi) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(n,n) 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) is epsilon-transitive epsilon-connected ordinal set
rng a is set
((rng a)) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(n,b) is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
C is epsilon-transitive epsilon-connected ordinal set
D is T-Sequence-like Relation-like Function-like () set
(D) is set
dom D is epsilon-transitive epsilon-connected ordinal set
union (dom D) is epsilon-transitive epsilon-connected ordinal set
D . (union (dom D)) is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
succ B is non empty epsilon-transitive epsilon-connected ordinal set
{B} is non empty set
B \/ {B} is non empty set
D . {} is epsilon-transitive epsilon-connected ordinal set
(n,B) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
({},n) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
({},n) is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
({},(succ n)) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
({},n) 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
rng a is set
b is set
xi is set
a . xi is set
B is epsilon-transitive epsilon-connected ordinal set
({},B) is epsilon-transitive epsilon-connected ordinal set
b is set
xi is epsilon-transitive epsilon-connected ordinal set
({},xi) is epsilon-transitive epsilon-connected ordinal set
a . xi is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
((rng a)) is epsilon-transitive epsilon-connected ordinal set
({},{}) is epsilon-transitive epsilon-connected ordinal set
succ {} is non empty epsilon-transitive epsilon-connected ordinal natural set
{{}} is non empty set
{} \/ {{}} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
(n,1) is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
(n,{}) is epsilon-transitive epsilon-connected ordinal set
succ (n,{}) is non empty epsilon-transitive epsilon-connected ordinal set
{(n,{})} is non empty set
(n,{}) \/ {(n,{})} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,n) is epsilon-transitive epsilon-connected ordinal set
(a,n) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(a,b) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
(a,xi) is epsilon-transitive epsilon-connected ordinal 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
(a,(succ xi)) is epsilon-transitive epsilon-connected ordinal set
xi is T-Sequence-like Relation-like Function-like () set
dom xi is epsilon-transitive epsilon-connected ordinal set
xi . n is epsilon-transitive epsilon-connected ordinal set
rng xi is set
(xi) is epsilon-transitive epsilon-connected ordinal set
((rng xi)) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,n) is epsilon-transitive epsilon-connected ordinal set
(a,n) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(n,a) is epsilon-transitive epsilon-connected ordinal set
(n,a) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(n,b) is epsilon-transitive epsilon-connected ordinal set
(n,b) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
(n,xi) is epsilon-transitive epsilon-connected ordinal 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
(n,xi) is epsilon-transitive epsilon-connected ordinal 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
xi is T-Sequence-like Relation-like Function-like () set
dom xi is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
rng xi is set
C is set
xi . C is set
D is epsilon-transitive epsilon-connected ordinal set
(n,D) is epsilon-transitive epsilon-connected ordinal set
(n,D) is epsilon-transitive epsilon-connected ordinal set
(xi) is epsilon-transitive epsilon-connected ordinal set
((rng xi)) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
({},n) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(n,n) is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
xi is epsilon-transitive epsilon-connected ordinal set
B is T-Sequence-like Relation-like Function-like () set
(B) is set
dom B is epsilon-transitive epsilon-connected ordinal set
union (dom B) is epsilon-transitive epsilon-connected ordinal set
B . (union (dom B)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
B . {} is epsilon-transitive epsilon-connected ordinal set
(b,n) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
((succ n),n) is epsilon-transitive epsilon-connected ordinal set
(n,n) is epsilon-transitive epsilon-connected ordinal set
((n,n),n) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,n) is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
B is epsilon-transitive epsilon-connected ordinal set
C is T-Sequence-like Relation-like Function-like () set
(C) is set
dom C is epsilon-transitive epsilon-connected ordinal set
union (dom C) is epsilon-transitive epsilon-connected ordinal set
C . (union (dom C)) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
C . {} is epsilon-transitive epsilon-connected ordinal set
(xi,n) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(n,n) 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) is epsilon-transitive epsilon-connected ordinal set
rng a is set
((rng a)) is epsilon-transitive epsilon-connected ordinal set
union (a) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(b,n) is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
C is epsilon-transitive epsilon-connected ordinal set
D is T-Sequence-like Relation-like Function-like () set
(D) is set
dom D is epsilon-transitive epsilon-connected ordinal set
union (dom D) is epsilon-transitive epsilon-connected ordinal set
D . (union (dom D)) is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
succ B is non empty epsilon-transitive epsilon-connected ordinal set
{B} is non empty set
B \/ {B} is non empty set
D . {} is epsilon-transitive epsilon-connected ordinal set
(B,n) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(n,{}) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(n,{}) is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
((succ n),{}) is epsilon-transitive epsilon-connected ordinal set
({},{}) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(n,{}) 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
rng a is set
b is set
xi is set
a . xi is set
B is epsilon-transitive epsilon-connected ordinal set
(B,{}) is epsilon-transitive epsilon-connected ordinal set
b is set
({},{}) is epsilon-transitive epsilon-connected ordinal set
a . b is set
((rng a)) is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
union (a) is epsilon-transitive epsilon-connected ordinal set
union ((rng a)) is epsilon-transitive epsilon-connected ordinal set
({},{}) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(1,n) is epsilon-transitive epsilon-connected ordinal set
(n,1) is epsilon-transitive epsilon-connected ordinal set
({},n) is epsilon-transitive epsilon-connected ordinal set
(({},n),n) is epsilon-transitive epsilon-connected ordinal set
({},n) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(n,(succ {})) 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
rng a is set
b is set
xi is epsilon-transitive epsilon-connected ordinal set
(xi,(succ {})) is epsilon-transitive epsilon-connected ordinal set
a . b is set
b is set
xi is set
a . xi is set
B is epsilon-transitive epsilon-connected ordinal set
a . B is epsilon-transitive epsilon-connected ordinal set
(B,(succ {})) is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
((rng a)) is epsilon-transitive epsilon-connected ordinal set
union (a) is epsilon-transitive epsilon-connected ordinal set
union ((rng a)) is epsilon-transitive epsilon-connected ordinal set
union n is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
(a,(succ {})) is epsilon-transitive epsilon-connected ordinal set
((a,(succ {})),(succ {})) is epsilon-transitive epsilon-connected ordinal set
(a,(succ {})) is epsilon-transitive epsilon-connected ordinal set
(a,{}) is epsilon-transitive epsilon-connected ordinal set
succ (a,{}) is non empty epsilon-transitive epsilon-connected ordinal set
{(a,{})} is non empty set
(a,{}) \/ {(a,{})} is non empty set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(n,n) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,n) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(b,n) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
(xi,n) is epsilon-transitive epsilon-connected ordinal set
((xi,n),{}) is epsilon-transitive epsilon-connected ordinal set
((xi,n),n) is epsilon-transitive epsilon-connected ordinal set
((succ xi),n) is epsilon-transitive epsilon-connected ordinal set
((n,n),{}) is epsilon-transitive epsilon-connected ordinal set
((n,n),n) is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
((succ n),n) is epsilon-transitive epsilon-connected ordinal set
xi is T-Sequence-like Relation-like Function-like () set
dom xi is epsilon-transitive epsilon-connected ordinal set
xi . (succ n) is epsilon-transitive epsilon-connected ordinal set
rng xi is set
((rng xi)) is epsilon-transitive epsilon-connected ordinal set
union ((rng xi)) is epsilon-transitive epsilon-connected ordinal set
(xi) is epsilon-transitive epsilon-connected ordinal set
union (xi) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(n,a) is epsilon-transitive epsilon-connected ordinal set
(n,a) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,n) is epsilon-transitive epsilon-connected ordinal set
(a,n) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(b,n) is epsilon-transitive epsilon-connected ordinal set
(b,n) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
(xi,n) is epsilon-transitive epsilon-connected ordinal set
(xi,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
((xi,n),n) is epsilon-transitive epsilon-connected ordinal set
xi is T-Sequence-like Relation-like Function-like () set
dom xi is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
rng xi is set
C is set
xi . C is set
D is epsilon-transitive epsilon-connected ordinal set
(D,n) is epsilon-transitive epsilon-connected ordinal set
(D,n) is epsilon-transitive epsilon-connected ordinal set
((rng xi)) is epsilon-transitive epsilon-connected ordinal set
(xi) is epsilon-transitive epsilon-connected ordinal set
union (xi) is epsilon-transitive epsilon-connected ordinal set
union ((rng xi)) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
(n,{}) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(n,n) is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
xi is epsilon-transitive epsilon-connected ordinal set
B is T-Sequence-like Relation-like Function-like () set
(B) is set
dom B is epsilon-transitive epsilon-connected ordinal set
union (dom B) is epsilon-transitive epsilon-connected ordinal set
B . (union (dom B)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
B . {} is epsilon-transitive epsilon-connected ordinal set
(n,b) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
(n,(succ n)) is epsilon-transitive epsilon-connected ordinal set
(n,n) is epsilon-transitive epsilon-connected ordinal set
(n,(n,n)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(n,a) is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
{a} is non empty set
a \/ {a} is non empty set
B is epsilon-transitive epsilon-connected ordinal set
C is T-Sequence-like Relation-like Function-like () set
(C) is set
dom C is epsilon-transitive epsilon-connected ordinal set
union (dom C) is epsilon-transitive epsilon-connected ordinal set
C . (union (dom C)) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
succ xi is non empty epsilon-transitive epsilon-connected ordinal set
{xi} is non empty set
xi \/ {xi} is non empty set
C . {} is epsilon-transitive epsilon-connected ordinal set
(n,xi) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(n,n) 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) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(n,b) is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
C is epsilon-transitive epsilon-connected ordinal set
D is T-Sequence-like Relation-like Function-like () set
(D) is set
dom D is epsilon-transitive epsilon-connected ordinal set
union (dom D) is epsilon-transitive epsilon-connected ordinal set
D . (union (dom D)) is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
succ B is non empty epsilon-transitive epsilon-connected ordinal set
{B} is non empty set
B \/ {B} is non empty set
D . {} is epsilon-transitive epsilon-connected ordinal set
(n,B) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(n,1) is epsilon-transitive epsilon-connected ordinal set
(1,n) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(1,n) is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
(1,(succ n)) is epsilon-transitive epsilon-connected ordinal set
(1,1) is epsilon-transitive epsilon-connected ordinal set
(n,{}) is epsilon-transitive epsilon-connected ordinal set
(n,(n,{})) is epsilon-transitive epsilon-connected ordinal set
(n,1) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
(1,n) 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
rng a is set
{1} is non empty set
b is set
xi is set
a . xi is set
B is epsilon-transitive epsilon-connected ordinal set
(1,B) is epsilon-transitive epsilon-connected ordinal set
the epsilon-transitive epsilon-connected ordinal Element of n is epsilon-transitive epsilon-connected ordinal Element of n
xi is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
E is epsilon-transitive epsilon-connected ordinal set
a . E is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
(1,{}) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(a,b) is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
{b} is non empty set
b \/ {b} is non empty set
xi is non empty epsilon-transitive epsilon-connected ordinal set
(a,xi) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
a is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional set
(n,a) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
a is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(a,b) is epsilon-transitive epsilon-connected ordinal set
xi is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
(xi,B) is epsilon-transitive epsilon-connected ordinal set
n is set
n is epsilon-transitive epsilon-connected ordinal set
n --> n is Relation-like n -defined Function-like constant V24(n) V28(n,{n}) Element of bool [:n,{n}:]
{n} is non empty set
[:n,{n}:] is set
bool [:n,{n}:] is non empty set
rng (n --> n) is trivial set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
n \/ {n} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
n is set
n --> n is Relation-like n -defined Function-like constant V24(n) V28(n,{n}) Element of bool [:n,{n}:]
{n} is non empty set
[:n,{n}:] is set
bool [:n,{n}:] is non empty set
dom (n --> n) is set
a is epsilon-transitive epsilon-connected ordinal set
id a is Relation-like Function-like one-to-one set
dom (id a) is set
rng (id a) is set
b is T-Sequence-like Relation-like Function-like set
xi is T-Sequence-like Relation-like Function-like () set
dom xi is epsilon-transitive epsilon-connected ordinal set
rng xi is set
(xi) is epsilon-transitive epsilon-connected ordinal set
((rng xi)) is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
xi . B is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
xi . C is epsilon-transitive epsilon-connected ordinal set
n is T-Sequence-like Relation-like Function-like () set
rng n is set
n is set
dom n is epsilon-transitive epsilon-connected ordinal set
a is set
n . a is set
n is T-Sequence-like Relation-like Function-like () set
rng n is set
(n) is epsilon-transitive epsilon-connected ordinal set
((rng n)) is epsilon-transitive epsilon-connected ordinal set
n is set
n is epsilon-transitive epsilon-connected ordinal set
n is T-Sequence-like Relation-like Function-like () set
dom n is epsilon-transitive epsilon-connected ordinal set
rng n is set
(n) is epsilon-transitive epsilon-connected ordinal set
((rng n)) is epsilon-transitive epsilon-connected ordinal set
({}) is epsilon-transitive epsilon-connected ordinal set
F₁() is epsilon-transitive epsilon-connected ordinal natural set
n is epsilon-transitive epsilon-connected ordinal set
succ n is non empty epsilon-transitive epsilon-connected ordinal set
{n} is non empty set
n \/ {n} is non empty set
n is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal natural set
n is epsilon-transitive epsilon-connected ordinal natural set
(n,n) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal natural set
(n,a) is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal natural set
{a} is non empty set
a \/ {a} is non empty set
(n,(succ a)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal natural set
succ b is non empty epsilon-transitive epsilon-connected ordinal natural set
{b} is non empty set
b \/ {b} is non empty set
(n,{}) is epsilon-transitive epsilon-connected ordinal set
n is set
n is set
a is epsilon-transitive epsilon-connected ordinal natural set
b is epsilon-transitive epsilon-connected ordinal natural set
IFEQ (n,n,a,b) is set
F₁() is set
n is T-Sequence-like Relation-like Function-like set
dom n is epsilon-transitive epsilon-connected ordinal set
n . {} is set
n is epsilon-transitive epsilon-connected ordinal natural set
succ n is non empty epsilon-transitive epsilon-connected ordinal natural set
{n} is non empty set
n \/ {n} is non empty set
n . (succ n) is set
n . n is set
F₂(n,(n . n)) is set
F₂() is Relation-like Function-like set
dom F₂() is set
F₂() . {} is set
F₁() is set
F₃() is Relation-like Function-like set
dom F₃() is set
F₃() . {} is set
n is epsilon-transitive epsilon-connected ordinal natural set
F₂() . n is set
F₃() . n is set
succ n is non empty epsilon-transitive epsilon-connected ordinal natural set
{n} is non empty set
n \/ {n} is non empty set
F₂() . (succ n) is set
F₃() . (succ n) is set
n is epsilon-transitive epsilon-connected ordinal natural set
F₂() . n is set
F₃() . n is set
n is set
F₂() . n is set
F₃() . n is set
F₃() is Relation-like Function-like set
dom F₃() is set
F₃() . {} is set
F₁() is set
F₄() is Relation-like Function-like set
dom F₄() is set
F₄() . {} is set
n is epsilon-transitive epsilon-connected ordinal natural set
succ n is non empty epsilon-transitive epsilon-connected ordinal natural set
{n} is non empty set
n \/ {n} is non empty set
F₄() . (succ n) is set
F₄() . n is set
F₂(n,(F₄() . n)) is set
a is set
n is epsilon-transitive epsilon-connected ordinal natural set
n is set
F₂(n,n) is set
b is set
n is epsilon-transitive epsilon-connected ordinal natural set
succ n is non empty epsilon-transitive epsilon-connected ordinal natural set
{n} is non empty set
n \/ {n} is non empty set
F₃() . (succ n) is set
F₃() . n is set
F₂(n,(F₃() . n)) is set