:: ORDINAL6 semantic presentation

REAL is set

bool REAL is non empty set

bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set

a is set
a is set
On a is set

a is set
U is set

g is set
a is () set
U is Element of a
a is set
On a is () set
U is set
a is () set

U is set

a \ U is Element of bool a
bool a is non empty set
g is set

a \ U is Element of bool a
bool a is non empty set
a is set
RelIncl a is Relation-like V34() V37() V41() set
U is set
RelIncl U is Relation-like V34() V37() V41() set

o is set
g . o is set
f is set
g . f is set
field () is set
field () is set
dom g is set
rng g is set
[o,f] is set
{o,f} is non empty finite set
{o} is non empty trivial finite 1 -element set
{{o,f},{o}} is non empty finite finite-membered set
[(g . o),(g . f)] is set
{(g . o),(g . f)} is non empty finite set
{(g . o)} is non empty trivial finite 1 -element set
{{(g . o),(g . f)},{(g . o)}} is non empty finite finite-membered set
a is () set
RelIncl a is Relation-like V34() V37() V41() set
U is () set
RelIncl U is Relation-like V34() V37() V41() set

o is set
g . o is set
f is set
g . f is set
field () is set
field () is set
dom g is set
rng g is set

a is set
U is set
[a,U] is set
{a,U} is non empty finite set
{a} is non empty trivial finite 1 -element set
{{a,U},{a}} is non empty finite finite-membered set
g is set
RelIncl g is Relation-like V34() V37() V41() set
field () is set

g is set
a . g is set
(a ^ U) . g is set

rng (a ^ U) is set
rng a is set
rng U is set
(rng a) \/ (rng U) is set

a is set
b is set
(a ^ U) . b is set

a . y is set

(dom a) +^ (y -^ (dom a)) is epsilon-transitive epsilon-connected ordinal () set
U . (y -^ (dom a)) is set

a is set
b is set
a . b is set
(a ^ U) . b is set
b is set
U . b is set

(a ^ U) . ((dom a) +^ y) is set

a is () set
union a is set

rng a is set

[:a,a:] is Relation-like set
bool [:a,a:] is non empty set
dom (id a) is set
rng (id a) is set

[:a,a:] is Relation-like set
bool [:a,a:] is non empty set

[:a,a:] is Relation-like set
bool [:a,a:] is non empty set

rng U is () set

[:g,g:] is Relation-like set
bool [:g,g:] is non empty set

{a} is non empty trivial finite 1 -element set
a \/ {a} is non empty set

[::] is Relation-like non empty set
bool [::] is non empty set

[::] is Relation-like non empty set
bool [::] is non empty set

rng U is () set

a is set
On a is () set
RelIncl (On a) is Relation-like V34() V37() V41() set

a is () set

On a is () set
RelIncl (On a) is Relation-like V34() V37() V41() set

RelIncl a is Relation-like V34() V37() V41() set

a is () set
RelIncl a is Relation-like V34() V37() V41() set

On a is () set

{a} is non empty trivial finite 1 -element set

On {a} is () set

a \/ {a} is non empty set
RelIncl {a} is Relation-like non empty V34() V37() V41() finite set

{a,U} is non empty finite set

On {a,U} is () set
RelIncl (On {a,U}) is Relation-like well-ordering V34() V37() V41() set

{(a \/ U)} is non empty trivial finite 1 -element set
(a \/ U) \/ {(a \/ U)} is non empty set

On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set

a is set

On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set

canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set

rng a is () set
a is set

On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set

canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set

rng (a) is () set

rng a is () set
a is () set

On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set

canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
rng (a) is () set
a is set

On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set

canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set

a is set

On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set

canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
a is set

On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set

canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
U is set
g is set

o . U is set
o . g is set
a is set

On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set

canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
U is set
g is set

o . U is set
o . g is set
a is set

On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set

canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set

rng a is () set
a is () set
U is () set
a \/ U is set

a is () set
U is set
a \ U is Element of bool a
bool a is non empty set

a is () set
U is () set

On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set

On U is () set
RelIncl (On U) is Relation-like well-ordering V34() V37() V41() set

RelIncl ((a) +^ (U)) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
a \/ U is () set
RelIncl (a \/ U) is Relation-like well-ordering V34() V37() V41() set

canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set

canonical_isomorphism_of ((RelIncl (U)),(RelIncl (On U))) is Relation-like Function-like set

dom ((a) ^ (U)) is epsilon-transitive epsilon-connected ordinal () set

(dom (a)) +^ (dom (U)) is epsilon-transitive epsilon-connected ordinal () set
rng (a) is () set
rng (U) is () set
field (RelIncl ((a) +^ (U))) is set
rng ((a) ^ (U)) is () set
field (RelIncl (a \/ U)) is set
(rng (a)) \/ (rng (U)) is () set
h is set
((a) ^ (U)) . h is set
f2 is set
((a) ^ (U)) . f2 is set
(a) . h is set
(a) . f2 is set

(dom (a)) +^ (f1 -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
(a) . h is set
(U) . (f1 -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set

(dom (a)) +^ (y -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
(a) . f2 is set
(U) . (y -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set

(dom (a)) +^ (y -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set

(dom (a)) +^ (f1 -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
(U) . (f1 -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
(U) . (y -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
h is set
((a) ^ (U)) . h is set
f2 is set
[h,f2] is set
{h,f2} is non empty finite set
{h} is non empty trivial finite 1 -element set
{{h,f2},{h}} is non empty finite finite-membered set
((a) ^ (U)) . f2 is set
[(((a) ^ (U)) . h),(((a) ^ (U)) . f2)] is set
{(((a) ^ (U)) . h),(((a) ^ (U)) . f2)} is non empty finite set
{(((a) ^ (U)) . h)} is non empty trivial finite 1 -element set
{{(((a) ^ (U)) . h),(((a) ^ (U)) . f2)},{(((a) ^ (U)) . h)}} is non empty finite finite-membered set

[y,f1] is set
{y,f1} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,f1},{y}} is non empty finite finite-membered set
((a) ^ (U)) . y is epsilon-transitive epsilon-connected ordinal () set

((a) ^ (U)) . f1 is epsilon-transitive epsilon-connected ordinal () set

[(((a) ^ (U)) . y),(((a) ^ (U)) . f1)] is set
{(((a) ^ (U)) . y),(((a) ^ (U)) . f1)} is non empty finite set
{(((a) ^ (U)) . y)} is non empty trivial finite 1 -element set
{{(((a) ^ (U)) . y),(((a) ^ (U)) . f1)},{(((a) ^ (U)) . y)}} is non empty finite finite-membered set
field () is set

(dom (a)) +^ (f1 -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
((a) ^ (U)) . y is epsilon-transitive epsilon-connected ordinal () set

((a) ^ (U)) . f1 is epsilon-transitive epsilon-connected ordinal () set
(U) . (f1 -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set

(dom (a)) +^ (y -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set

(dom (a)) +^ (f1 -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set

[(y -^ (a)),(f1 -^ (a))] is set
{(y -^ (a)),(f1 -^ (a))} is non empty finite set
{(y -^ (a))} is non empty trivial finite 1 -element set
{{(y -^ (a)),(f1 -^ (a))},{(y -^ (a))}} is non empty finite finite-membered set
((a) ^ (U)) . f1 is epsilon-transitive epsilon-connected ordinal () set
(U) . (f1 -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
((a) ^ (U)) . y is epsilon-transitive epsilon-connected ordinal () set
(U) . (y -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
[(((a) ^ (U)) . y),(((a) ^ (U)) . f1)] is set
{(((a) ^ (U)) . y),(((a) ^ (U)) . f1)} is non empty finite set
{(((a) ^ (U)) . y)} is non empty trivial finite 1 -element set
{{(((a) ^ (U)) . y),(((a) ^ (U)) . f1)},{(((a) ^ (U)) . y)}} is non empty finite finite-membered set
field () is set

field (RelIncl (a)) is set
field (RelIncl (U)) is set

((a) ^ (U)) . y is epsilon-transitive epsilon-connected ordinal () set

((a) ^ (U)) . f1 is epsilon-transitive epsilon-connected ordinal () set

[((a) . y),((a) . f1)] is set
{((a) . y),((a) . f1)} is non empty finite set
{((a) . y)} is non empty trivial finite 1 -element set
{{((a) . y),((a) . f1)},{((a) . y)}} is non empty finite finite-membered set
[y,f1] is set
{y,f1} is non empty finite set
{y} is non empty trivial finite 1 -element set
{{y,f1},{y}} is non empty finite finite-membered set

((a) ^ (U)) . f1 is epsilon-transitive epsilon-connected ordinal () set

(dom (a)) +^ (y -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
((a) ^ (U)) . y is epsilon-transitive epsilon-connected ordinal () set
(U) . (y -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set

(dom (a)) +^ (y -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set

(dom (a)) +^ (f1 -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
(U) . (f1 -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
(U) . (y -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
((a) ^ (U)) . f1 is epsilon-transitive epsilon-connected ordinal () set
((a) ^ (U)) . y is epsilon-transitive epsilon-connected ordinal () set
[((U) . (y -^ (dom (a)))),((U) . (f1 -^ (dom (a))))] is set
{((U) . (y -^ (dom (a)))),((U) . (f1 -^ (dom (a))))} is non empty finite set
{((U) . (y -^ (dom (a))))} is non empty trivial finite 1 -element set
{{((U) . (y -^ (dom (a)))),((U) . (f1 -^ (dom (a))))},{((U) . (y -^ (dom (a))))}} is non empty finite finite-membered set
[(y -^ (dom (a))),(f1 -^ (dom (a)))] is set
{(y -^ (dom (a))),(f1 -^ (dom (a)))} is non empty finite set
{(y -^ (dom (a)))} is non empty trivial finite 1 -element set
{{(y -^ (dom (a))),(f1 -^ (dom (a)))},{(y -^ (dom (a)))}} is non empty finite finite-membered set

a is () set
U is () set
a \/ U is () set

((a \/ U)) is epsilon-transitive epsilon-connected ordinal () set
On (a \/ U) is () set
RelIncl (On (a \/ U)) is Relation-like well-ordering V34() V37() V41() set

RelIncl (a \/ U) is Relation-like well-ordering V34() V37() V41() set

RelIncl ((a \/ U)) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ((a \/ U))),(RelIncl (On (a \/ U)))) is Relation-like Function-like set

On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set

canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set

On U is () set
RelIncl (On U) is Relation-like well-ordering V34() V37() V41() set

canonical_isomorphism_of ((RelIncl (U)),(RelIncl (On U))) is Relation-like Function-like set

RelIncl ((a) +^ (U)) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
a is () set
U is () set
a \/ U is () set
((a \/ U)) is epsilon-transitive epsilon-connected ordinal () set
On (a \/ U) is () set
RelIncl (On (a \/ U)) is Relation-like well-ordering V34() V37() V41() set

RelIncl (a \/ U) is Relation-like well-ordering V34() V37() V41() set

On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set

On U is () set
RelIncl (On U) is Relation-like well-ordering V34() V37() V41() set

RelIncl ((a \/ U)) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ((a \/ U))),(RelIncl (On (a \/ U)))) is Relation-like Function-like set

canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set

canonical_isomorphism_of ((RelIncl (U)),(RelIncl (On U))) is Relation-like Function-like set

dom ((a \/ U)) is epsilon-transitive epsilon-connected ordinal () set

(dom (a)) +^ (dom (U)) is epsilon-transitive epsilon-connected ordinal () set
(a) +^ (dom (U)) is epsilon-transitive epsilon-connected ordinal () set
a is set

rng U is set
dom U is set
U . a is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } is set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is epsilon-transitive epsilon-connected ordinal () set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } is () set
RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } )),(RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ))) is Relation-like Function-like set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } is set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } is () set
g is set

a is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } is set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is epsilon-transitive epsilon-connected ordinal () set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } is () set
RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } )),(RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ))) is Relation-like Function-like set

(U) . a is set
rng (U) is () set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } is set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is epsilon-transitive epsilon-connected ordinal () set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } is () set
RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } )),(RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ))) is Relation-like Function-like set
rng (a) is () set
rng a is () set
g is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } is set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is epsilon-transitive epsilon-connected ordinal () set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } is () set
RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } )),(RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ))) is Relation-like Function-like set
a is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } is set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is epsilon-transitive epsilon-connected ordinal () set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } is () set
RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } )),(RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ))) is Relation-like Function-like set

(U) . a is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } is set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is epsilon-transitive epsilon-connected ordinal () set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } is () set
RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } )),(RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ))) is Relation-like Function-like set

rng (a) is () set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } is set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is epsilon-transitive epsilon-connected ordinal () set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } is () set
RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } )),(RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ))) is Relation-like Function-like set

rng (U) is () set
o is set
(U) . o is set

{a} is non empty trivial finite 1 -element set
a \/ {a} is non empty set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } is set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ) is epsilon-transitive epsilon-connected ordinal () set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } is () set
RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } )),(RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ))) is Relation-like Function-like set

{a} is non empty trivial finite 1 -element set
a \/ {a} is non empty set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } is set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ) is epsilon-transitive epsilon-connected ordinal () set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } is () set
RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } )),(RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ))) is Relation-like Function-like set

RelIncl { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } is Relation-like V34() V37() V41() set
a is set
union a is set

U . () is set

f is set
a is set
f is set
U . f is set
the Element of a is Element of a
f is set

y is set
c is set

{b} is non empty trivial finite 1 -element set
b \/ {b} is non empty set

rng U is () set

rng y is () set

c is set
x is set
y . x is set
y is set
z is set
U . z is set

a is set
union a is set

U . () is set
g is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } is set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ) is epsilon-transitive epsilon-connected ordinal () set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } is () set
RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } )),(RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom g : b1 is_a_fixpoint_of g } ))) is Relation-like Function-like set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } is set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is epsilon-transitive epsilon-connected ordinal () set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } is () set
RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } )),(RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ))) is Relation-like Function-like set

rng (U) is () set

rng ((U) | a) is () set
union (rng ((U) | a)) is epsilon-transitive epsilon-connected ordinal () set

rng o is () set
U . ((U) . a) is epsilon-transitive epsilon-connected ordinal () set

a is set
b is set
o . b is set
(U) . b is set

b is set
y is set
o . y is set
(U) . y is set

{y} is non empty trivial finite 1 -element set
y \/ {y} is non empty set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } is set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is epsilon-transitive epsilon-connected ordinal () set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } is () set
RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } )),(RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ))) is Relation-like Function-like set

rng (a) is () set

rng f is () set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } is set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is epsilon-transitive epsilon-connected ordinal () set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } is () set
RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } )),(RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom a : b1 is_a_fixpoint_of a } ))) is Relation-like Function-like set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } is set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is epsilon-transitive epsilon-connected ordinal () set
On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } is () set
RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } )),(RelIncl (On { b1 where b1 is epsilon-transitive epsilon-connected ordinal () Element of dom U : b1 is_a_fixpoint_of U } ))) is Relation-like Function-like set
a is () set
f is () set
a \ f is () Element of bool a
bool a is non empty set
y is set

c is set

y is set

f \/ (a \ f) is () set

((a \ f)) is epsilon-transitive epsilon-connected ordinal () set
On (a \ f) is () set
RelIncl (On (a \ f)) is Relation-like well-ordering V34() V37() V41() set

RelIncl (a \ f) is Relation-like well-ordering V34() V37() V41() set

RelIncl ((a \ f)) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ((a \ f))),(RelIncl (On (a \ f)))) is Relation-like Function-like set

[:(On a),(On a):] is Relation-like non empty set
bool [:(On a),(On a):] is non empty set

[:U,(On a):] is Relation-like set
bool [:U,(On a):] is non empty set
g is Relation-like U -defined On a -valued Function-like V26(U) V30(U, On a) Element of bool [:U,(On a):]
dom g is set
rng g is set

[:U,(On a):] is Relation-like set
bool [:U,(On a):] is non empty set

o is set
g . o is set

[:a,(On U):] is Relation-like set
bool [:a,(On U):] is non empty set

rng g is () set

[:a,(On U):] is Relation-like set
bool [:a,(On U):] is non empty set

rng g is () set

On (rng g) is () set

{o} is non empty trivial finite 1 -element set
o \/ {o} is non empty set

[:omega,(On F1()):] is Relation-like non empty non trivial non finite set
bool [:omega,(On F1()):] is non empty non trivial non finite set
F3() is Relation-like omega -defined On F1() -valued Function-like T-Sequence-like non empty V26( omega ) V30( omega , On F1()) Ordinal-yielding Element of bool [:omega,(On F1()):]
(F1(),omega,F3(),0) is epsilon-transitive epsilon-connected ordinal () Element of F1()
F2() is epsilon-transitive epsilon-connected ordinal () Element of F1()

rng F3() is non empty () set

F4((Union F3())) is epsilon-transitive epsilon-connected ordinal () set

F4(F4(U)) is epsilon-transitive epsilon-connected ordinal () set
F4(F2()) is epsilon-transitive epsilon-connected ordinal () set
U is set
(F1(),omega,F3(),U) is epsilon-transitive epsilon-connected ordinal () Element of F1()

(F1(),omega,F3(),o) is epsilon-transitive epsilon-connected ordinal () Element of F1()

o \/ {o} is non empty finite set
(F1(),omega,F3(),(succ o)) is epsilon-transitive epsilon-connected ordinal () Element of F1()

(F1(),omega,F3(),(o + 1)) is epsilon-transitive epsilon-connected ordinal () Element of F1()

(F1(),omega,F3(),g) is epsilon-transitive epsilon-connected ordinal () Element of F1()
{F2()} is non empty trivial finite 1 -element Element of F1()
U is set
g is set
(F1(),omega,F3(),g) is epsilon-transitive epsilon-connected ordinal () Element of F1()

{U} is non empty trivial finite 1 -element set
U \/ {U} is non empty set
(F1(),omega,F3(),(succ U)) is epsilon-transitive epsilon-connected ordinal () Element of F1()
(F1(),omega,F3(),U) is epsilon-transitive epsilon-connected ordinal () Element of F1()
F4((F1(),omega,F3(),U)) is epsilon-transitive epsilon-connected ordinal () set

(F1(),omega,F3(),U) is epsilon-transitive epsilon-connected ordinal () Element of F1()

{U} is non empty trivial finite 1 -element set
U \/ {U} is non empty set
(F1(),omega,F3(),(succ U)) is epsilon-transitive epsilon-connected ordinal () Element of F1()

(F1(),omega,F3(),()) is epsilon-transitive epsilon-connected ordinal () Element of F1()

(F1(),omega,F3(),o) is epsilon-transitive epsilon-connected ordinal () Element of F1()

o \/ {o} is non empty finite set
(F1(),omega,F3(),(succ o)) is epsilon-transitive epsilon-connected ordinal () Element of F1()

{(o + 1)} is non empty trivial finite finite-membered 1 -element set
(o + 1) \/ {(o + 1)} is non empty finite set
(F1(),omega,F3(),(o + 1)) is epsilon-transitive epsilon-connected ordinal () Element of F1()
F4((F1(),omega,F3(),o)) is epsilon-transitive epsilon-connected ordinal () set
(F1(),omega,F3(),((o + 1) + 1)) is epsilon-transitive epsilon-connected ordinal () Element of F1()
F4((F1(),omega,F3(),(o + 1))) is epsilon-transitive epsilon-connected ordinal () set
(F1(),omega,F3(),(succ (o + 1))) is epsilon-transitive epsilon-connected ordinal () Element of F1()

(F1(),omega,F3(),g) is epsilon-transitive epsilon-connected ordinal () Element of F1()

g \/ {g} is non empty finite set
(F1(),omega,F3(),(succ g)) is epsilon-transitive epsilon-connected ordinal () Element of F1()

(F1(),omega,F3(),1) is epsilon-transitive epsilon-connected ordinal () Element of F1()

o is set
(F1(),omega,F3(),o) is epsilon-transitive epsilon-connected ordinal () Element of F1()

{g} is non empty trivial finite 1 -element set
g \/ {g} is non empty set

(F1(),omega,F3(),f) is epsilon-transitive epsilon-connected ordinal () Element of F1()

f \/ {f} is non empty