:: ORDINAL4 semantic presentation

bool omega is V33() set

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

last D is set

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

dom g is set

C . c is set
D . c is set

C . ((dom D) +^ c) is set
f . c is set
((dom D) +^ c) -^ (dom D) is epsilon-transitive epsilon-connected ordinal set
f . (((dom D) +^ c) -^ (dom D)) is set

c is set

g . b is set
D . b is set
g . c is set
C . c is set

(dom D) +^ (b -^ (dom D)) is epsilon-transitive epsilon-connected ordinal set
g . b is set
f . (b -^ (dom D)) is set
g . c is set
C . c is set
g . c is set
C . c is set
g . c is set
C . c is set

rng D is set

rng (D,f) is set
rng f is set
(rng D) \/ (rng f) is set

b is set
e is set
(D,f) . e is set

(dom D) +^ (e -^ (dom D)) is epsilon-transitive epsilon-connected ordinal set

rng D is set

rng f is set

rng (D,f) is set
(rng D) \/ (rng f) is set

(dom f) +^ (C +^ (b -^ c)) is epsilon-transitive epsilon-connected ordinal set
D . (C +^ (b -^ c)) is epsilon-transitive epsilon-connected ordinal set

(dom f) +^ (b +^ (e -^ e)) is epsilon-transitive epsilon-connected ordinal set
D . (b +^ (e -^ e)) is epsilon-transitive epsilon-connected ordinal set

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

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

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

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

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

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

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

rng D is set

b is set
D . b is set

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

D " f is set

g is set
D . g is set
c is set

D . c is set

dom (D * f) is set

D " (dom f) is set
rng f is set

rng g is set

rng g is set

e is set
g . e is set

b is set
g . b is set

rng D is set

rng D is set

C is set
D . C is set

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

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

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

rng D is set

g is set

D * (f | g) is Relation-like Function-like set
D " (rng D) is set
dom D is set
D " g is set
dom (D * (f | g)) is set
dom (f | g) is set
D " (dom (f | g)) is set
dom f is set
(dom f) /\ g is set
D " ((dom f) /\ g) is set
D " (dom f) is set
(D " (dom f)) /\ (D " g) is set
dom (D * f) is set

rng g is set

rng D is set

rng (D | C) is set

rng f is set

e is set
e is set
(D | C) . e is set
(D | C) * f is Relation-like Function-like set
(D | C) * (f | b) is Relation-like Function-like set

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

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

rng e is set

rng C is set

c is set
C . c is set

g . c is set

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

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

rng c is set

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

rng g is set

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

exp (D,(f +^ g)) is epsilon-transitive epsilon-connected ordinal set

(exp (D,g)) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

exp (D,(f +^ C)) is epsilon-transitive epsilon-connected ordinal set

(exp (D,C)) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

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

exp (D,(f +^ (succ C))) is epsilon-transitive epsilon-connected ordinal set

(exp (D,(succ C))) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

{(f +^ C)} is non empty trivial 1 -element set
(f +^ C) \/ {(f +^ C)} is non empty set
exp (D,(succ (f +^ C))) is epsilon-transitive epsilon-connected ordinal set
D *^ (exp (D,(f +^ C))) is epsilon-transitive epsilon-connected ordinal set

(D *^ (exp (D,C))) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

exp (D,(f +^ C)) is epsilon-transitive epsilon-connected ordinal set

(exp (D,C)) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

dom (c *^ (exp (D,f))) is epsilon-transitive epsilon-connected ordinal set

exp (D,(f +^ e)) is epsilon-transitive epsilon-connected ordinal set

(exp (D,e)) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

(c . e) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set
(c *^ (exp (D,f))) . e is epsilon-transitive epsilon-connected ordinal set

(dom e) +^ (dom (c *^ (exp (D,f)))) is epsilon-transitive epsilon-connected ordinal set
(e,(c *^ (exp (D,f)))) is Relation-like T-Sequence-like Function-like Ordinal-yielding set

(exp (D,{})) *^ (exp (D,f)) is epsilon-transitive epsilon-connected ordinal set

exp ((exp (D,f)),g) is epsilon-transitive epsilon-connected ordinal set

exp (D,(g *^ f)) is epsilon-transitive epsilon-connected ordinal set

exp ((exp (D,f)),C) is epsilon-transitive epsilon-connected ordinal set

exp (D,(C *^ f)) is epsilon-transitive epsilon-connected ordinal set

{C} is non empty trivial 1 -element set
C \/ {C} is non empty set
exp ((exp (D,f)),(succ C)) is epsilon-transitive epsilon-connected ordinal set

exp (D,((succ C) *^ f)) is epsilon-transitive epsilon-connected ordinal set
(exp (D,f)) *^ (exp (D,(C *^ f))) is epsilon-transitive epsilon-connected ordinal set

exp (D,((C *^ f) +^ f)) is epsilon-transitive epsilon-connected ordinal set

exp ((exp (D,f)),C) is epsilon-transitive epsilon-connected ordinal set

exp (D,(C *^ f)) is epsilon-transitive epsilon-connected ordinal set

rng b is set
e is set
b is set
b . b is set

e is set

dom (b * e) is set
e is set

e is set

c . e is set
exp ((exp (D,f)),b) is epsilon-transitive epsilon-connected ordinal set
exp (D,(b *^ f)) is epsilon-transitive epsilon-connected ordinal set

(b * e) . e is set

exp ((exp (D,f)),{}) is epsilon-transitive epsilon-connected ordinal set

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

c is set

rng C is set

F1(F1(D)) is epsilon-transitive epsilon-connected ordinal set

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

{(f +^ C)} is non empty trivial 1 -element set
(f +^ C) \/ {(f +^ C)} is non empty set

rng D is set

rng f is set

g is set

b is set
f . b is set

b is set
D . b is set

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

[:(On D),(On D):] is set
bool [:(On D),(On D):] is set
f is Relation-like On D -defined On D -valued Function-like V25( On D, On D) Element of bool [:(On D),(On D):]
dom f is set
rng f is set
F1() is epsilon-transitive non empty V41() V42() universal set

[:(On F1()),(On F1()):] is set
bool [:(On F1()),(On F1()):] is set

rng D is set
f is set
g is set
D . g is set

F2(C) is epsilon-transitive epsilon-connected ordinal Element of F1()
f is Relation-like On F1() -defined On F1() -valued T-Sequence-like Function-like V25( On F1(), On F1()) Ordinal-yielding Element of bool [:(On F1()),(On F1()):]

F2(g) is epsilon-transitive epsilon-connected ordinal Element of F1()

[:(On D),(On D):] is set
bool [:(On D),(On D):] is set

rng f is set

[:(On D),(On D):] is set
bool [:(On D),(On D):] is set

rng f is set

dom (f * g) is set
rng g is set
rng (f * g) is set

rng C is set

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

{(D)} is non empty trivial 1 -element Element of D
[:C,{(D)}:] is set

{(D)} is non empty trivial 1 -element Element of D
[:f,{(D)}:] is Element of D
[:f,{(D)}:] \/ [:C,{(D)}:] is set

c is set

[:C,g:] is set

c is set

(D,b,e) is epsilon-transitive epsilon-connected ordinal Element of D

[:(On D),(On D):] is set
bool [:(On D),(On D):] is set

rng D is set

g is set

union (rng D) is set
D .: (dom D) is set

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

[:(On D),(On D):] is set
bool [:(On D),(On D):] is set

(D,f,(D)) is epsilon-transitive epsilon-connected ordinal Element of D

C . {} is set

C . c is set

{c} is non empty trivial 1 -element set
c \/ {c} is non empty set
C . (succ c) is set

(D,f,b) is epsilon-transitive epsilon-connected ordinal Element of D

C . c is set
rng C is set

c is set
b is set
C . b is set

C . e is set

(D,f,b) is epsilon-transitive epsilon-connected ordinal Element of D

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

{(b +^ e)} is non empty trivial 1 -element set
(b +^ e) \/ {(b +^ e)} is non empty set

(D,f,b) is epsilon-transitive epsilon-connected ordinal Element of D

rng c is set

b is set

e is set
c . e is set

rng f is set

(D,f,b) is epsilon-transitive epsilon-connected ordinal Element of D

rng (f | (sup c)) is set
sup (rng (f | (sup c))) is epsilon-transitive epsilon-connected ordinal set
e is set

e is set
(f | (sup c)) . e is set

(D,f,u) is epsilon-transitive epsilon-connected ordinal Element of D

z is set
c . z is set

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

rng C is set

rng c is set

rng b is set

e is set

e is set
C . e is set

u is set
c . u is set

rng g is set

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

e is set
g . e is set

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

rng f is set
rng g is set
(rng f) \/ (rng g) is set
rng (f,g) is set