:: ORDINAL6 semantic presentation

REAL is set
NAT is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
omega is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal limit_cardinal set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty finite finite-yielding finite-membered cardinal {} -element Ordinal-yielding increasing V71() decreasing non-decreasing non-increasing Cantor-normal-form set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty finite finite-yielding finite-membered cardinal {} -element Ordinal-yielding increasing V71() decreasing non-decreasing non-increasing Cantor-normal-form set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty finite finite-yielding finite-membered cardinal {} -element Ordinal-yielding increasing V71() decreasing non-decreasing non-increasing Cantor-normal-form set
1 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal Element of NAT
2 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty finite finite-yielding finite-membered cardinal {} -element Ordinal-yielding increasing V71() decreasing non-decreasing non-increasing Cantor-normal-form Element of NAT
a is set
a is set
On a is set
sup a is epsilon-transitive epsilon-connected ordinal () set
a is set
U is set
g is epsilon-transitive epsilon-connected ordinal () set
sup a is epsilon-transitive epsilon-connected ordinal () set
U is epsilon-transitive epsilon-connected ordinal () 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
sup a is epsilon-transitive epsilon-connected ordinal () set
U is set
a is epsilon-transitive epsilon-connected ordinal () set
U is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal () set
U is epsilon-transitive epsilon-connected ordinal () set
a \ U is Element of bool a
bool a is non empty set
g is set
a is epsilon-transitive epsilon-connected ordinal () set
U is epsilon-transitive epsilon-connected ordinal () 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
g is Relation-like Function-like set
o is set
g . o is set
f is set
g . f is set
field (RelIncl a) is set
field (RelIncl U) 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
g is Relation-like Function-like set
o is set
g . o is set
f is set
g . f is set
field (RelIncl a) is set
field (RelIncl U) is set
dom g is set
rng g is set
c is epsilon-transitive epsilon-connected ordinal () set
y is epsilon-transitive epsilon-connected ordinal () set
b is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal () 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 (RelIncl g) is set
a is Relation-like Function-like T-Sequence-like set
U is Relation-like Function-like T-Sequence-like set
a ^ U is Relation-like Function-like T-Sequence-like set
dom (a ^ U) is epsilon-transitive epsilon-connected ordinal () set
dom a is epsilon-transitive epsilon-connected ordinal () set
dom U is epsilon-transitive epsilon-connected ordinal () set
(dom a) +^ (dom U) is epsilon-transitive epsilon-connected ordinal () set
g is set
a . g is set
(a ^ U) . g is set
a is Relation-like Function-like T-Sequence-like set
U is Relation-like Function-like T-Sequence-like set
a ^ U is Relation-like Function-like T-Sequence-like set
rng (a ^ U) is set
rng a is set
rng U is set
(rng a) \/ (rng U) is set
dom (a ^ U) is epsilon-transitive epsilon-connected ordinal () set
dom a is epsilon-transitive epsilon-connected ordinal () set
dom U is epsilon-transitive epsilon-connected ordinal () set
(dom a) +^ (dom U) is epsilon-transitive epsilon-connected ordinal () set
a is set
b is set
(a ^ U) . b is set
y is epsilon-transitive epsilon-connected ordinal () set
a . y is set
y is epsilon-transitive epsilon-connected ordinal () set
y -^ (dom a) is epsilon-transitive epsilon-connected ordinal () set
(dom a) +^ (y -^ (dom a)) is epsilon-transitive epsilon-connected ordinal () set
U . (y -^ (dom a)) is set
y is epsilon-transitive epsilon-connected ordinal () set
a is set
b is set
a . b is set
(a ^ U) . b is set
b is set
U . b is set
y is epsilon-transitive epsilon-connected ordinal () set
(dom a) +^ y is epsilon-transitive epsilon-connected ordinal () set
(a ^ U) . ((dom a) +^ y) is set
a is epsilon-transitive epsilon-connected ordinal () set
epsilon_ a is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite epsilon () set
U is epsilon-transitive epsilon-connected ordinal () set
epsilon_ U is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite epsilon () set
a is epsilon-transitive epsilon-connected ordinal () set
epsilon_ a is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite epsilon () set
U is epsilon-transitive epsilon-connected ordinal () set
epsilon_ U is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite epsilon () set
a is () set
union a is set
U is epsilon-transitive epsilon-connected ordinal () set
a is Relation-like Function-like Ordinal-yielding set
rng a is set
a is epsilon-transitive epsilon-connected ordinal () set
id a is Relation-like a -defined a -valued Function-like one-to-one V26(a) V30(a,a) Element of bool [:a,a:]
[:a,a:] is Relation-like set
bool [:a,a:] is non empty set
dom (id a) is set
rng (id a) is set
a is epsilon-transitive epsilon-connected ordinal () set
id a is Relation-like a -defined a -valued Function-like one-to-one T-Sequence-like V26(a) V30(a,a) Ordinal-yielding Element of bool [:a,a:]
[:a,a:] is Relation-like set
bool [:a,a:] is non empty set
U is Relation-like Function-like T-Sequence-like Ordinal-yielding set
g is epsilon-transitive epsilon-connected ordinal () set
dom U is epsilon-transitive epsilon-connected ordinal () set
U . g is epsilon-transitive epsilon-connected ordinal () set
o is epsilon-transitive epsilon-connected ordinal () set
U . o is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal () set
id a is Relation-like a -defined a -valued Function-like one-to-one T-Sequence-like V26(a) V30(a,a) Ordinal-yielding increasing non-decreasing Element of bool [:a,a:]
[:a,a:] is Relation-like set
bool [:a,a:] is non empty set
U is Relation-like Function-like T-Sequence-like Ordinal-yielding set
g is epsilon-transitive epsilon-connected ordinal () set
dom U is epsilon-transitive epsilon-connected ordinal () set
U . g is epsilon-transitive epsilon-connected ordinal () set
U | g is Relation-like rng U -valued Function-like T-Sequence-like Ordinal-yielding set
rng U is () set
o is epsilon-transitive epsilon-connected ordinal () set
id g is Relation-like g -defined g -valued Function-like one-to-one T-Sequence-like V26(g) V30(g,g) Ordinal-yielding increasing non-decreasing Element of bool [:g,g:]
[:g,g:] is Relation-like set
bool [:g,g:] is non empty set
dom (id g) is epsilon-transitive epsilon-connected ordinal () set
dom (U | g) is epsilon-transitive epsilon-connected ordinal () set
dom (U | g) is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal () set
b is epsilon-transitive epsilon-connected ordinal () set
succ a is epsilon-transitive epsilon-connected ordinal non empty () set
{a} is non empty trivial finite 1 -element set
a \/ {a} is non empty set
y is epsilon-transitive epsilon-connected ordinal non empty () set
c is epsilon-transitive epsilon-connected ordinal () set
(U | g) . c is epsilon-transitive epsilon-connected ordinal () set
the epsilon-transitive epsilon-connected ordinal non empty () set is epsilon-transitive epsilon-connected ordinal non empty () set
id the epsilon-transitive epsilon-connected ordinal non empty () set is Relation-like the epsilon-transitive epsilon-connected ordinal non empty () set -defined the epsilon-transitive epsilon-connected ordinal non empty () set -valued Function-like one-to-one T-Sequence-like non empty V26( the epsilon-transitive epsilon-connected ordinal non empty () set ) V30( the epsilon-transitive epsilon-connected ordinal non empty () set , the epsilon-transitive epsilon-connected ordinal non empty () set ) Ordinal-yielding increasing continuous non-decreasing Element of bool [: the epsilon-transitive epsilon-connected ordinal non empty () set , the epsilon-transitive epsilon-connected ordinal non empty () set :]
[: the epsilon-transitive epsilon-connected ordinal non empty () set , the epsilon-transitive epsilon-connected ordinal non empty () set :] is Relation-like non empty set
bool [: the epsilon-transitive epsilon-connected ordinal non empty () set , the epsilon-transitive epsilon-connected ordinal non empty () set :] is non empty set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
a is Relation-like Function-like T-Sequence-like set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
the epsilon-transitive epsilon-connected ordinal non empty () set is epsilon-transitive epsilon-connected ordinal non empty () set
id the epsilon-transitive epsilon-connected ordinal non empty () set is Relation-like the epsilon-transitive epsilon-connected ordinal non empty () set -defined the epsilon-transitive epsilon-connected ordinal non empty () set -valued Function-like one-to-one T-Sequence-like non empty V26( the epsilon-transitive epsilon-connected ordinal non empty () set ) V30( the epsilon-transitive epsilon-connected ordinal non empty () set , the epsilon-transitive epsilon-connected ordinal non empty () set ) Ordinal-yielding increasing continuous non-decreasing () Element of bool [: the epsilon-transitive epsilon-connected ordinal non empty () set , the epsilon-transitive epsilon-connected ordinal non empty () set :]
[: the epsilon-transitive epsilon-connected ordinal non empty () set , the epsilon-transitive epsilon-connected ordinal non empty () set :] is Relation-like non empty set
bool [: the epsilon-transitive epsilon-connected ordinal non empty () set , the epsilon-transitive epsilon-connected ordinal non empty () set :] is non empty set
a is epsilon-transitive epsilon-connected ordinal () set
U is Relation-like Function-like T-Sequence-like Ordinal-yielding set
U | a is Relation-like rng U -valued Function-like T-Sequence-like Ordinal-yielding set
rng U is () set
dom U is epsilon-transitive epsilon-connected ordinal () set
g is epsilon-transitive epsilon-connected ordinal () set
dom (U | a) is epsilon-transitive epsilon-connected ordinal () set
(U | a) . g is epsilon-transitive epsilon-connected ordinal () set
o is epsilon-transitive epsilon-connected ordinal () set
(U | a) . o is epsilon-transitive epsilon-connected ordinal () set
U . g is epsilon-transitive epsilon-connected ordinal () set
U . o is epsilon-transitive epsilon-connected ordinal () set
a is set
On a is () set
RelIncl (On a) is Relation-like V34() V37() V41() set
order_type_of (RelIncl (On a)) is epsilon-transitive epsilon-connected ordinal () set
a is () set
(a) is epsilon-transitive epsilon-connected ordinal () set
On a is () set
RelIncl (On a) is Relation-like V34() V37() V41() set
order_type_of (RelIncl (On a)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl a is Relation-like V34() V37() V41() set
order_type_of (RelIncl a) is epsilon-transitive epsilon-connected ordinal () set
U is epsilon-transitive epsilon-connected ordinal () set
g is epsilon-transitive epsilon-connected ordinal () set
a is () set
RelIncl a is Relation-like V34() V37() V41() set
U is epsilon-transitive epsilon-connected ordinal () set
a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty finite finite-yielding finite-membered cardinal {} -element Ordinal-yielding increasing V71() decreasing non-decreasing non-increasing Cantor-normal-form () set
On a is () set
a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty finite finite-yielding finite-membered cardinal {} -element Ordinal-yielding increasing V71() decreasing non-decreasing non-increasing Cantor-normal-form () set
order_type_of a is epsilon-transitive epsilon-connected ordinal () set
RelIncl a is Relation-like well_founded well-ordering V34() V37() V39() V41() finite set
({}) is epsilon-transitive epsilon-connected ordinal () set
On {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty finite finite-yielding finite-membered cardinal {} -element Ordinal-yielding increasing V71() decreasing non-decreasing non-increasing Cantor-normal-form () set
RelIncl (On {}) is Relation-like well_founded well-ordering V34() V37() V39() V41() finite set
order_type_of (RelIncl (On {})) is epsilon-transitive epsilon-connected ordinal () set
RelIncl {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional well_founded well-ordering epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V34() V37() V39() V41() finite finite-yielding finite-membered cardinal {} -element Ordinal-yielding increasing V71() decreasing non-decreasing non-increasing Cantor-normal-form () set
order_type_of (RelIncl {}) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty finite finite-yielding finite-membered cardinal {} -element Ordinal-yielding increasing V71() decreasing non-decreasing non-increasing Cantor-normal-form () set
a is epsilon-transitive epsilon-connected ordinal () set
{a} is non empty trivial finite 1 -element set
({a}) is epsilon-transitive epsilon-connected ordinal () set
On {a} is () set
RelIncl (On {a}) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On {a})) is epsilon-transitive epsilon-connected ordinal () set
succ a is epsilon-transitive epsilon-connected ordinal non empty () set
a \/ {a} is non empty set
RelIncl {a} is Relation-like non empty V34() V37() V41() finite set
order_type_of (RelIncl {a}) is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal () set
U is epsilon-transitive epsilon-connected ordinal () set
{a,U} is non empty finite 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
order_type_of (RelIncl (On {a,U})) is epsilon-transitive epsilon-connected ordinal () set
card {a,U} is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal () Element of omega
a \/ U is epsilon-transitive epsilon-connected ordinal () set
succ (a \/ U) is epsilon-transitive epsilon-connected ordinal non empty () set
{(a \/ U)} is non empty trivial finite 1 -element set
(a \/ U) \/ {(a \/ U)} is non empty set
a is epsilon-transitive epsilon-connected ordinal () set
(a) is epsilon-transitive epsilon-connected ordinal () set
On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On a)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl a is Relation-like well_founded well-ordering V34() V37() V39() V41() set
order_type_of (RelIncl a) is epsilon-transitive epsilon-connected ordinal () set
a is set
(a) is epsilon-transitive epsilon-connected ordinal () set
On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On a)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl (a) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
f is epsilon-transitive epsilon-connected ordinal () set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal () set
rng a is () set
a is set
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(a) is epsilon-transitive epsilon-connected ordinal () set
On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On a)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl (a) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
dom (a) is epsilon-transitive epsilon-connected ordinal () set
rng (a) is () set
f is epsilon-transitive epsilon-connected ordinal () set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal () set
rng a is () set
a is () set
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(a) is epsilon-transitive epsilon-connected ordinal () set
On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On a)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl a is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl a) is epsilon-transitive epsilon-connected ordinal () set
RelIncl (a) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
rng (a) is () set
a is set
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(a) is epsilon-transitive epsilon-connected ordinal () set
On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On a)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl (a) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
dom (a) is epsilon-transitive epsilon-connected ordinal () set
card (dom (a)) is epsilon-transitive epsilon-connected ordinal cardinal () set
card (On a) is epsilon-transitive epsilon-connected ordinal cardinal () set
U is epsilon-transitive epsilon-connected ordinal () set
a is set
(a) is epsilon-transitive epsilon-connected ordinal () set
On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On a)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl (a) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding set
canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
a is set
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(a) is epsilon-transitive epsilon-connected ordinal () set
On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On a)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl (a) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
U is set
g is set
o is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom o is epsilon-transitive epsilon-connected ordinal () set
o . U is set
o . g is set
a is set
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(a) is epsilon-transitive epsilon-connected ordinal () set
On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On a)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl (a) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
U is set
g is set
o is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom o is epsilon-transitive epsilon-connected ordinal () set
o . U is set
o . g is set
a is set
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(a) is epsilon-transitive epsilon-connected ordinal () set
On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On a)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl (a) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
f is epsilon-transitive epsilon-connected ordinal () set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal () set
rng a is () set
a is () set
U is () set
a \/ U is set
g is epsilon-transitive epsilon-connected ordinal () set
o is epsilon-transitive epsilon-connected ordinal () set
g \/ o is epsilon-transitive epsilon-connected ordinal () set
a is () set
U is set
a \ U is Element of bool a
bool a is non empty set
g is epsilon-transitive epsilon-connected ordinal () set
a is () set
U is () set
(a) is epsilon-transitive epsilon-connected ordinal () set
On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On a)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl a is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl a) is epsilon-transitive epsilon-connected ordinal () set
(U) is epsilon-transitive epsilon-connected ordinal () set
On U is () set
RelIncl (On U) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On U)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl U is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl U) is epsilon-transitive epsilon-connected ordinal () set
(a) +^ (U) is epsilon-transitive epsilon-connected ordinal () 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
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
RelIncl (a) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
(U) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
RelIncl (U) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl (U)),(RelIncl (On U))) is Relation-like Function-like set
(a) ^ (U) is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom ((a) ^ (U)) is epsilon-transitive epsilon-connected ordinal () set
dom (a) is epsilon-transitive epsilon-connected ordinal () set
dom (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
f1 is epsilon-transitive epsilon-connected ordinal () set
f1 -^ (dom (a)) is epsilon-transitive epsilon-connected ordinal () 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
y is epsilon-transitive epsilon-connected ordinal () set
y -^ (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
y is epsilon-transitive epsilon-connected ordinal () set
y -^ (dom (a)) is epsilon-transitive epsilon-connected ordinal () set
(dom (a)) +^ (y -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
f1 is epsilon-transitive epsilon-connected ordinal () set
f1 -^ (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 is epsilon-transitive epsilon-connected ordinal () set
f1 is epsilon-transitive epsilon-connected ordinal () 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) . y is epsilon-transitive epsilon-connected ordinal () set
((a) ^ (U)) . f1 is epsilon-transitive epsilon-connected ordinal () set
(a) . 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 (RelIncl a) is set
y is epsilon-transitive epsilon-connected ordinal () set
f1 is epsilon-transitive epsilon-connected ordinal () set
f1 -^ (dom (a)) is epsilon-transitive epsilon-connected ordinal () set
(dom (a)) +^ (f1 -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
((a) ^ (U)) . y is epsilon-transitive epsilon-connected ordinal () set
(a) . 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
y is epsilon-transitive epsilon-connected ordinal () set
f1 is epsilon-transitive epsilon-connected ordinal () set
y is epsilon-transitive epsilon-connected ordinal () set
f1 is epsilon-transitive epsilon-connected ordinal () set
y -^ (dom (a)) is epsilon-transitive epsilon-connected ordinal () set
(dom (a)) +^ (y -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
f1 -^ (dom (a)) is epsilon-transitive epsilon-connected ordinal () set
(dom (a)) +^ (f1 -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
y -^ (a) is epsilon-transitive epsilon-connected ordinal () set
f1 -^ (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 (RelIncl U) is set
y is epsilon-transitive epsilon-connected ordinal () set
f1 is epsilon-transitive epsilon-connected ordinal () set
field (RelIncl (a)) is set
field (RelIncl (U)) is set
y is epsilon-transitive epsilon-connected ordinal () set
f1 is epsilon-transitive epsilon-connected ordinal () set
((a) ^ (U)) . y is epsilon-transitive epsilon-connected ordinal () set
(a) . y is epsilon-transitive epsilon-connected ordinal () set
((a) ^ (U)) . f1 is epsilon-transitive epsilon-connected ordinal () set
(a) . 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
y is epsilon-transitive epsilon-connected ordinal () set
f1 is epsilon-transitive epsilon-connected ordinal () set
y is epsilon-transitive epsilon-connected ordinal () set
f1 is epsilon-transitive epsilon-connected ordinal () set
((a) ^ (U)) . f1 is epsilon-transitive epsilon-connected ordinal () set
(a) . f1 is epsilon-transitive epsilon-connected ordinal () set
y -^ (dom (a)) 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
y is epsilon-transitive epsilon-connected ordinal () set
f1 is epsilon-transitive epsilon-connected ordinal () set
y -^ (dom (a)) is epsilon-transitive epsilon-connected ordinal () set
(dom (a)) +^ (y -^ (dom (a))) is epsilon-transitive epsilon-connected ordinal () set
f1 -^ (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
y is epsilon-transitive epsilon-connected ordinal () set
f1 is epsilon-transitive epsilon-connected ordinal () set
a is () set
U is () set
a \/ U is () set
((a \/ U)) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing 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
order_type_of (RelIncl (On (a \/ U))) is epsilon-transitive epsilon-connected ordinal () set
RelIncl (a \/ U) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (a \/ U)) is epsilon-transitive epsilon-connected ordinal () 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
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
(a) is epsilon-transitive epsilon-connected ordinal () set
On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On a)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl a is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl a) is epsilon-transitive epsilon-connected ordinal () set
RelIncl (a) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
(U) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
(U) is epsilon-transitive epsilon-connected ordinal () set
On U is () set
RelIncl (On U) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On U)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl U is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl U) is epsilon-transitive epsilon-connected ordinal () set
RelIncl (U) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl (U)),(RelIncl (On U))) is Relation-like Function-like set
(a) ^ (U) is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(a) +^ (U) is epsilon-transitive epsilon-connected ordinal () 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
order_type_of (RelIncl (On (a \/ U))) is epsilon-transitive epsilon-connected ordinal () set
RelIncl (a \/ U) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (a \/ U)) is epsilon-transitive epsilon-connected ordinal () set
(a) is epsilon-transitive epsilon-connected ordinal () set
On a is () set
RelIncl (On a) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On a)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl a is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl a) is epsilon-transitive epsilon-connected ordinal () set
(U) is epsilon-transitive epsilon-connected ordinal () set
On U is () set
RelIncl (On U) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On U)) is epsilon-transitive epsilon-connected ordinal () set
RelIncl U is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl U) is epsilon-transitive epsilon-connected ordinal () set
(a) +^ (U) is epsilon-transitive epsilon-connected ordinal () set
((a \/ U)) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing 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
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
RelIncl (a) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl (a)),(RelIncl (On a))) is Relation-like Function-like set
(U) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
RelIncl (U) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl (U)),(RelIncl (On U))) is Relation-like Function-like set
(a) ^ (U) is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom ((a \/ U)) is epsilon-transitive epsilon-connected ordinal () set
dom (a) is epsilon-transitive epsilon-connected ordinal () set
dom (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
U is Relation-like Function-like set
rng U is set
dom U is set
U . a is set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } is set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is epsilon-transitive epsilon-connected ordinal () set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } is () set
RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } )),(RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ))) is Relation-like Function-like set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } is set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } is () set
g is set
o is epsilon-transitive epsilon-connected ordinal () Element of dom a
a is set
U is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(U) is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom U is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } is set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is epsilon-transitive epsilon-connected ordinal () set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } is () set
RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } )),(RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ))) is Relation-like Function-like set
dom (U) is epsilon-transitive epsilon-connected ordinal () set
(U) . a is set
rng (U) is () set
a is epsilon-transitive epsilon-connected ordinal () Element of dom U
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } is set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is epsilon-transitive epsilon-connected ordinal () set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } is () set
RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } )),(RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ))) is Relation-like Function-like set
rng (a) is () set
rng a is () set
g is set
o is epsilon-transitive epsilon-connected ordinal () Element of dom a
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } is set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is epsilon-transitive epsilon-connected ordinal () set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } is () set
RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } )),(RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ))) is Relation-like Function-like set
a is set
U is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(U) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
dom U is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } is set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is epsilon-transitive epsilon-connected ordinal () set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } is () set
RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } )),(RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ))) is Relation-like Function-like set
dom (U) is epsilon-transitive epsilon-connected ordinal () set
(U) . a is set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
dom a is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } is set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is epsilon-transitive epsilon-connected ordinal () set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } is () set
RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } )),(RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ))) is Relation-like Function-like set
dom (a) is epsilon-transitive epsilon-connected ordinal () set
U is epsilon-transitive epsilon-connected ordinal () set
(a) . U is epsilon-transitive epsilon-connected ordinal () set
rng (a) is () set
o is epsilon-transitive epsilon-connected ordinal () Element of dom a
a . o is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal () set
U is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(U) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
dom U is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } is set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is epsilon-transitive epsilon-connected ordinal () set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } is () set
RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } )),(RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ))) is Relation-like Function-like set
dom (U) is epsilon-transitive epsilon-connected ordinal () set
rng (U) is () set
o is set
(U) . o is set
a is epsilon-transitive epsilon-connected ordinal () set
succ a is epsilon-transitive epsilon-connected ordinal non empty () set
{a} is non empty trivial finite 1 -element set
a \/ {a} is non empty set
U is epsilon-transitive epsilon-connected ordinal () set
g is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(g) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
dom g is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } is set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ) is epsilon-transitive epsilon-connected ordinal () set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } is () set
RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } )),(RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ))) is Relation-like Function-like set
dom (g) is epsilon-transitive epsilon-connected ordinal () set
(g) . a is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal () set
(g) . f is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal () set
succ a is epsilon-transitive epsilon-connected ordinal non empty () set
{a} is non empty trivial finite 1 -element set
a \/ {a} is non empty set
U is epsilon-transitive epsilon-connected ordinal () set
g is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(g) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
dom g is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } is set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ) is epsilon-transitive epsilon-connected ordinal () set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } is () set
RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } )),(RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ))) is Relation-like Function-like set
dom (g) is epsilon-transitive epsilon-connected ordinal () set
(g) . a is epsilon-transitive epsilon-connected ordinal () set
(g) . (succ a) is epsilon-transitive epsilon-connected ordinal () set
b is epsilon-transitive epsilon-connected ordinal () set
(g) . b is epsilon-transitive epsilon-connected ordinal () set
RelIncl { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } is Relation-like V34() V37() V41() set
a is set
union a is set
U is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom U is epsilon-transitive epsilon-connected ordinal () set
U . (union a) is set
o is epsilon-transitive epsilon-connected ordinal () set
o is epsilon-transitive epsilon-connected ordinal () 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
a is epsilon-transitive epsilon-connected ordinal () set
b is epsilon-transitive epsilon-connected ordinal () set
g is epsilon-transitive epsilon-connected ordinal () set
y is set
c is set
x is epsilon-transitive epsilon-connected ordinal () set
succ b is epsilon-transitive epsilon-connected ordinal non empty () set
{b} is non empty trivial finite 1 -element set
b \/ {b} is non empty set
b is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite () set
U | b is Relation-like rng U -valued Function-like T-Sequence-like Ordinal-yielding set
rng U is () set
y is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
dom y is epsilon-transitive epsilon-connected ordinal () set
Union y is epsilon-transitive epsilon-connected ordinal () set
rng y is () set
union (rng y) is epsilon-transitive epsilon-connected ordinal () set
U . b is epsilon-transitive epsilon-connected ordinal () set
lim y is epsilon-transitive epsilon-connected ordinal () set
c is set
x is set
y . x is set
y is set
z is set
U . z is set
h is epsilon-transitive epsilon-connected ordinal () set
U . h is epsilon-transitive epsilon-connected ordinal () set
y . h is epsilon-transitive epsilon-connected ordinal () set
f2 is epsilon-transitive epsilon-connected ordinal () set
o is epsilon-transitive epsilon-connected ordinal () set
a is set
union a is set
U is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom U is epsilon-transitive epsilon-connected ordinal () set
U . (union a) is set
g is set
a is epsilon-transitive epsilon-connected ordinal () set
U is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite () set
g is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(g) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
dom g is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } is set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ) is epsilon-transitive epsilon-connected ordinal () set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } is () set
RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } )),(RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom g : b₁ is_a_fixpoint_of g } ))) is Relation-like Function-like set
dom (g) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal () set
(g) . f is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal () set
(g) . a is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite () set
U is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(U) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
dom U is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } is set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is epsilon-transitive epsilon-connected ordinal () set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } is () set
RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } )),(RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ))) is Relation-like Function-like set
dom (U) is epsilon-transitive epsilon-connected ordinal () set
(U) . a is epsilon-transitive epsilon-connected ordinal () set
(U) | a is Relation-like rng (U) -valued Function-like T-Sequence-like Ordinal-yielding set
rng (U) is () set
Union ((U) | a) is epsilon-transitive epsilon-connected ordinal () set
rng ((U) | a) is () set
union (rng ((U) | a)) is epsilon-transitive epsilon-connected ordinal () set
o is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
rng o is () set
U . ((U) . a) is epsilon-transitive epsilon-connected ordinal () set
dom o is epsilon-transitive epsilon-connected ordinal () set
a is set
b is set
o . b is set
(U) . b is set
union (rng o) is epsilon-transitive epsilon-connected ordinal () set
b is set
y is set
o . y is set
(U) . y is set
a is epsilon-transitive epsilon-connected ordinal () set
U . a is epsilon-transitive epsilon-connected ordinal () set
b is epsilon-transitive epsilon-connected ordinal () set
(U) . b is epsilon-transitive epsilon-connected ordinal () set
y is epsilon-transitive epsilon-connected ordinal () set
succ y is epsilon-transitive epsilon-connected ordinal non empty () set
{y} is non empty trivial finite 1 -element set
y \/ {y} is non empty set
(U) . y is epsilon-transitive epsilon-connected ordinal () set
o . y is epsilon-transitive epsilon-connected ordinal () set
(U) . (succ y) is epsilon-transitive epsilon-connected ordinal () set
o . (succ y) is epsilon-transitive epsilon-connected ordinal () set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing continuous non-decreasing () set
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
dom a is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } is set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is epsilon-transitive epsilon-connected ordinal () set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } is () set
RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } )),(RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ))) is Relation-like Function-like set
g is epsilon-transitive epsilon-connected ordinal () set
dom (a) is epsilon-transitive epsilon-connected ordinal () set
(a) . g is epsilon-transitive epsilon-connected ordinal () set
(a) | g is Relation-like rng (a) -valued Function-like T-Sequence-like Ordinal-yielding set
rng (a) is () set
o is epsilon-transitive epsilon-connected ordinal () set
f is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
Union f is epsilon-transitive epsilon-connected ordinal () set
rng f is () set
union (rng f) is epsilon-transitive epsilon-connected ordinal () set
dom f is epsilon-transitive epsilon-connected ordinal () set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
U is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(a) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
dom a is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } is set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is epsilon-transitive epsilon-connected ordinal () set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } is () set
RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } )),(RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom a : b₁ is_a_fixpoint_of a } ))) is Relation-like Function-like set
(U) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
dom U is epsilon-transitive epsilon-connected ordinal () set
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } is set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing set
( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is epsilon-transitive epsilon-connected ordinal () set
On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } is () set
RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } )) is epsilon-transitive epsilon-connected ordinal () set
RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } ) is Relation-like well_founded well-ordering V34() V37() V39() V41() set
canonical_isomorphism_of ((RelIncl ( { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ is_a_fixpoint_of U } )),(RelIncl (On { b₁ where b₁ is epsilon-transitive epsilon-connected ordinal () Element of dom U : b₁ 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
x is epsilon-transitive epsilon-connected ordinal () Element of dom a
c is set
y is epsilon-transitive epsilon-connected ordinal () Element of dom U
a . y is epsilon-transitive epsilon-connected ordinal () set
U . y is epsilon-transitive epsilon-connected ordinal () set
y is set
c is epsilon-transitive epsilon-connected ordinal () Element of dom a
a . c is epsilon-transitive epsilon-connected ordinal () set
U . c is epsilon-transitive epsilon-connected ordinal () set
f \/ (a \ f) is () set
((a \ f)) is Relation-like Function-like T-Sequence-like Ordinal-yielding increasing non-decreasing 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
order_type_of (RelIncl (On (a \ f))) is epsilon-transitive epsilon-connected ordinal () set
RelIncl (a \ f) is Relation-like well-ordering V34() V37() V41() set
order_type_of (RelIncl (a \ f)) is epsilon-transitive epsilon-connected ordinal () 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
(a) ^ ((a \ f)) is Relation-like Function-like T-Sequence-like Ordinal-yielding set
a is epsilon-transitive non empty subset-closed Tarski universal set
On a is epsilon-transitive epsilon-connected ordinal non empty () set
[:(On a),(On a):] is Relation-like non empty set
bool [:(On a),(On a):] is non empty set
id (On a) is Relation-like On a -defined On a -valued Function-like one-to-one T-Sequence-like non empty V26( On a) V30( On a, On a) V30( On a, On a) Ordinal-yielding increasing continuous non-decreasing () Element of bool [:(On a),(On a):]
U is Relation-like On a -defined On a -valued Function-like T-Sequence-like non empty V26( On a) V30( On a, On a) Ordinal-yielding Element of bool [:(On a),(On a):]
U is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive non empty subset-closed Tarski universal set
On a is epsilon-transitive epsilon-connected ordinal 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 is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive non empty subset-closed Tarski universal set
On a is epsilon-transitive epsilon-connected ordinal 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 T-Sequence-like V26(U) V30(U, On a) Ordinal-yielding Element of bool [:U,(On a):]
o is set
g . o is set
dom g is epsilon-transitive epsilon-connected ordinal () set
dom g is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal () set
U is epsilon-transitive non empty subset-closed Tarski universal set
On U is epsilon-transitive epsilon-connected ordinal non empty () set
[:a,(On U):] is Relation-like set
bool [:a,(On U):] is non empty set
g is Relation-like a -defined On U -valued Function-like T-Sequence-like V26(a) V30(a, On U) Ordinal-yielding Element of bool [:a,(On U):]
Union g is epsilon-transitive epsilon-connected ordinal () set
rng g is () set
union (rng g) is epsilon-transitive epsilon-connected ordinal () set
dom g is epsilon-transitive epsilon-connected ordinal () set
card (dom g) is epsilon-transitive epsilon-connected ordinal cardinal () set
card U is epsilon-transitive epsilon-connected ordinal non empty cardinal () set
card (rng g) is epsilon-transitive epsilon-connected ordinal cardinal () set
a is epsilon-transitive epsilon-connected ordinal () set
U is epsilon-transitive non empty subset-closed Tarski universal set
On U is epsilon-transitive epsilon-connected ordinal non empty () set
[:a,(On U):] is Relation-like set
bool [:a,(On U):] is non empty set
g is Relation-like a -defined On U -valued Function-like T-Sequence-like V26(a) V30(a, On U) Ordinal-yielding Element of bool [:a,(On U):]
sup g is epsilon-transitive epsilon-connected ordinal () set
rng g is () set
sup (rng g) is epsilon-transitive epsilon-connected ordinal () set
Union g is epsilon-transitive epsilon-connected ordinal () set
union (rng g) is epsilon-transitive epsilon-connected ordinal () set
On (rng g) is () set
o is epsilon-transitive epsilon-connected ordinal () Element of U
succ o is epsilon-transitive epsilon-connected ordinal non empty () Element of U
{o} is non empty trivial finite 1 -element set
o \/ {o} is non empty set
F₁() is epsilon-transitive non empty subset-closed Tarski universal set
On F₁() is epsilon-transitive epsilon-connected ordinal non empty () set
[:omega,(On F₁()):] is Relation-like non empty non trivial non finite set
bool [:omega,(On F₁()):] is non empty non trivial non finite set
F₃() is Relation-like omega -defined On F₁() -valued Function-like T-Sequence-like non empty V26( omega ) V30( omega , On F₁()) Ordinal-yielding Element of bool [:omega,(On F₁()):]
(F₁(),omega,F₃(),0) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
F₂() is epsilon-transitive epsilon-connected ordinal () Element of F₁()
Union F₃() is epsilon-transitive epsilon-connected ordinal () set
rng F₃() is non empty () set
union (rng F₃()) is epsilon-transitive epsilon-connected ordinal () set
F₄((Union F₃())) is epsilon-transitive epsilon-connected ordinal () set
dom F₃() is epsilon-transitive epsilon-connected ordinal non empty () set
U is epsilon-transitive epsilon-connected ordinal () set
F₄(U) is epsilon-transitive epsilon-connected ordinal () set
F₄(F₄(U)) is epsilon-transitive epsilon-connected ordinal () set
F₄(F₂()) is epsilon-transitive epsilon-connected ordinal () set
U is set
(F₁(),omega,F₃(),U) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
o is epsilon-transitive epsilon-connected ordinal natural finite cardinal () set
(F₁(),omega,F₃(),o) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
succ o is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal () Element of omega
{o} is non empty trivial finite finite-membered 1 -element set
o \/ {o} is non empty finite set
(F₁(),omega,F₃(),(succ o)) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
o + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal () Element of NAT
(F₁(),omega,F₃(),(o + 1)) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
g is epsilon-transitive epsilon-connected ordinal natural finite cardinal () Element of omega
(F₁(),omega,F₃(),g) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
{F₂()} is non empty trivial finite 1 -element Element of F₁()
U is set
g is set
(F₁(),omega,F₃(),g) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
U is epsilon-transitive epsilon-connected ordinal () set
F₄(U) is epsilon-transitive epsilon-connected ordinal () set
U is epsilon-transitive epsilon-connected ordinal () set
succ U is epsilon-transitive epsilon-connected ordinal non empty () set
{U} is non empty trivial finite 1 -element set
U \/ {U} is non empty set
(F₁(),omega,F₃(),(succ U)) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
(F₁(),omega,F₃(),U) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
F₄((F₁(),omega,F₃(),U)) is epsilon-transitive epsilon-connected ordinal () set
U is epsilon-transitive epsilon-connected ordinal () set
(F₁(),omega,F₃(),U) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
succ U is epsilon-transitive epsilon-connected ordinal non empty () set
{U} is non empty trivial finite 1 -element set
U \/ {U} is non empty set
(F₁(),omega,F₃(),(succ U)) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
succ 0 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal () Element of omega
{0} is functional non empty trivial finite finite-membered 1 -element set
0 \/ {0} is non empty finite finite-membered set
(F₁(),omega,F₃(),(succ 0)) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
o is epsilon-transitive epsilon-connected ordinal natural finite cardinal () set
(F₁(),omega,F₃(),o) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
succ o is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal () Element of omega
{o} is non empty trivial finite finite-membered 1 -element set
o \/ {o} is non empty finite set
(F₁(),omega,F₃(),(succ o)) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
o + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal () Element of NAT
(o + 1) + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal () Element of NAT
succ (o + 1) is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal () Element of omega
{(o + 1)} is non empty trivial finite finite-membered 1 -element set
(o + 1) \/ {(o + 1)} is non empty finite set
(F₁(),omega,F₃(),(o + 1)) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
F₄((F₁(),omega,F₃(),o)) is epsilon-transitive epsilon-connected ordinal () set
(F₁(),omega,F₃(),((o + 1) + 1)) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
F₄((F₁(),omega,F₃(),(o + 1))) is epsilon-transitive epsilon-connected ordinal () set
(F₁(),omega,F₃(),(succ (o + 1))) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
g is epsilon-transitive epsilon-connected ordinal natural finite cardinal () Element of omega
(F₁(),omega,F₃(),g) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
succ g is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal () Element of omega
{g} is non empty trivial finite finite-membered 1 -element set
g \/ {g} is non empty finite set
(F₁(),omega,F₃(),(succ g)) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
U is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom U is epsilon-transitive epsilon-connected ordinal () set
succ 0 is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal () Element of omega
{0} is functional non empty trivial finite finite-membered 1 -element set
0 \/ {0} is non empty finite finite-membered set
(F₁(),omega,F₃(),1) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
g is epsilon-transitive epsilon-connected ordinal () set
o is set
(F₁(),omega,F₃(),o) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
succ g is epsilon-transitive epsilon-connected ordinal non empty () set
{g} is non empty trivial finite 1 -element set
g \/ {g} is non empty set
f is epsilon-transitive epsilon-connected ordinal natural finite cardinal () Element of omega
(F₁(),omega,F₃(),f) is epsilon-transitive epsilon-connected ordinal () Element of F₁()
succ f is epsilon-transitive epsilon-connected ordinal natural non empty finite cardinal () Element of omega
{f} is non empty trivial finite finite-membered 1 -element set
f \/ {f} is non empty