:: 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

( { b

( { b

On { b

RelIncl (On { b

order_type_of (RelIncl (On { b

RelIncl ( { b

canonical_isomorphism_of ((RelIncl ( { b

a is Relation-like Function-like T-Sequence-like Ordinal-yielding set

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

{ b

On { b

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

( { b

( { b

On { b

RelIncl (On { b

order_type_of (RelIncl (On { b

RelIncl ( { b

canonical_isomorphism_of ((RelIncl ( { b

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

( { b

( { b

On { b

RelIncl (On { b

order_type_of (RelIncl (On { b

RelIncl ( { b

canonical_isomorphism_of ((RelIncl ( { b

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

( { b

( { b

On { b

RelIncl (On { b

order_type_of (RelIncl (On { b

RelIncl ( { b

canonical_isomorphism_of ((RelIncl ( { b

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

( { b

( { b

On { b

RelIncl (On { b

order_type_of (RelIncl (On { b

RelIncl ( { b

canonical_isomorphism_of ((RelIncl ( { b

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

( { b

( { b

On { b

RelIncl (On { b

order_type_of (RelIncl (On { b

RelIncl ( { b

canonical_isomorphism_of ((RelIncl ( { b

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

( { b

( { b

On { b

RelIncl (On { b

order_type_of (RelIncl (On { b

RelIncl ( { b

canonical_isomorphism_of ((RelIncl ( { b

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

( { b

( { b

On { b

RelIncl (On { b

order_type_of (RelIncl (On { b

RelIncl ( { b

canonical_isomorphism_of ((RelIncl ( { b

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

( { b

( { b

On { b

RelIncl (On { b

order_type_of (RelIncl (On { b

RelIncl ( { b

canonical_isomorphism_of ((RelIncl ( { b

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

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

( { b

( { b

On { b

RelIncl (On { b

order_type_of (RelIncl (On { b

RelIncl ( { b

canonical_isomorphism_of ((RelIncl ( { b

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

( { b

( { b

On { b

RelIncl (On { b

order_type_of (RelIncl (On { b

RelIncl ( { b

canonical_isomorphism_of ((RelIncl ( { b

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

( { b

( { b

On { b

RelIncl (On { b

order_type_of (RelIncl (On { b

RelIncl ( { b

canonical_isomorphism_of ((RelIncl ( { b

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

( { b

( { b

On { b

RelIncl (On { b

order_type_of (RelIncl (On { b

RelIncl ( { b

canonical_isomorphism_of ((RelIncl ( { b

(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

( { b

( { b

On { b

RelIncl (On { b

order_type_of (RelIncl (On { b

RelIncl ( { b

canonical_isomorphism_of ((RelIncl ( { b

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

On F

[:omega,(On F

bool [:omega,(On F

F

(F

F

Union F

rng F

union (rng F

F

dom F

U is epsilon-transitive epsilon-connected ordinal () set

F

F

F

U is set

(F

o is epsilon-transitive epsilon-connected ordinal natural finite cardinal () set

(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

o + 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal () Element of NAT

(F

g is epsilon-transitive epsilon-connected ordinal natural finite cardinal () Element of omega

(F

{F

U is set

g is set

(F

U is epsilon-transitive epsilon-connected ordinal () set

F

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

(F

F

U is epsilon-transitive epsilon-connected ordinal () set

(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

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

o is epsilon-transitive epsilon-connected ordinal natural finite cardinal () set

(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

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

F

(F

F

(F

g is epsilon-transitive epsilon-connected ordinal natural finite cardinal () Element of omega

(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

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

g is epsilon-transitive epsilon-connected ordinal () set

o is set

(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

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