:: ORDINAL5 semantic presentation

REAL is set

K19(REAL) is set

K19(NAT) is non empty V12() non finite set
K19(NAT) is non empty V12() non finite set

the set is set

rng c3 is set

dom ((c3 | a) ^ s) is epsilon-transitive epsilon-connected ordinal set
A is set

c3 . A is set
(c3 | a) . B is set
((c3 | a) ^ s) . A is set

c3 . A is set
s . c9 is set
((c3 | a) ^ s) . A is set

rng a is set

rng (a ^ A) is set
rng A is set

b is set
s is set
a . s is set

(a ^ A) . c is set
b is set
s is set
A . s is set

(a ^ A) . ((dom a) +^ c) is set

rng (a ^ A) is set

rng a is set
rng A is set

a .: NAT is set
a . 0 is set
c3 is set
b is set
a . b is set

a . (succ s) is set

rng <%a%> is non empty V12() finite V35(1) set
A is set
{a} is non empty V12() finite V35(1) set

rng a is set
union (rng a) is set

s is set
a . s is set

rng b is set
union (rng b) is set

c is set
b . c is set

c3 is set

rng b is set
union (rng b) is set

s is set
b . s is set

exp (a,(a,A)) is epsilon-transitive epsilon-connected ordinal set

rng c3 is set
{1} is non empty V12() finite finite-membered V35(1) set
b is set
s is set
c3 . s is set

exp (a,(a,1)) is epsilon-transitive epsilon-connected ordinal set

exp (a,(exp (a,a))) is epsilon-transitive epsilon-connected ordinal set

exp (a,(a,2)) is epsilon-transitive epsilon-connected ordinal set

(0,((2 * 0) + 1)) is epsilon-transitive epsilon-connected ordinal set

(0,(2 * a)) is epsilon-transitive epsilon-connected ordinal set
(2 * a) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(0,((2 * a) + 1)) is epsilon-transitive epsilon-connected ordinal set

(0,(2 * (a + 1))) is epsilon-transitive epsilon-connected ordinal set
(2 * (a + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(0,((2 * (a + 1)) + 1)) is epsilon-transitive epsilon-connected ordinal set
((2 * a) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(0,(((2 * a) + 1) + 1)) is epsilon-transitive epsilon-connected ordinal set
succ ((2 * a) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(0,(succ ((2 * a) + 1))) is epsilon-transitive epsilon-connected ordinal set

succ (2 * (a + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(0,(succ (2 * (a + 1)))) is epsilon-transitive epsilon-connected ordinal set

exp (c3,(c3,b)) is epsilon-transitive epsilon-connected ordinal set

rng s is set
union (rng s) is set

exp (a,(a,c3)) is epsilon-transitive epsilon-connected ordinal set

rng b is set
union (rng b) is set

(a,(0 + 1)) is epsilon-transitive epsilon-connected ordinal set

(a,(s + 1)) is epsilon-transitive epsilon-connected ordinal set

(s + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
exp (a,(a,s)) is epsilon-transitive epsilon-connected ordinal set
(a,((s + 1) + 1)) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,(s + 1))) is epsilon-transitive epsilon-connected ordinal set
(s + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,((s + 1) + 1)) is epsilon-transitive epsilon-connected ordinal set

(a,((A + 1) + 0)) is epsilon-transitive epsilon-connected ordinal set

(a,((A + 1) + s)) is epsilon-transitive epsilon-connected ordinal set
((A + 1) + s) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,(((A + 1) + s) + 1)) is epsilon-transitive epsilon-connected ordinal set

(A + 1) + (s + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,((A + 1) + (s + 1))) is epsilon-transitive epsilon-connected ordinal set

exp (a,(A + 1)) is epsilon-transitive epsilon-connected ordinal set

(a,(c3 + 1)) is epsilon-transitive epsilon-connected ordinal set

(a,(c3 + 1)) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
exp (a,(a,c3)) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set

rng A is set
c3 is set
b is set
A . b is set

rng A is set

rng c3 is set
union (rng c3) is set

rng A is set
union (rng A) is set
b is set
s is set
c3 . s is set
c is set
A . c is set

exp (a,(A . B)) is epsilon-transitive epsilon-connected ordinal set

(a,(NAT +^ c3)) is epsilon-transitive epsilon-connected ordinal set

(a,(NAT +^ (succ c3))) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,(NAT +^ c3))) is epsilon-transitive epsilon-connected ordinal set

(a,(succ (NAT +^ c3))) is epsilon-transitive epsilon-connected ordinal set

(a,(NAT +^ c3)) is epsilon-transitive epsilon-connected ordinal set

(a,(NAT +^ (B -^ A))) is epsilon-transitive epsilon-connected ordinal set

rng F2() is set
union (rng F2()) is set
F3((Union F2())) is epsilon-transitive epsilon-connected ordinal set

F3(F3(A)) is epsilon-transitive epsilon-connected ordinal set

A is set
F2() . A is set

F2() . (b + 1) is epsilon-transitive epsilon-connected ordinal set

{F1()} is non empty V12() finite V35(1) set
A is set
c3 is set
F2() . c3 is set

F3((F2() . A)) is epsilon-transitive epsilon-connected ordinal set

(b + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

F2() . (b + 1) is epsilon-transitive epsilon-connected ordinal set
F3((F2() . b)) is epsilon-transitive epsilon-connected ordinal set
F2() . ((b + 1) + 1) is epsilon-transitive epsilon-connected ordinal set
F3((F2() . (b + 1))) is epsilon-transitive epsilon-connected ordinal set
F2() . (succ (b + 1)) is epsilon-transitive epsilon-connected ordinal set

b is set
F2() . b is set

rng A is set

c3 is set

c is set
A . c is set

B is set
F2() . B is set

F3((F2() . c9)) is epsilon-transitive epsilon-connected ordinal set

b is set
s is set
F2() . s is set

F3((F2() . A)) is epsilon-transitive epsilon-connected ordinal set

F2() . (A + 1) is epsilon-transitive epsilon-connected ordinal set

F2(F2(A)) is epsilon-transitive epsilon-connected ordinal set

F2((a . b)) is epsilon-transitive epsilon-connected ordinal set

succ (A +^ b) is non empty epsilon-transitive epsilon-connected ordinal set

rng a is set

rng A is set

c3 is set

c is set
A . c is set

c9 is set
a . c9 is set

rng c3 is set
union (rng c3) is set

rng A is set
union (rng A) is set

rng a is set
union (rng a) is set

(NAT,(c3 + 1)) is epsilon-transitive epsilon-connected ordinal set

exp (NAT,(a . c3)) is epsilon-transitive epsilon-connected ordinal set

exp (a,(exp (a,NAT))) is epsilon-transitive epsilon-connected ordinal set

exp (NAT,(exp (a,()))) is epsilon-transitive epsilon-connected ordinal set

(exp (a,NAT)) *^ (exp (a,1)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,((exp (a,NAT)) *^ (exp (a,1)))) is epsilon-transitive epsilon-connected ordinal set

exp (NAT,((exp (a,NAT)) *^ a)) is epsilon-transitive epsilon-connected ordinal set

exp ((exp (NAT,a)),(exp (a,NAT))) is epsilon-transitive epsilon-connected ordinal set

(A,(a + 2)) is epsilon-transitive epsilon-connected ordinal set
(A,(a + 1)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(A,(a + 1))) is epsilon-transitive epsilon-connected ordinal set

(a + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(A,((a + 1) + 1)) is epsilon-transitive epsilon-connected ordinal set

(A,(succ (a + 1))) is epsilon-transitive epsilon-connected ordinal set
exp (A,(A,(a + 1))) is epsilon-transitive epsilon-connected ordinal set

exp ((exp (NAT,A)),(A,(a + 1))) is epsilon-transitive epsilon-connected ordinal set
(A,(a + 1)) *^ A is epsilon-transitive epsilon-connected ordinal set
exp (NAT,((A,(a + 1)) *^ A)) is epsilon-transitive epsilon-connected ordinal set

exp (NAT,((A,(succ a)) *^ A)) is epsilon-transitive epsilon-connected ordinal set
exp (A,(A,a)) is epsilon-transitive epsilon-connected ordinal set
(exp (A,(A,a))) *^ A is epsilon-transitive epsilon-connected ordinal set
exp (NAT,((exp (A,(A,a))) *^ A)) is epsilon-transitive epsilon-connected ordinal set

(exp (A,(A,a))) *^ (exp (A,1)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,((exp (A,(A,a))) *^ (exp (A,1)))) is epsilon-transitive epsilon-connected ordinal set

exp (A,(1 +^ (A,a))) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(exp (A,(1 +^ (A,a))))) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(exp (A,(A,a)))) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(A,(succ a))) is epsilon-transitive epsilon-connected ordinal set

(a) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set

rng c3 is set
union (rng c3) is set

exp (NAT,(A . c3)) is epsilon-transitive epsilon-connected ordinal set

rng A is set
union (rng A) is set

exp (a,(exp (a,NAT))) is epsilon-transitive epsilon-connected ordinal set

(a,(0 + 2)) is epsilon-transitive epsilon-connected ordinal set

(a,(b + 2)) is epsilon-transitive epsilon-connected ordinal set
(a,(b + 1)) is epsilon-transitive epsilon-connected ordinal set
(b + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
A . ((b + 1) + 1) is epsilon-transitive epsilon-connected ordinal set
(b + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,((b + 1) + 2)) is epsilon-transitive epsilon-connected ordinal set

(b + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT

A . ((b + 1) + 1) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(A . (b + 1))) is epsilon-transitive epsilon-connected ordinal set

(s + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,(s + 2)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(a,(s + 2))) is epsilon-transitive epsilon-connected ordinal set
(s + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,((s + 1) + 2)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(a,(b + 2))) is epsilon-transitive epsilon-connected ordinal set
(b + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,((b + 1) + 2)) is epsilon-transitive epsilon-connected ordinal set

rng b is set
union (rng b) is set
s is set
c is set
A . c is set

(a,(A + 2)) is epsilon-transitive epsilon-connected ordinal set

s is set
c is set
b . c is set