omega is epsilon-transitive epsilon-connected ordinal non empty V33() cardinal limit_cardinal set
bool omega is V33() set
{} is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V33() cardinal {} -element set
the epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V33() cardinal {} -element set is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V33() cardinal {} -element set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() cardinal Element of omega
succ {} is epsilon-transitive epsilon-connected ordinal natural non empty V33() cardinal Element of omega
{{}} is non empty trivial 1 -element set
{} \/ {{}} is non empty set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
last 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 Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
last 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
lim D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
succ f is epsilon-transitive epsilon-connected ordinal non empty set
{f} is non empty trivial 1 -element set
f \/ {f} is non empty set
D . f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
D . g is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
D . c is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like set
dom D is epsilon-transitive epsilon-connected ordinal set
f is Relation-like T-Sequence-like Function-like set
dom f is epsilon-transitive epsilon-connected ordinal set
(dom D) +^ (dom f) is epsilon-transitive epsilon-connected ordinal set
g is Relation-like Function-like set
dom g is set
C is Relation-like T-Sequence-like Function-like set
dom C is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
C . c is set
D . c is set
c is epsilon-transitive epsilon-connected ordinal set
(dom D) +^ c is epsilon-transitive epsilon-connected ordinal set
C . ((dom D) +^ c) is set
f . c is set
((dom D) +^ c) -^ (dom D) is epsilon-transitive epsilon-connected ordinal set
f . (((dom D) +^ c) -^ (dom D)) is set
g is Relation-like T-Sequence-like Function-like set
dom g is epsilon-transitive epsilon-connected ordinal set
C is Relation-like T-Sequence-like Function-like set
dom C is epsilon-transitive epsilon-connected ordinal set
c is set
b is epsilon-transitive epsilon-connected ordinal set
g . b is set
D . b is set
g . c is set
C . c is set
b is epsilon-transitive epsilon-connected ordinal set
b -^ (dom D) is epsilon-transitive epsilon-connected ordinal set
(dom D) +^ (b -^ (dom D)) is epsilon-transitive epsilon-connected ordinal set
g . b is set
f . (b -^ (dom D)) is set
g . c is set
C . c is set
g . c is set
C . c is set
g . c is set
C . c is set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
rng D is set
f is Relation-like T-Sequence-like Function-like Ordinal-yielding set
(D,f) is Relation-like T-Sequence-like Function-like set
rng (D,f) is set
rng f is set
(rng D) \/ (rng f) is set
dom (D,f) is epsilon-transitive epsilon-connected ordinal set
dom D is epsilon-transitive epsilon-connected ordinal set
dom f is epsilon-transitive epsilon-connected ordinal set
(dom D) +^ (dom f) is epsilon-transitive epsilon-connected ordinal set
b is set
e is set
(D,f) . e is set
e is epsilon-transitive epsilon-connected ordinal set
D . e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e -^ (dom D) is epsilon-transitive epsilon-connected ordinal set
(dom D) +^ (e -^ (dom D)) is epsilon-transitive epsilon-connected ordinal set
f . (e -^ (dom D)) is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
f is Relation-like T-Sequence-like Function-like Ordinal-yielding set
(D,f) is Relation-like T-Sequence-like Function-like set
rng D is set
C is epsilon-transitive epsilon-connected ordinal set
rng f is set
c is epsilon-transitive epsilon-connected ordinal set
C +^ c is epsilon-transitive epsilon-connected ordinal set
C \/ c is epsilon-transitive epsilon-connected ordinal set
rng (D,f) is set
(rng D) \/ (rng f) is set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
f is Relation-like T-Sequence-like Function-like Ordinal-yielding set
(f,D) is Relation-like T-Sequence-like Function-like Ordinal-yielding set
g is epsilon-transitive epsilon-connected ordinal set
dom D is epsilon-transitive epsilon-connected ordinal set
dom (f,D) is epsilon-transitive epsilon-connected ordinal set
dom f is epsilon-transitive epsilon-connected ordinal set
(dom f) +^ (dom D) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
(dom f) +^ C is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(f,D) . b is epsilon-transitive epsilon-connected ordinal set
b -^ c is epsilon-transitive epsilon-connected ordinal set
c +^ (b -^ c) is epsilon-transitive epsilon-connected ordinal set
C +^ (b -^ c) is epsilon-transitive epsilon-connected ordinal set
(dom f) +^ (C +^ (b -^ c)) is epsilon-transitive epsilon-connected ordinal set
D . (C +^ (b -^ c)) 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 epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(dom f) +^ b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
(f,D) . e is epsilon-transitive epsilon-connected ordinal set
e -^ e is epsilon-transitive epsilon-connected ordinal set
b +^ (e -^ e) is epsilon-transitive epsilon-connected ordinal set
e +^ (e -^ e) is epsilon-transitive epsilon-connected ordinal set
(dom f) +^ (b +^ (e -^ e)) is epsilon-transitive epsilon-connected ordinal set
D . (b +^ (e -^ e)) is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
g +^ f is epsilon-transitive epsilon-connected ordinal set
g +^ D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
dom (g +^ D) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
(g +^ D) . c is epsilon-transitive epsilon-connected ordinal set
D . c is epsilon-transitive epsilon-connected ordinal set
g +^ (D . c) is epsilon-transitive epsilon-connected ordinal set
C 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 epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
(g +^ D) . e is epsilon-transitive epsilon-connected ordinal set
D . e is epsilon-transitive epsilon-connected ordinal set
g +^ (D . e) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
C -^ g is epsilon-transitive epsilon-connected ordinal set
c -^ g is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
g +^ (C -^ g) is epsilon-transitive epsilon-connected ordinal set
g +^ (c -^ g) is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
(g +^ D) . e is epsilon-transitive epsilon-connected ordinal set
D . e is epsilon-transitive epsilon-connected ordinal set
g +^ (D . e) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
g +^ b is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
succ f is epsilon-transitive epsilon-connected ordinal non empty set
{f} is non empty trivial 1 -element set
f \/ {f} is non empty set
g is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
f *^ g is epsilon-transitive epsilon-connected ordinal set
D *^ g is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
dom (D *^ g) is epsilon-transitive epsilon-connected ordinal set
the epsilon-transitive epsilon-connected ordinal Element of dom D is epsilon-transitive epsilon-connected ordinal Element of dom D
c is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
(D *^ g) . e is epsilon-transitive epsilon-connected ordinal set
D . e is epsilon-transitive epsilon-connected ordinal set
(D . e) *^ g 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 epsilon-transitive epsilon-connected ordinal set
(D *^ g) . b is epsilon-transitive epsilon-connected ordinal set
D . b is epsilon-transitive epsilon-connected ordinal set
(D . b) *^ g is epsilon-transitive epsilon-connected ordinal set
C 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 epsilon-transitive epsilon-connected ordinal set
b *^ g is epsilon-transitive epsilon-connected ordinal set
succ f is epsilon-transitive epsilon-connected ordinal non empty set
{f} is non empty trivial 1 -element set
f \/ {f} is non empty set
e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
D . b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e *^ g is epsilon-transitive epsilon-connected ordinal set
(D *^ g) . b is epsilon-transitive epsilon-connected ordinal set
(D . b) *^ g is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is epsilon-transitive epsilon-connected ordinal non empty set
{b} is non empty trivial 1 -element set
b \/ {b} is non empty set
e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
D . b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
(D *^ g) . b is epsilon-transitive epsilon-connected ordinal set
e *^ g is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
succ e is epsilon-transitive epsilon-connected ordinal non empty set
{e} is non empty trivial 1 -element set
e \/ {e} is non empty set
e is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
f is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
D . c is epsilon-transitive epsilon-connected ordinal set
f . c is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
succ g is epsilon-transitive epsilon-connected ordinal non empty set
{g} is non empty trivial 1 -element set
g \/ {g} is non empty set
c is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
b \/ c is epsilon-transitive epsilon-connected ordinal set
D . (b \/ c) is epsilon-transitive epsilon-connected ordinal set
f . (b \/ c) is epsilon-transitive epsilon-connected ordinal set
succ g is epsilon-transitive epsilon-connected ordinal non empty set
{g} is non empty trivial 1 -element set
g \/ {g} is non empty set
c is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
succ C is epsilon-transitive epsilon-connected ordinal non empty set
{C} is non empty trivial 1 -element set
C \/ {C} is non empty set
b is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
c \/ b is epsilon-transitive epsilon-connected ordinal set
f . (c \/ b) is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
D . (c \/ b) is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
g is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom g is epsilon-transitive epsilon-connected ordinal set
C is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom C 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 epsilon-transitive epsilon-connected ordinal set
D . b is epsilon-transitive epsilon-connected ordinal set
C . b is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e \/ e is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
D . e is epsilon-transitive epsilon-connected ordinal set
C . e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
g . e is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
sup D is epsilon-transitive epsilon-connected ordinal set
rng D is set
sup (rng D) is epsilon-transitive epsilon-connected ordinal set
lim D is epsilon-transitive epsilon-connected ordinal set
D . {} is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
g 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 set
D . b is set
e is epsilon-transitive epsilon-connected ordinal set
succ e is epsilon-transitive epsilon-connected ordinal non empty set
{e} is non empty trivial 1 -element set
e \/ {e} is non empty set
e is epsilon-transitive epsilon-connected ordinal non empty set
b is epsilon-transitive epsilon-connected ordinal set
D . b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
D . f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
D . g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
D . f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
D . g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
D . C is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
f is epsilon-transitive epsilon-connected ordinal set
D " f is set
dom D is epsilon-transitive epsilon-connected ordinal set
g is set
D . g is set
c is set
C is epsilon-transitive epsilon-connected ordinal set
D . C is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
D . b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
D . c is set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
f is Relation-like T-Sequence-like Function-like Ordinal-yielding set
D * f is Relation-like Function-like set
dom (D * f) is set
dom f is epsilon-transitive epsilon-connected ordinal set
D " (dom f) is set
rng f is set
C is epsilon-transitive epsilon-connected ordinal set
g is Relation-like T-Sequence-like Function-like set
rng g is set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
f is Relation-like T-Sequence-like Function-like Ordinal-yielding set
f * D is Relation-like Function-like set
g is Relation-like T-Sequence-like Function-like Ordinal-yielding set
C is epsilon-transitive epsilon-connected ordinal set
dom g is epsilon-transitive epsilon-connected ordinal set
g . C is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
g . c is epsilon-transitive epsilon-connected ordinal set
f . C is epsilon-transitive epsilon-connected ordinal set
f . c is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
dom D is epsilon-transitive epsilon-connected ordinal set
dom f is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
D . e is epsilon-transitive epsilon-connected ordinal set
D . b is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
f is epsilon-transitive epsilon-connected ordinal set
g is Relation-like T-Sequence-like Function-like Ordinal-yielding set
rng g is set
sup (rng g) is epsilon-transitive epsilon-connected ordinal set
C is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom C is epsilon-transitive epsilon-connected ordinal set
g * C is Relation-like Function-like set
dom D 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 epsilon-transitive epsilon-connected ordinal set
dom g is epsilon-transitive epsilon-connected ordinal set
e is set
g . e is set
e is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
D . b is epsilon-transitive epsilon-connected ordinal set
g . b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
C . e is epsilon-transitive epsilon-connected ordinal set
dom D is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
dom g is epsilon-transitive epsilon-connected ordinal set
b is set
g . b is set
e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
D . e is epsilon-transitive epsilon-connected ordinal set
g . e is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
C . c is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
f is epsilon-transitive epsilon-connected ordinal set
D | f is Relation-like rng D -valued T-Sequence-like Function-like Ordinal-yielding set
rng D is set
dom D is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
dom (D | f) is epsilon-transitive epsilon-connected ordinal set
(D | f) . g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
(D | f) . C is epsilon-transitive epsilon-connected ordinal set
D . g is epsilon-transitive epsilon-connected ordinal set
D . C is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
sup D is epsilon-transitive epsilon-connected ordinal set
rng D is set
sup (rng D) is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
C is set
D . C is set
c is epsilon-transitive epsilon-connected ordinal set
succ c is epsilon-transitive epsilon-connected ordinal non empty set
{c} is non empty trivial 1 -element set
c \/ {c} is non empty set
D . (succ c) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ g is epsilon-transitive epsilon-connected ordinal non empty set
{g} is non empty trivial 1 -element set
g \/ {g} is non empty set
succ f is epsilon-transitive epsilon-connected ordinal non empty set
{f} is non empty trivial 1 -element set
f \/ {f} is non empty set
D is Relation-like Function-like set
rng D is set
f is Relation-like Function-like set
D * f is Relation-like Function-like set
g is set
f | g is Relation-like Function-like set
D * (f | g) is Relation-like Function-like set
D " (rng D) is set
dom D is set
D " g is set
dom (D * (f | g)) is set
dom (f | g) is set
D " (dom (f | g)) is set
dom f is set
(dom f) /\ g is set
D " ((dom f) /\ g) is set
D " (dom f) is set
(D " (dom f)) /\ (D " g) is set
dom (D * f) is set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
f is Relation-like T-Sequence-like Function-like Ordinal-yielding set
D * f is Relation-like Function-like set
g is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
dom f is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
dom g is epsilon-transitive epsilon-connected ordinal set
g . C is epsilon-transitive epsilon-connected ordinal set
g | C is Relation-like rng g -valued T-Sequence-like Function-like Ordinal-yielding set
rng g is set
c is epsilon-transitive epsilon-connected ordinal set
D . C is epsilon-transitive epsilon-connected ordinal set
D | C is Relation-like rng D -valued T-Sequence-like Function-like Ordinal-yielding set
rng D is set
dom (D | C) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
lim (D | C) is epsilon-transitive epsilon-connected ordinal set
sup (D | C) is epsilon-transitive epsilon-connected ordinal set
rng (D | C) is set
sup (rng (D | C)) is epsilon-transitive epsilon-connected ordinal set
f . b is epsilon-transitive epsilon-connected ordinal set
f | b is Relation-like rng f -valued T-Sequence-like Function-like Ordinal-yielding set
rng f is set
dom (f | b) is epsilon-transitive epsilon-connected ordinal set
e is set
e is set
(D | C) . e is set
(D | C) * f is Relation-like Function-like set
(D | C) * (f | b) is Relation-like Function-like set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
D . g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
D . C is epsilon-transitive epsilon-connected ordinal set
f +^ C is epsilon-transitive epsilon-connected ordinal set
f +^ g is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
D . g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
D . C is epsilon-transitive epsilon-connected ordinal set
C *^ f is epsilon-transitive epsilon-connected ordinal set
g *^ f is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
exp ({},D) is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
exp ({},f) is epsilon-transitive epsilon-connected ordinal set
succ f is epsilon-transitive epsilon-connected ordinal non empty set
{f} is non empty trivial 1 -element set
f \/ {f} is non empty set
exp ({},(succ f)) is epsilon-transitive epsilon-connected ordinal set
{} *^ (exp ({},f)) is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
exp ({},f) is epsilon-transitive epsilon-connected ordinal set
g is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal natural non empty V33() cardinal Element of omega
c is epsilon-transitive epsilon-connected ordinal set
g . c is epsilon-transitive epsilon-connected ordinal set
exp ({},c) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
lim g is epsilon-transitive epsilon-connected ordinal set
exp ({},{}) is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal natural non empty V33() cardinal Element of omega
C is epsilon-transitive epsilon-connected ordinal set
f . C is epsilon-transitive epsilon-connected ordinal set
exp ({},C) is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like functional empty V33() cardinal {} -element set
b is epsilon-transitive epsilon-connected ordinal set
f . b is epsilon-transitive epsilon-connected ordinal set
exp (1,b) is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
C is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom C is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
exp (D,c) is epsilon-transitive epsilon-connected ordinal set
succ c is epsilon-transitive epsilon-connected ordinal non empty set
{c} is non empty trivial 1 -element set
c \/ {c} is non empty set
exp (D,(succ c)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
exp (D,b) is epsilon-transitive epsilon-connected ordinal set
1 *^ (exp (D,c)) is epsilon-transitive epsilon-connected ordinal set
D *^ (exp (D,c)) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
exp (D,c) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
exp (D,b) is epsilon-transitive epsilon-connected ordinal set
e is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom e is epsilon-transitive epsilon-connected ordinal set
e . b is epsilon-transitive epsilon-connected ordinal set
rng e is set
e is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
e . e is epsilon-transitive epsilon-connected ordinal set
e . b is epsilon-transitive epsilon-connected ordinal set
exp (D,e) is epsilon-transitive epsilon-connected ordinal set
exp (D,b) is epsilon-transitive epsilon-connected ordinal set
lim e is epsilon-transitive epsilon-connected ordinal set
sup e is epsilon-transitive epsilon-connected ordinal set
sup (rng e) is epsilon-transitive epsilon-connected ordinal set
exp (D,{}) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
exp (D,c) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
C . c is epsilon-transitive epsilon-connected ordinal set
C . b is epsilon-transitive epsilon-connected ordinal set
exp (D,c) is epsilon-transitive epsilon-connected ordinal set
exp (D,b) is epsilon-transitive epsilon-connected ordinal set
sup C is epsilon-transitive epsilon-connected ordinal set
rng C is set
sup (rng C) is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
exp (f,D) is epsilon-transitive epsilon-connected ordinal set
g is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom g is epsilon-transitive epsilon-connected ordinal set
C is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom C is epsilon-transitive epsilon-connected ordinal set
c is set
C . c is set
b is epsilon-transitive epsilon-connected ordinal set
exp (f,b) is epsilon-transitive epsilon-connected ordinal set
g . c is set
c is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
lim C is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
exp (D,f) is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
exp (D,g) is epsilon-transitive epsilon-connected ordinal set
succ g is epsilon-transitive epsilon-connected ordinal non empty set
{g} is non empty trivial 1 -element set
g \/ {g} is non empty set
exp (D,(succ g)) is epsilon-transitive epsilon-connected ordinal set
D *^ (exp (D,g)) is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
exp (D,g) is epsilon-transitive epsilon-connected ordinal set
C is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom C is epsilon-transitive epsilon-connected ordinal set
lim C 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 epsilon-transitive epsilon-connected ordinal set
C . b is epsilon-transitive epsilon-connected ordinal set
exp (D,b) is epsilon-transitive epsilon-connected ordinal set
exp (D,{}) is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
exp (D,f) is epsilon-transitive epsilon-connected ordinal set
succ f is epsilon-transitive epsilon-connected ordinal non empty set
{f} is non empty trivial 1 -element set
f \/ {f} is non empty set
exp (D,(succ f)) is epsilon-transitive epsilon-connected ordinal set
1 *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set
D *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
exp (D,f) is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
exp (D,g) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
exp (D,C) is epsilon-transitive epsilon-connected ordinal set
c is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom c is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
c . b is epsilon-transitive epsilon-connected ordinal set
c . e is epsilon-transitive epsilon-connected ordinal set
exp (D,b) is epsilon-transitive epsilon-connected ordinal set
exp (D,e) is epsilon-transitive epsilon-connected ordinal set
sup c is epsilon-transitive epsilon-connected ordinal set
rng c is set
sup (rng c) is epsilon-transitive epsilon-connected ordinal set
lim c is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
exp (D,b) is epsilon-transitive epsilon-connected ordinal set
c . b is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
exp (D,C) is epsilon-transitive epsilon-connected ordinal set
succ C is epsilon-transitive epsilon-connected ordinal non empty set
{C} is non empty trivial 1 -element set
C \/ {C} is non empty set
exp (D,(succ C)) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
exp (D,c) is epsilon-transitive epsilon-connected ordinal set
exp (D,{}) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
exp (D,C) is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
D . g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
D . C is epsilon-transitive epsilon-connected ordinal set
exp (f,C) is epsilon-transitive epsilon-connected ordinal set
exp (f,g) is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
exp (D,f) is epsilon-transitive epsilon-connected ordinal set
g is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom g is epsilon-transitive epsilon-connected ordinal set
sup g is epsilon-transitive epsilon-connected ordinal set
rng g is set
sup (rng g) is epsilon-transitive epsilon-connected ordinal set
lim g is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
exp (D,f) is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
exp (D,g) is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
exp (D,g) is epsilon-transitive epsilon-connected ordinal set
exp (f,g) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
exp (D,C) is epsilon-transitive epsilon-connected ordinal set
exp (f,C) is epsilon-transitive epsilon-connected ordinal set
succ C is epsilon-transitive epsilon-connected ordinal non empty set
{C} is non empty trivial 1 -element set
C \/ {C} is non empty set
exp (D,(succ C)) is epsilon-transitive epsilon-connected ordinal set
exp (f,(succ C)) is epsilon-transitive epsilon-connected ordinal set
f *^ (exp (f,C)) is epsilon-transitive epsilon-connected ordinal set
D *^ (exp (D,C)) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
exp (D,C) is epsilon-transitive epsilon-connected ordinal set
exp (f,C) is epsilon-transitive epsilon-connected ordinal set
c is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom c is epsilon-transitive epsilon-connected ordinal set
b is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
c . e is epsilon-transitive epsilon-connected ordinal set
exp (D,e) is epsilon-transitive epsilon-connected ordinal set
b . e is epsilon-transitive epsilon-connected ordinal set
exp (f,e) is epsilon-transitive epsilon-connected ordinal set
exp (D,{}) is epsilon-transitive epsilon-connected ordinal set
exp (f,{}) is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
exp (D,f) is epsilon-transitive epsilon-connected ordinal set
exp (D,{}) is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
exp (D,f) is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
f +^ g is epsilon-transitive epsilon-connected ordinal set
exp (D,(f +^ g)) is epsilon-transitive epsilon-connected ordinal set
exp (D,g) is epsilon-transitive epsilon-connected ordinal set
(exp (D,g)) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set
exp (D,{}) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
f +^ C is epsilon-transitive epsilon-connected ordinal set
exp (D,(f +^ C)) is epsilon-transitive epsilon-connected ordinal set
exp (D,C) is epsilon-transitive epsilon-connected ordinal set
(exp (D,C)) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set
succ C is epsilon-transitive epsilon-connected ordinal non empty set
{C} is non empty trivial 1 -element set
C \/ {C} is non empty set
f +^ (succ C) is epsilon-transitive epsilon-connected ordinal set
exp (D,(f +^ (succ C))) is epsilon-transitive epsilon-connected ordinal set
exp (D,(succ C)) is epsilon-transitive epsilon-connected ordinal set
(exp (D,(succ C))) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set
succ (f +^ C) is epsilon-transitive epsilon-connected ordinal non empty set
{(f +^ C)} is non empty trivial 1 -element set
(f +^ C) \/ {(f +^ C)} is non empty set
exp (D,(succ (f +^ C))) is epsilon-transitive epsilon-connected ordinal set
D *^ (exp (D,(f +^ C))) is epsilon-transitive epsilon-connected ordinal set
D *^ (exp (D,C)) is epsilon-transitive epsilon-connected ordinal set
(D *^ (exp (D,C))) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
f +^ C is epsilon-transitive epsilon-connected ordinal set
exp (D,(f +^ C)) is epsilon-transitive epsilon-connected ordinal set
exp (D,C) is epsilon-transitive epsilon-connected ordinal set
(exp (D,C)) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set
c is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom c is epsilon-transitive epsilon-connected ordinal set
b is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
e is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
c *^ (exp (D,f)) is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom (c *^ (exp (D,f))) is epsilon-transitive epsilon-connected ordinal set
(dom e) +^ e is epsilon-transitive epsilon-connected ordinal set
b . ((dom e) +^ e) is epsilon-transitive epsilon-connected ordinal set
f +^ e is epsilon-transitive epsilon-connected ordinal set
exp (D,(f +^ e)) is epsilon-transitive epsilon-connected ordinal set
exp (D,e) is epsilon-transitive epsilon-connected ordinal set
(exp (D,e)) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set
c . e is epsilon-transitive epsilon-connected ordinal set
(c . e) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set
(c *^ (exp (D,f))) . e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
b . e is epsilon-transitive epsilon-connected ordinal set
exp (D,e) is epsilon-transitive epsilon-connected ordinal set
e . e is epsilon-transitive epsilon-connected ordinal set
(dom e) +^ (dom (c *^ (exp (D,f)))) is epsilon-transitive epsilon-connected ordinal set
(e,(c *^ (exp (D,f)))) is Relation-like T-Sequence-like Function-like Ordinal-yielding set
lim b is epsilon-transitive epsilon-connected ordinal set
1 *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set
f +^ {} is epsilon-transitive epsilon-connected ordinal set
exp (D,(f +^ {})) is epsilon-transitive epsilon-connected ordinal set
(exp (D,{})) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
exp (D,f) is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
exp ((exp (D,f)),g) is epsilon-transitive epsilon-connected ordinal set
g *^ f is epsilon-transitive epsilon-connected ordinal set
exp (D,(g *^ f)) is epsilon-transitive epsilon-connected ordinal set
exp (D,{}) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
exp ((exp (D,f)),C) is epsilon-transitive epsilon-connected ordinal set
C *^ f is epsilon-transitive epsilon-connected ordinal set
exp (D,(C *^ f)) is epsilon-transitive epsilon-connected ordinal set
succ C is epsilon-transitive epsilon-connected ordinal non empty set
{C} is non empty trivial 1 -element set
C \/ {C} is non empty set
exp ((exp (D,f)),(succ C)) is epsilon-transitive epsilon-connected ordinal set
(succ C) *^ f is epsilon-transitive epsilon-connected ordinal set
exp (D,((succ C) *^ f)) is epsilon-transitive epsilon-connected ordinal set
(exp (D,f)) *^ (exp (D,(C *^ f))) is epsilon-transitive epsilon-connected ordinal set
(C *^ f) +^ f is epsilon-transitive epsilon-connected ordinal set
exp (D,((C *^ f) +^ f)) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
exp ((exp (D,f)),C) is epsilon-transitive epsilon-connected ordinal set
C *^ f is epsilon-transitive epsilon-connected ordinal set
exp (D,(C *^ f)) is epsilon-transitive epsilon-connected ordinal set
c is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom c is epsilon-transitive epsilon-connected ordinal set
b is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
e is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom e is epsilon-transitive epsilon-connected ordinal set
rng b is set
e is set
b is set
b . b is set
e is epsilon-transitive epsilon-connected ordinal set
e *^ f is epsilon-transitive epsilon-connected ordinal set
sup (rng b) is epsilon-transitive epsilon-connected ordinal set
sup (dom e) is epsilon-transitive epsilon-connected ordinal set
e is set
b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e *^ f is epsilon-transitive epsilon-connected ordinal set
b . e is epsilon-transitive epsilon-connected ordinal set
b * e is Relation-like Function-like set
dom (b * e) is set
e is set
b is epsilon-transitive epsilon-connected ordinal set
b . b is epsilon-transitive epsilon-connected ordinal set
b *^ f is epsilon-transitive epsilon-connected ordinal set
e is set
b is epsilon-transitive epsilon-connected ordinal set
b . b is epsilon-transitive epsilon-connected ordinal set
b *^ f is epsilon-transitive epsilon-connected ordinal set
c . e is set
exp ((exp (D,f)),b) is epsilon-transitive epsilon-connected ordinal set
exp (D,(b *^ f)) is epsilon-transitive epsilon-connected ordinal set
e . (b . b) is epsilon-transitive epsilon-connected ordinal set
(b * e) . e is set
lim c is epsilon-transitive epsilon-connected ordinal set
C *^ {} is epsilon-transitive epsilon-connected ordinal set
exp ((exp (D,f)),{}) is epsilon-transitive epsilon-connected ordinal set
{} *^ f is epsilon-transitive epsilon-connected ordinal set
exp (D,({} *^ f)) is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
exp (D,f) is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
exp (D,g) is epsilon-transitive epsilon-connected ordinal set
succ g is epsilon-transitive epsilon-connected ordinal non empty set
{g} is non empty trivial 1 -element set
g \/ {g} is non empty set
exp (D,(succ g)) is epsilon-transitive epsilon-connected ordinal set
1 *^ (exp (D,g)) is epsilon-transitive epsilon-connected ordinal set
D *^ (exp (D,g)) is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
exp (D,g) is epsilon-transitive epsilon-connected ordinal set
C is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom C is epsilon-transitive epsilon-connected ordinal set
c is set
b is epsilon-transitive epsilon-connected ordinal set
C . b is epsilon-transitive epsilon-connected ordinal set
exp (D,b) is epsilon-transitive epsilon-connected ordinal set
rng C is set
sup C is epsilon-transitive epsilon-connected ordinal set
sup (rng C) is epsilon-transitive epsilon-connected ordinal set
lim C is epsilon-transitive epsilon-connected ordinal set
exp (D,{}) is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
F1(D) is epsilon-transitive epsilon-connected ordinal set
F1(F1(D)) is epsilon-transitive epsilon-connected ordinal set
F1({}) is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
D . {} is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
F1(f) is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
D . f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
D . g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
f +^ C is epsilon-transitive epsilon-connected ordinal set
D . (f +^ C) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
f +^ C is epsilon-transitive epsilon-connected ordinal set
D . (f +^ C) is epsilon-transitive epsilon-connected ordinal set
succ C is epsilon-transitive epsilon-connected ordinal non empty set
{C} is non empty trivial 1 -element set
C \/ {C} is non empty set
f +^ (succ C) is epsilon-transitive epsilon-connected ordinal set
D . (f +^ (succ C)) is epsilon-transitive epsilon-connected ordinal set
succ (f +^ C) is epsilon-transitive epsilon-connected ordinal non empty set
{(f +^ C)} is non empty trivial 1 -element set
(f +^ C) \/ {(f +^ C)} is non empty set
c is epsilon-transitive epsilon-connected ordinal set
F1(c) is epsilon-transitive epsilon-connected ordinal set
f +^ {} is epsilon-transitive epsilon-connected ordinal set
D . (f +^ {}) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
f +^ C is epsilon-transitive epsilon-connected ordinal set
sup D is epsilon-transitive epsilon-connected ordinal set
rng D is set
sup (rng D) is epsilon-transitive epsilon-connected ordinal set
f is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom f is epsilon-transitive epsilon-connected ordinal set
F1((sup D)) is epsilon-transitive epsilon-connected ordinal set
sup f is epsilon-transitive epsilon-connected ordinal set
rng f is set
sup (rng f) is epsilon-transitive epsilon-connected ordinal set
g is set
C is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
b is set
f . b is set
e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
F1(e) is epsilon-transitive epsilon-connected ordinal set
F1(e) is epsilon-transitive epsilon-connected ordinal set
b is set
D . b is set
e is epsilon-transitive epsilon-connected ordinal set
succ e is epsilon-transitive epsilon-connected ordinal non empty set
{e} is non empty trivial 1 -element set
e \/ {e} is non empty set
D . (succ e) is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
f . g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
f . C is epsilon-transitive epsilon-connected ordinal set
F1(C) is epsilon-transitive epsilon-connected ordinal set
F1(g) is epsilon-transitive epsilon-connected ordinal set
lim f is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive non empty V41() V42() universal set
On D is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive non empty V41() V42() universal set
On D is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive non empty V41() V42() universal set
On D is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive non empty V41() V42() universal set
On D is epsilon-transitive epsilon-connected ordinal non empty set
[:(On D),(On D):] is set
bool [:(On D),(On D):] is set
f is Relation-like On D -defined On D -valued Function-like V25( On D, On D) Element of bool [:(On D),(On D):]
dom f is set
rng f is set
F1() is epsilon-transitive non empty V41() V42() universal set
On F1() is epsilon-transitive epsilon-connected ordinal non empty set
[:(On F1()),(On F1()):] is set
bool [:(On F1()),(On F1()):] is set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
rng D is set
f is set
g is set
D . g is set
C is epsilon-transitive epsilon-connected ordinal set
F2(C) is epsilon-transitive epsilon-connected ordinal Element of F1()
f is Relation-like On F1() -defined On F1() -valued T-Sequence-like Function-like V25( On F1(), On F1()) Ordinal-yielding Element of bool [:(On F1()),(On F1()):]
g is epsilon-transitive epsilon-connected ordinal Element of F1()
f . g is epsilon-transitive epsilon-connected ordinal set
F2(g) is epsilon-transitive epsilon-connected ordinal Element of F1()
D is epsilon-transitive non empty V41() V42() universal set
On D is epsilon-transitive epsilon-connected ordinal non empty set
f is epsilon-transitive epsilon-connected ordinal Element of D
On D is epsilon-transitive epsilon-connected ordinal non empty set
f is epsilon-transitive epsilon-connected ordinal Element of D
On D is epsilon-transitive epsilon-connected ordinal non empty set
[:(On D),(On D):] is set
bool [:(On D),(On D):] is set
f is Relation-like On D -defined On D -valued T-Sequence-like Function-like V25( On D, On D) Ordinal-yielding Element of bool [:(On D),(On D):]
g is epsilon-transitive epsilon-connected ordinal Element of D
f . g is epsilon-transitive epsilon-connected ordinal set
dom f is epsilon-transitive epsilon-connected ordinal set
rng f is set
C is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive non empty V41() V42() universal set
On D is epsilon-transitive epsilon-connected ordinal non empty set
[:(On D),(On D):] is set
bool [:(On D),(On D):] is set
f is Relation-like On D -defined On D -valued T-Sequence-like Function-like V25( On D, On D) Ordinal-yielding Element of bool [:(On D),(On D):]
g is Relation-like On D -defined On D -valued T-Sequence-like Function-like V25( On D, On D) Ordinal-yielding Element of bool [:(On D),(On D):]
f * g is Relation-like Function-like set
rng f is set
dom f is epsilon-transitive epsilon-connected ordinal set
dom g is epsilon-transitive epsilon-connected ordinal set
dom (f * g) is set
rng g is set
rng (f * g) is set
C is Relation-like T-Sequence-like Function-like set
rng C is set
D is epsilon-transitive non empty V41() V42() universal set
(D) is epsilon-transitive epsilon-connected ordinal Element of D
f is epsilon-transitive non empty V41() V42() universal set
(f) is epsilon-transitive epsilon-connected ordinal non empty Element of f
D is epsilon-transitive non empty V41() V42() universal set
f is epsilon-transitive epsilon-connected ordinal Element of D
succ f is epsilon-transitive epsilon-connected ordinal non empty set
{f} is non empty trivial 1 -element set
f \/ {f} is non empty set
g is epsilon-transitive epsilon-connected ordinal Element of D
f +^ g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
f +^ C is epsilon-transitive epsilon-connected ordinal set
(D) is epsilon-transitive epsilon-connected ordinal non empty Element of D
{(D)} is non empty trivial 1 -element Element of D
[:C,{(D)}:] is set
(D) is epsilon-transitive epsilon-connected ordinal Element of D
{(D)} is non empty trivial 1 -element Element of D
[:f,{(D)}:] is Element of D
[:f,{(D)}:] \/ [:C,{(D)}:] is set
card ([:f,{(D)}:] \/ [:C,{(D)}:]) is epsilon-transitive epsilon-connected ordinal cardinal set
card D is epsilon-transitive epsilon-connected ordinal non empty cardinal set
c is set
b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
f +^ e is epsilon-transitive epsilon-connected ordinal set
card (f +^ C) is epsilon-transitive epsilon-connected ordinal cardinal set
D is epsilon-transitive non empty V41() V42() universal set
f is epsilon-transitive epsilon-connected ordinal Element of D
g is epsilon-transitive epsilon-connected ordinal Element of D
f *^ g is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
C *^ g is epsilon-transitive epsilon-connected ordinal set
[:C,g:] is set
card [:C,g:] is epsilon-transitive epsilon-connected ordinal cardinal set
card D is epsilon-transitive epsilon-connected ordinal non empty cardinal set
c is set
b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e *^ g is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
(e *^ g) +^ e is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal Element of D
e is epsilon-transitive epsilon-connected ordinal Element of D
(D,b,e) is epsilon-transitive epsilon-connected ordinal Element of D
card (C *^ g) is epsilon-transitive epsilon-connected ordinal cardinal set
D is epsilon-transitive non empty V41() V42() universal set
On D is epsilon-transitive epsilon-connected ordinal non empty set
[:(On D),(On D):] is set
bool [:(On D),(On D):] is set
f is epsilon-transitive epsilon-connected ordinal Element of D
g is Relation-like On D -defined On D -valued T-Sequence-like Function-like V25( On D, On D) Ordinal-yielding Element of bool [:(On D),(On D):]
dom g is epsilon-transitive epsilon-connected ordinal set
D is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom D is epsilon-transitive epsilon-connected ordinal set
rng D is set
sup D is epsilon-transitive epsilon-connected ordinal set
sup (rng D) is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive non empty V41() V42() universal set
g is set
C is epsilon-transitive epsilon-connected ordinal set
union (rng D) is set
D .: (dom D) is set
g is epsilon-transitive epsilon-connected ordinal set
succ g is epsilon-transitive epsilon-connected ordinal non empty set
{g} is non empty trivial 1 -element set
g \/ {g} is non empty set
C is set
c is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
card (dom D) is epsilon-transitive epsilon-connected ordinal cardinal set
card f is epsilon-transitive epsilon-connected ordinal non empty cardinal set
card (rng D) is epsilon-transitive epsilon-connected ordinal cardinal set
D is epsilon-transitive non empty V41() V42() universal set
On D is epsilon-transitive epsilon-connected ordinal non empty set
[:(On D),(On D):] is set
bool [:(On D),(On D):] is set
f is Relation-like On D -defined On D -valued T-Sequence-like Function-like V25( On D, On D) Ordinal-yielding Element of bool [:(On D),(On D):]
dom f is epsilon-transitive epsilon-connected ordinal set
(D) is epsilon-transitive epsilon-connected ordinal Element of D
(D,f,(D)) is epsilon-transitive epsilon-connected ordinal Element of D
g is epsilon-transitive epsilon-connected ordinal set
C is Relation-like T-Sequence-like Function-like set
dom C is epsilon-transitive epsilon-connected ordinal set
C . {} is set
c is epsilon-transitive epsilon-connected ordinal set
C . c is set
succ c is epsilon-transitive epsilon-connected ordinal non empty set
{c} is non empty trivial 1 -element set
c \/ {c} is non empty set
C . (succ c) is set
b is epsilon-transitive epsilon-connected ordinal Element of D
(D,f,b) is epsilon-transitive epsilon-connected ordinal Element of D
c is epsilon-transitive epsilon-connected ordinal set
C . c is set
rng C is set
sup (rng C) is epsilon-transitive epsilon-connected ordinal set
c is set
b is set
C . b is set
e is epsilon-transitive epsilon-connected ordinal set
C . e is set
e is epsilon-transitive epsilon-connected ordinal Element of D
b is epsilon-transitive epsilon-connected ordinal Element of D
(D,f,b) is epsilon-transitive epsilon-connected ordinal Element of D
c is Relation-like T-Sequence-like Function-like Ordinal-yielding set
b is epsilon-transitive epsilon-connected ordinal set
dom c is epsilon-transitive epsilon-connected ordinal set
c . b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
c . e is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
b +^ e is epsilon-transitive epsilon-connected ordinal set
c . (b +^ e) is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
b +^ e is epsilon-transitive epsilon-connected ordinal set
c . (b +^ e) is epsilon-transitive epsilon-connected ordinal set
succ e is epsilon-transitive epsilon-connected ordinal non empty set
{e} is non empty trivial 1 -element set
e \/ {e} is non empty set
b +^ (succ e) is epsilon-transitive epsilon-connected ordinal set
c . (b +^ (succ e)) is epsilon-transitive epsilon-connected ordinal set
succ (b +^ e) is epsilon-transitive epsilon-connected ordinal non empty set
{(b +^ e)} is non empty trivial 1 -element set
(b +^ e) \/ {(b +^ e)} is non empty set
b is epsilon-transitive epsilon-connected ordinal Element of D
(D,f,b) is epsilon-transitive epsilon-connected ordinal Element of D
b +^ {} is epsilon-transitive epsilon-connected ordinal set
c . (b +^ {}) is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
b +^ e is epsilon-transitive epsilon-connected ordinal set
sup c is epsilon-transitive epsilon-connected ordinal set
rng c is set
sup (rng c) is epsilon-transitive epsilon-connected ordinal set
b is set
dom c is epsilon-transitive epsilon-connected ordinal set
e is set
c . e is set
e is epsilon-transitive epsilon-connected ordinal set
c . e is epsilon-transitive epsilon-connected ordinal set
f | (sup c) is Relation-like rng f -valued T-Sequence-like Function-like Ordinal-yielding set
rng f is set
b is epsilon-transitive epsilon-connected ordinal Element of D
(D,f,b) is epsilon-transitive epsilon-connected ordinal Element of D
dom (f | (sup c)) is epsilon-transitive epsilon-connected ordinal set
sup (f | (sup c)) is epsilon-transitive epsilon-connected ordinal set
rng (f | (sup c)) is set
sup (rng (f | (sup c))) is epsilon-transitive epsilon-connected ordinal set
e is set
b is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
e is set
(f | (sup c)) . e is set
c is epsilon-transitive epsilon-connected ordinal set
u is epsilon-transitive epsilon-connected ordinal set
u is epsilon-transitive epsilon-connected ordinal Element of D
f . c is epsilon-transitive epsilon-connected ordinal set
(D,f,u) is epsilon-transitive epsilon-connected ordinal Element of D
dom c is epsilon-transitive epsilon-connected ordinal set
z is set
c . z is set
z is epsilon-transitive epsilon-connected ordinal set
succ z is epsilon-transitive epsilon-connected ordinal non empty set
{z} is non empty trivial 1 -element set
z \/ {z} is non empty set
c . (succ z) is epsilon-transitive epsilon-connected ordinal set
f . u is epsilon-transitive epsilon-connected ordinal set
e is epsilon-transitive epsilon-connected ordinal set
(f | (sup c)) . e is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(f | (sup c)) . b is epsilon-transitive epsilon-connected ordinal set
f . b is epsilon-transitive epsilon-connected ordinal set
f . e is epsilon-transitive epsilon-connected ordinal set
lim (f | (sup c)) is epsilon-transitive epsilon-connected ordinal set
f . (sup c) is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
g is epsilon-transitive epsilon-connected ordinal set
C is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom C is epsilon-transitive epsilon-connected ordinal set
rng C is set
sup C is epsilon-transitive epsilon-connected ordinal set
sup (rng C) is epsilon-transitive epsilon-connected ordinal set
c is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom c is epsilon-transitive epsilon-connected ordinal set
rng c is set
sup c is epsilon-transitive epsilon-connected ordinal set
sup (rng c) is epsilon-transitive epsilon-connected ordinal set
c * C is Relation-like Function-like set
b is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
rng b is set
sup b is epsilon-transitive epsilon-connected ordinal set
sup (rng b) is epsilon-transitive epsilon-connected ordinal set
e is set
e is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
e is set
C . e is set
e is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
u is set
c . u is set
C . c is epsilon-transitive epsilon-connected ordinal set
u is epsilon-transitive epsilon-connected ordinal set
b . u is epsilon-transitive epsilon-connected ordinal set
C . e is epsilon-transitive epsilon-connected ordinal set
sup D is epsilon-transitive epsilon-connected ordinal set
D is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
g is Relation-like T-Sequence-like Function-like Ordinal-yielding set
dom g is epsilon-transitive epsilon-connected ordinal set
rng g is set
sup g is epsilon-transitive epsilon-connected ordinal set
sup (rng g) is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
g . C is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
succ c is epsilon-transitive epsilon-connected ordinal non empty set
{c} is non empty trivial 1 -element set
c \/ {c} is non empty set
b is epsilon-transitive epsilon-connected ordinal set
e is set
g . e is set
e is epsilon-transitive epsilon-connected ordinal set
succ C is epsilon-transitive epsilon-connected ordinal non empty set
{C} is non empty trivial 1 -element set
C \/ {C} is non empty set
D is epsilon-transitive epsilon-connected ordinal set
f is Relation-like D -valued T-Sequence-like Function-like Ordinal-yielding set
g is Relation-like D -valued T-Sequence-like Function-like Ordinal-yielding set
(f,g) is Relation-like T-Sequence-like Function-like Ordinal-yielding set
rng f is set
rng g is set
(rng f) \/ (rng g) is set
rng (f,g) is set