REAL is set
NAT is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite V33() V34() Element of K19(REAL)
K19(REAL) is set
COMPLEX is set
NAT is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite V33() V34() set
K19(NAT) is non empty V12() non finite set
K19(NAT) is non empty V12() non finite set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() Element of NAT
{{}} is functional non empty V12() finite finite-membered V35(1) set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V53() set
rng a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V12() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative V49() V53() set
the set is set
<% the set %> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) V53() set
a is Relation-like Function-like T-Sequence-like set
A is Relation-like Function-like non empty T-Sequence-like set
a ^ A is Relation-like Function-like T-Sequence-like set
dom a is epsilon-transitive epsilon-connected ordinal set
dom A is non empty epsilon-transitive epsilon-connected ordinal set
(dom a) +^ (dom A) is epsilon-transitive epsilon-connected ordinal set
dom (a ^ A) is epsilon-transitive epsilon-connected ordinal set
A ^ a is Relation-like Function-like T-Sequence-like set
dom A is non empty epsilon-transitive epsilon-connected ordinal set
dom a is epsilon-transitive epsilon-connected ordinal set
(dom A) +^ (dom a) is epsilon-transitive epsilon-connected ordinal set
dom (A ^ a) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a +^ A is epsilon-transitive epsilon-connected ordinal set
c3 is Relation-like Function-like T-Sequence-like set
dom c3 is epsilon-transitive epsilon-connected ordinal set
c3 | a is Relation-like rng c3 -valued Function-like T-Sequence-like set
rng c3 is set
dom (c3 | a) is epsilon-transitive epsilon-connected ordinal set
s is Relation-like Function-like T-Sequence-like set
dom s is epsilon-transitive epsilon-connected ordinal set
(c3 | a) ^ s is Relation-like Function-like T-Sequence-like set
dom ((c3 | a) ^ s) is epsilon-transitive epsilon-connected ordinal set
A is set
B is epsilon-transitive epsilon-connected ordinal set
c3 . A is set
(c3 | a) . B is set
((c3 | a) ^ s) . A is set
B is epsilon-transitive epsilon-connected ordinal set
c9 is epsilon-transitive epsilon-connected ordinal set
a +^ c9 is epsilon-transitive epsilon-connected ordinal set
c9 is epsilon-transitive epsilon-connected ordinal set
a +^ c9 is epsilon-transitive epsilon-connected ordinal set
c3 . A is set
s . c9 is set
((c3 | a) ^ s) . A is set
B is epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like set
rng a is set
A is Relation-like Function-like T-Sequence-like set
a ^ A is Relation-like Function-like T-Sequence-like set
rng (a ^ A) is set
rng A is set
dom (a ^ A) is epsilon-transitive epsilon-connected ordinal set
dom a is epsilon-transitive epsilon-connected ordinal set
dom A is epsilon-transitive epsilon-connected ordinal set
(dom a) +^ (dom A) is epsilon-transitive epsilon-connected ordinal set
b is set
s is set
a . s is set
c is epsilon-transitive epsilon-connected ordinal set
(a ^ A) . c is set
b is set
s is set
A . s is set
c is epsilon-transitive epsilon-connected ordinal set
(dom a) +^ c is epsilon-transitive epsilon-connected ordinal set
(a ^ A) . ((dom a) +^ c) is set
a is Relation-like Function-like T-Sequence-like set
A is Relation-like Function-like T-Sequence-like set
a ^ A is Relation-like Function-like T-Sequence-like set
rng (a ^ A) is set
c3 is epsilon-transitive epsilon-connected ordinal set
rng a is set
rng A is set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 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
A is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like set
dom a is epsilon-transitive epsilon-connected ordinal set
a is Relation-like Function-like T-Sequence-like set
dom a is epsilon-transitive epsilon-connected ordinal set
a .: NAT is set
a . 0 is set
c3 is set
b is set
a . b is set
s is epsilon-transitive epsilon-connected ordinal set
succ s is non empty epsilon-transitive epsilon-connected ordinal set
a . (succ s) is set
a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set
A is epsilon-transitive epsilon-connected ordinal set
dom a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set
a . A is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set
A is epsilon-transitive epsilon-connected ordinal set
dom a is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set
a . A is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding V53() set
a is epsilon-transitive epsilon-connected ordinal set
<%a%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) V53() set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
rng <%a%> is non empty V12() finite V35(1) set
A is set
{a} is non empty V12() finite V35(1) set
a is epsilon-transitive epsilon-connected ordinal set
<%a%> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding V53() set
dom <%a%> is non empty V12() epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() V35(1) ext-real positive non negative Element of K19(NAT)
<%a%> . 0 is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
<%a%> . b is epsilon-transitive epsilon-connected ordinal set
<%a%> . c3 is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
dom <%a%> is non empty V12() epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() V35(1) ext-real positive non negative set
<%a%> . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
<%a%> . b is epsilon-transitive epsilon-connected ordinal set
the epsilon-transitive epsilon-connected ordinal set is epsilon-transitive epsilon-connected ordinal set
<% the epsilon-transitive epsilon-connected ordinal set %> is Relation-like NAT -defined Function-like constant non empty V12() T-Sequence-like finite V35(1) Ordinal-yielding increasing V53() () () () set
a is Relation-like Function-like T-Sequence-like Ordinal-yielding () set
dom a is epsilon-transitive epsilon-connected ordinal set
Union a is epsilon-transitive epsilon-connected ordinal set
rng a is set
union (rng a) is set
the epsilon-transitive epsilon-connected ordinal Element of dom a is epsilon-transitive epsilon-connected ordinal Element of dom a
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
s is set
a . s is set
c is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
a . c is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
c3 *^ (exp (NAT,a)) is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
exp (NAT,(succ a)) is epsilon-transitive epsilon-connected ordinal set
NAT *^ (exp (NAT,a)) is epsilon-transitive epsilon-connected ordinal set
a 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
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
exp (a,c3) is epsilon-transitive epsilon-connected ordinal set
exp (a,b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
exp (a,{}) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (a,c3) is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
exp (a,(succ c3)) is epsilon-transitive epsilon-connected ordinal set
a *^ (exp (a,c3)) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (a,c3) is epsilon-transitive epsilon-connected ordinal set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
lim b is epsilon-transitive epsilon-connected ordinal set
Union b is epsilon-transitive epsilon-connected ordinal set
rng b is set
union (rng b) is set
s is epsilon-transitive epsilon-connected ordinal set
succ s is non empty epsilon-transitive epsilon-connected ordinal set
c is set
b . c is set
A is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
b . A is epsilon-transitive epsilon-connected ordinal set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
b . (succ A) is epsilon-transitive epsilon-connected ordinal set
exp (a,(succ A)) is epsilon-transitive epsilon-connected ordinal set
a 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
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
exp (a,c3) is epsilon-transitive epsilon-connected ordinal set
exp (a,b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
c3 is set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
Union b is epsilon-transitive epsilon-connected ordinal set
rng b is set
union (rng b) is set
lim b is epsilon-transitive epsilon-connected ordinal set
s is set
b . s is set
c is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
exp (a,s) is epsilon-transitive epsilon-connected ordinal set
b . s is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (a,c3) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
s is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last s is epsilon-transitive epsilon-connected ordinal set
dom s is epsilon-transitive epsilon-connected ordinal set
union (dom s) is epsilon-transitive epsilon-connected ordinal set
s . (union (dom s)) is epsilon-transitive epsilon-connected ordinal set
s . {} is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
c is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last c is epsilon-transitive epsilon-connected ordinal set
dom c is epsilon-transitive epsilon-connected ordinal set
union (dom c) is epsilon-transitive epsilon-connected ordinal set
c . (union (dom c)) is epsilon-transitive epsilon-connected ordinal set
c . {} is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
B is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last B is epsilon-transitive epsilon-connected ordinal set
dom B is epsilon-transitive epsilon-connected ordinal set
union (dom B) is epsilon-transitive epsilon-connected ordinal set
B . (union (dom B)) is epsilon-transitive epsilon-connected ordinal set
B . {} is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,0) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(a,A) is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last c is epsilon-transitive epsilon-connected ordinal set
dom c is epsilon-transitive epsilon-connected ordinal set
union (dom c) is epsilon-transitive epsilon-connected ordinal set
c . (union (dom c)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
c . {} is epsilon-transitive epsilon-connected ordinal set
(a,b) is epsilon-transitive epsilon-connected ordinal set
(a,{}) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
(a,(succ A)) is epsilon-transitive epsilon-connected ordinal set
(a,A) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,A)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
(a,c3) is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last A is epsilon-transitive epsilon-connected ordinal set
dom A is epsilon-transitive epsilon-connected ordinal set
union (dom A) is epsilon-transitive epsilon-connected ordinal set
A . (union (dom A)) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
succ s is non empty epsilon-transitive epsilon-connected ordinal set
A . {} is epsilon-transitive epsilon-connected ordinal set
(a,s) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(A,a) is epsilon-transitive epsilon-connected ordinal set
c3 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom c3 is epsilon-transitive epsilon-connected ordinal set
lim c3 is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
(A,b) is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
B is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last B is epsilon-transitive epsilon-connected ordinal set
dom B is epsilon-transitive epsilon-connected ordinal set
union (dom B) is epsilon-transitive epsilon-connected ordinal set
B . (union (dom B)) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
succ c is non empty epsilon-transitive epsilon-connected ordinal set
B . {} is epsilon-transitive epsilon-connected ordinal set
(A,c) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,1) is epsilon-transitive epsilon-connected ordinal set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(a,0) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,0)) is epsilon-transitive epsilon-connected ordinal set
exp (a,1) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(1,a) is epsilon-transitive epsilon-connected ordinal set
(1,{}) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(1,A) is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
(1,(succ A)) is epsilon-transitive epsilon-connected ordinal set
exp (1,1) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(1,A) is epsilon-transitive epsilon-connected ordinal set
c3 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom c3 is epsilon-transitive epsilon-connected ordinal set
lim c3 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
c is epsilon-transitive epsilon-connected ordinal set
(1,c) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
the epsilon-transitive epsilon-connected ordinal Element of A is epsilon-transitive epsilon-connected ordinal Element of A
A is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
c9 is epsilon-transitive epsilon-connected ordinal set
c3 . c9 is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,2) is epsilon-transitive epsilon-connected ordinal set
exp (a,a) is epsilon-transitive epsilon-connected ordinal set
succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(a,1) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,1)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,3) is epsilon-transitive epsilon-connected ordinal set
exp (a,a) is epsilon-transitive epsilon-connected ordinal set
exp (a,(exp (a,a))) is epsilon-transitive epsilon-connected ordinal set
succ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(a,2) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,2)) is epsilon-transitive epsilon-connected ordinal set
2 * 0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V21() V22() finite finite-yielding finite-membered V33() V35( {} ) ext-real non positive non negative Ordinal-yielding increasing V53() () () () Element of NAT
(0,(2 * 0)) is epsilon-transitive epsilon-connected ordinal set
(2 * 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(0,((2 * 0) + 1)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
2 * a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
(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
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
2 * (a + 1) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
(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
exp (0,0) 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 (0,1) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
(c3,a) is epsilon-transitive epsilon-connected ordinal set
(c3,A) is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
b is epsilon-transitive epsilon-connected ordinal set
(c3,b) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
(c3,s) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
(c3,(succ b)) is epsilon-transitive epsilon-connected ordinal set
(c3,b) is epsilon-transitive epsilon-connected ordinal set
exp (c3,(c3,b)) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
(c3,s) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
(c3,c) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
s is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom s is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
s . c is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
s . A is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
c9 is epsilon-transitive epsilon-connected ordinal set
(c3,B) is epsilon-transitive epsilon-connected ordinal set
(c3,c9) is epsilon-transitive epsilon-connected ordinal set
(c3,c) is epsilon-transitive epsilon-connected ordinal set
(c3,A) is epsilon-transitive epsilon-connected ordinal set
Union s is epsilon-transitive epsilon-connected ordinal set
rng s is set
union (rng s) is set
(c3,b) is epsilon-transitive epsilon-connected ordinal set
lim s is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
(c3,c) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(c3,A) is epsilon-transitive epsilon-connected ordinal set
s . c is epsilon-transitive epsilon-connected ordinal set
a 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
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
(a,c3) is epsilon-transitive epsilon-connected ordinal set
(a,b) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(a,A) is epsilon-transitive epsilon-connected ordinal set
(a,0) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
(a,c3) is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
(a,(succ c3)) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,c3)) is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
exp (a,1) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
b . s is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
b . c is epsilon-transitive epsilon-connected ordinal set
(a,c) is epsilon-transitive epsilon-connected ordinal set
(a,s) is epsilon-transitive epsilon-connected ordinal set
Union b is epsilon-transitive epsilon-connected ordinal set
rng b is set
union (rng b) is set
lim b is epsilon-transitive epsilon-connected ordinal set
(a,c3) is epsilon-transitive epsilon-connected ordinal set
b . 1 is epsilon-transitive epsilon-connected ordinal set
(a,1) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,A) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,c3) is epsilon-transitive epsilon-connected ordinal set
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(A + 1) + b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,0) is epsilon-transitive epsilon-connected ordinal set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,(0 + 1)) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,s) is epsilon-transitive epsilon-connected ordinal set
s + 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)) is epsilon-transitive epsilon-connected ordinal set
succ s is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
succ (s + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative 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 + 1) + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,((A + 1) + 0)) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(A + 1) + s 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)) 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
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(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 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
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
A . s is epsilon-transitive epsilon-connected ordinal set
(a,s) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
A . c is epsilon-transitive epsilon-connected ordinal set
(a,c) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(a,A) is epsilon-transitive epsilon-connected ordinal set
succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(a,1) is epsilon-transitive epsilon-connected ordinal set
(a,2) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
exp (a,0) is epsilon-transitive epsilon-connected ordinal set
a |^ 0 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
a |^ A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
succ A is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
exp (a,(A + 1)) is epsilon-transitive epsilon-connected ordinal set
a *^ (exp (a,A)) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
c3 * b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
a |^ (A + 1) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
a |^ A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,A) is epsilon-transitive epsilon-connected ordinal set
(a,0) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,c3) is epsilon-transitive epsilon-connected ordinal set
c3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
succ c3 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(a,(c3 + 1)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
exp (a,b) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,A) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,0) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,c3) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
c3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(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
a |^ (a,c3) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a |^ c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,NAT) 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
c3 is set
b is set
A . b is set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
(a,s) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
lim A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
(a,s) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
(a,B) is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
A . B is epsilon-transitive epsilon-connected ordinal set
A . A is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,NAT) 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
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
A . s is epsilon-transitive epsilon-connected ordinal set
(a,s) is epsilon-transitive epsilon-connected ordinal set
(a,c) is epsilon-transitive epsilon-connected ordinal set
lim A is epsilon-transitive epsilon-connected ordinal set
sup A is epsilon-transitive epsilon-connected ordinal set
rng A is set
sup (rng A) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,NAT) is epsilon-transitive epsilon-connected ordinal set
exp (a,(a,NAT)) is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom A is epsilon-transitive epsilon-connected ordinal set
c3 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom c3 is epsilon-transitive epsilon-connected ordinal set
lim c3 is epsilon-transitive epsilon-connected ordinal set
Union c3 is epsilon-transitive epsilon-connected ordinal set
rng c3 is set
union (rng c3) is set
lim A is epsilon-transitive epsilon-connected ordinal set
Union A is epsilon-transitive epsilon-connected ordinal 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
A is epsilon-transitive epsilon-connected ordinal set
exp (a,A) is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
A . B is epsilon-transitive epsilon-connected ordinal set
exp (a,(A . B)) is epsilon-transitive epsilon-connected ordinal set
succ B is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
c3 . A is epsilon-transitive epsilon-connected ordinal set
(a,B) is epsilon-transitive epsilon-connected ordinal set
A . (succ B) is epsilon-transitive epsilon-connected ordinal set
(a,(succ B)) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a,NAT) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(a,A) is epsilon-transitive epsilon-connected ordinal set
A -^ NAT is epsilon-transitive epsilon-connected ordinal set
NAT +^ (A -^ NAT) is epsilon-transitive epsilon-connected ordinal set
NAT +^ {} is epsilon-transitive epsilon-connected ordinal set
(a,(NAT +^ {})) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
NAT +^ c3 is epsilon-transitive epsilon-connected ordinal set
(a,(NAT +^ c3)) is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
NAT +^ (succ 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
succ (NAT +^ c3) is non empty epsilon-transitive epsilon-connected ordinal set
(a,(succ (NAT +^ c3))) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
NAT +^ c3 is epsilon-transitive epsilon-connected ordinal set
(a,(NAT +^ c3)) is epsilon-transitive epsilon-connected ordinal set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
lim b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
A is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite V33() V34() set
B is epsilon-transitive epsilon-connected ordinal set
B -^ A is epsilon-transitive epsilon-connected ordinal set
(NAT +^ c3) -^ NAT is epsilon-transitive epsilon-connected ordinal set
NAT +^ (B -^ A) is epsilon-transitive epsilon-connected ordinal set
(a,(NAT +^ (B -^ A))) is epsilon-transitive epsilon-connected ordinal set
(a,B) is epsilon-transitive epsilon-connected ordinal set
b . B is epsilon-transitive epsilon-connected ordinal set
F2() is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom F2() is epsilon-transitive epsilon-connected ordinal set
F2() . 0 is epsilon-transitive epsilon-connected ordinal set
F1() is epsilon-transitive epsilon-connected ordinal set
Union F2() 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
A is epsilon-transitive epsilon-connected ordinal set
F3(A) is epsilon-transitive epsilon-connected ordinal set
F3(F3(A)) is epsilon-transitive epsilon-connected ordinal set
F3(F1()) is epsilon-transitive epsilon-connected ordinal set
A is set
F2() . A is set
b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
F2() . b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . (succ b) is epsilon-transitive epsilon-connected ordinal set
b + 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
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
F2() . c3 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
A is epsilon-transitive epsilon-connected ordinal set
F3(A) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
F2() . (succ A) is epsilon-transitive epsilon-connected ordinal set
F2() . A is epsilon-transitive epsilon-connected ordinal set
F3((F2() . A)) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
F2() . A is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
F2() . (succ A) is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . (succ 0) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
F2() . b is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . (succ b) is epsilon-transitive epsilon-connected ordinal set
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(b + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
succ (b + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
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
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
F2() . c3 is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . (succ c3) 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
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . 1 is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
b is set
F2() . b is set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
F2() . s is epsilon-transitive epsilon-connected ordinal set
succ s is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . (succ s) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
F3(c3) is epsilon-transitive epsilon-connected ordinal set
F3(b) is epsilon-transitive epsilon-connected ordinal set
sup A is epsilon-transitive epsilon-connected ordinal set
rng A is set
sup (rng A) is epsilon-transitive epsilon-connected ordinal set
lim A is epsilon-transitive epsilon-connected ordinal set
c3 is set
b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c is set
A . c is set
A is epsilon-transitive epsilon-connected ordinal set
B is set
F2() . B is set
c9 is epsilon-transitive epsilon-connected ordinal set
F2() . c9 is epsilon-transitive epsilon-connected ordinal set
succ c9 is non empty epsilon-transitive epsilon-connected ordinal set
F2() . (succ c9) is epsilon-transitive epsilon-connected ordinal set
F3((F2() . c9)) is epsilon-transitive epsilon-connected ordinal set
F3(A) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
F3(c3) is epsilon-transitive epsilon-connected ordinal set
b is set
s is set
F2() . s is set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
F2() . A is epsilon-transitive epsilon-connected ordinal set
F3((F2() . A)) is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
F2() . (succ A) is epsilon-transitive epsilon-connected ordinal set
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
F2() . (A + 1) is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
F2() . c is epsilon-transitive epsilon-connected ordinal set
union c3 is epsilon-transitive epsilon-connected ordinal set
F1() is epsilon-transitive epsilon-connected ordinal set
succ F1() is non empty 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
a . {} is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
F2(A) is epsilon-transitive epsilon-connected ordinal set
F2(F2(A)) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
F2(A) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
a . 0 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a . b is epsilon-transitive epsilon-connected ordinal set
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
succ b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
a . (b + 1) is epsilon-transitive epsilon-connected ordinal set
F2((a . b)) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
a . c3 is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is epsilon-transitive epsilon-connected ordinal set
A +^ {} is epsilon-transitive epsilon-connected ordinal set
a . (A +^ {}) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A +^ b is epsilon-transitive epsilon-connected ordinal set
a . (A +^ b) is epsilon-transitive epsilon-connected ordinal set
succ b is non empty epsilon-transitive epsilon-connected ordinal set
A +^ (succ b) is epsilon-transitive epsilon-connected ordinal set
a . (A +^ (succ b)) is epsilon-transitive epsilon-connected ordinal set
succ (A +^ b) is non empty epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
F2(s) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A +^ b is epsilon-transitive epsilon-connected ordinal set
a . (A +^ b) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A +^ b is epsilon-transitive epsilon-connected ordinal set
sup a is epsilon-transitive epsilon-connected ordinal set
rng a is set
sup (rng a) 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
F2((sup a)) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
F2(c3) is epsilon-transitive epsilon-connected ordinal set
F2(b) is epsilon-transitive epsilon-connected ordinal set
sup A is epsilon-transitive epsilon-connected ordinal set
rng A is set
sup (rng A) is epsilon-transitive epsilon-connected ordinal set
lim A is epsilon-transitive epsilon-connected ordinal set
c3 is set
b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c is set
A . c is set
A is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
c9 is set
a . c9 is set
c is epsilon-transitive epsilon-connected ordinal set
succ c is non empty epsilon-transitive epsilon-connected ordinal set
a . (succ c) is epsilon-transitive epsilon-connected ordinal set
F2(B) is epsilon-transitive epsilon-connected ordinal set
F2(A) is epsilon-transitive epsilon-connected ordinal set
a . 0 is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,c3) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
c3 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
c3 . b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c3 . s is epsilon-transitive epsilon-connected ordinal set
exp (NAT,b) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,s) is epsilon-transitive epsilon-connected ordinal set
Union c3 is epsilon-transitive epsilon-connected ordinal set
rng c3 is set
union (rng c3) is set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
lim c3 is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal () set
b is epsilon-transitive epsilon-connected ordinal () set
A is epsilon-transitive epsilon-connected ordinal () set
c3 is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal () set
A is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal () set
a is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal () set
A is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal () set
c3 is epsilon-transitive epsilon-connected ordinal () set
(0) is epsilon-transitive epsilon-connected ordinal () set
(NAT,NAT) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
a 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
c3 is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
exp (NAT,c3) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,b) is epsilon-transitive epsilon-connected ordinal set
Union A is epsilon-transitive epsilon-connected ordinal set
rng A is set
union (rng A) is set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
lim A 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
a . {} is epsilon-transitive epsilon-connected ordinal set
a . 0 is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
a . (succ A) is epsilon-transitive epsilon-connected ordinal set
a . A is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(a . A)) is epsilon-transitive epsilon-connected ordinal set
Union a is epsilon-transitive epsilon-connected ordinal set
rng a is set
union (rng a) is set
exp (NAT,(Union a)) is epsilon-transitive epsilon-connected ordinal set
(NAT,0) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a . c3 is epsilon-transitive epsilon-connected ordinal set
(NAT,c3) is epsilon-transitive epsilon-connected ordinal set
c3 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
a . (c3 + 1) is epsilon-transitive epsilon-connected ordinal set
(NAT,(c3 + 1)) is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
exp (NAT,(a . c3)) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is epsilon-transitive epsilon-connected ordinal set
(NAT,c3) is epsilon-transitive epsilon-connected ordinal set
lim a is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
a . c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
a . b is epsilon-transitive epsilon-connected ordinal set
(NAT,c3) is epsilon-transitive epsilon-connected ordinal set
(NAT,b) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
a . s is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
(NAT,c) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal () set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
c3 is epsilon-transitive epsilon-connected ordinal () set
exp (NAT,c3) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal () set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,0) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,1) is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
a is epsilon-transitive epsilon-connected ordinal set
exp (NAT,0) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
a is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
exp (a,NAT) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(exp (a,NAT))) is epsilon-transitive epsilon-connected ordinal set
exp (a,(exp (a,NAT))) is epsilon-transitive epsilon-connected ordinal set
1 +^ NAT is epsilon-transitive epsilon-connected ordinal set
exp (a,(1 +^ NAT)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(exp (a,(1 +^ NAT)))) is epsilon-transitive epsilon-connected ordinal set
exp (a,1) 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 (a,NAT)) *^ a is epsilon-transitive epsilon-connected ordinal set
exp (NAT,((exp (a,NAT)) *^ a)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
exp ((exp (NAT,a)),(exp (a,NAT))) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
a + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
A is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () 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,a) 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
succ (a + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative 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 (NAT,A) 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
succ a is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
(A,(succ a)) is epsilon-transitive epsilon-connected ordinal set
(A,(succ a)) *^ 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,1) 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
1 +^ (A,a) 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
(a) is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
(a,NAT) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,c3) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
c3 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom c3 is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
c3 . b is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal set
c3 . s is epsilon-transitive epsilon-connected ordinal set
exp (NAT,b) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,s) is epsilon-transitive epsilon-connected ordinal set
Union c3 is epsilon-transitive epsilon-connected ordinal set
rng c3 is set
union (rng c3) is set
exp (NAT,A) is epsilon-transitive epsilon-connected ordinal set
lim c3 is epsilon-transitive epsilon-connected ordinal set
succ a is non empty 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
A . {} is epsilon-transitive epsilon-connected ordinal set
A . 0 is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
A . (succ c3) is epsilon-transitive epsilon-connected ordinal set
A . c3 is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(A . c3)) is epsilon-transitive epsilon-connected ordinal set
Union A is epsilon-transitive epsilon-connected ordinal set
rng A is set
union (rng A) is set
exp (NAT,(Union A)) is epsilon-transitive epsilon-connected ordinal set
c3 is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
b is non empty V12() epsilon-transitive epsilon-connected ordinal limit_ordinal non finite () set
exp (NAT,b) is epsilon-transitive epsilon-connected ordinal set
succ 0 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
succ 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
succ 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
A . 1 is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(succ a)) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,a) is epsilon-transitive epsilon-connected ordinal set
NAT *^ H1(a) is epsilon-transitive epsilon-connected ordinal set
NAT *^ a is epsilon-transitive epsilon-connected ordinal set
A . 2 is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(NAT *^ a)) is epsilon-transitive epsilon-connected ordinal set
exp (H1(a),NAT) is epsilon-transitive epsilon-connected ordinal set
exp (a,NAT) is epsilon-transitive epsilon-connected ordinal set
A . 3 is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(exp (a,NAT))) is epsilon-transitive epsilon-connected ordinal set
exp (a,(exp (a,NAT))) is epsilon-transitive epsilon-connected ordinal set
(a,0) is epsilon-transitive epsilon-connected ordinal set
(a,1) is epsilon-transitive epsilon-connected ordinal set
(a,2) is epsilon-transitive epsilon-connected ordinal set
exp (a,a) is epsilon-transitive epsilon-connected ordinal set
exp (a,1) is epsilon-transitive epsilon-connected ordinal set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
A . (0 + 1) is epsilon-transitive epsilon-connected ordinal set
0 + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,(0 + 2)) is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
(a,b) is epsilon-transitive epsilon-connected ordinal set
b + 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) is epsilon-transitive epsilon-connected ordinal set
A . b is epsilon-transitive epsilon-connected ordinal set
b + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(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
succ b is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative 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
succ (b + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative set
exp (NAT,(A . b)) is epsilon-transitive epsilon-connected ordinal set
A . ((b + 1) + 1) is epsilon-transitive epsilon-connected ordinal set
exp (NAT,(A . (b + 1))) is epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative set
2 + s is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
s + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(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
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom b is epsilon-transitive epsilon-connected ordinal set
lim b is epsilon-transitive epsilon-connected ordinal set
Union b 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 is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
A . A is epsilon-transitive epsilon-connected ordinal set
A + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,(A + 2)) is epsilon-transitive epsilon-connected ordinal set
b . (A + 2) is epsilon-transitive epsilon-connected ordinal set
s is set
c is set
b . c is set
A is epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real non negative Element of NAT
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V21() V22() finite V33() ext-real positive non negative Element of NAT
(a,A) is epsilon-transitive epsilon-connected ordinal set
A . (A + 1) is epsilon-transitive epsilon-connected ordinal set
b . A is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
b is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last b is epsilon-transitive epsilon-connected ordinal set
dom b is epsilon-transitive epsilon-connected ordinal set
union (dom b) is epsilon-transitive epsilon-connected ordinal set
b . (union (dom b)) is epsilon-transitive epsilon-connected ordinal set
b . {} is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
s is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last s is epsilon-transitive epsilon-connected ordinal set
dom s is epsilon-transitive epsilon-connected ordinal set
union (dom s) is epsilon-transitive epsilon-connected ordinal set
s . (union (dom s)) is epsilon-transitive epsilon-connected ordinal set
s . {} is epsilon-transitive epsilon-connected ordinal set
c is epsilon-transitive epsilon-connected ordinal set
A is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last A is epsilon-transitive epsilon-connected ordinal set
dom A is epsilon-transitive epsilon-connected ordinal set
union (dom A) is epsilon-transitive epsilon-connected ordinal set
A . (union (dom A)) is epsilon-transitive epsilon-connected ordinal set
A . {} is epsilon-transitive epsilon-connected ordinal set
(0) is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
s is Relation-like Function-like T-Sequence-like Ordinal-yielding set
last s is epsilon-transitive epsilon-connected ordinal set
dom s is epsilon-transitive epsilon-connected ordinal set
union (dom s) is epsilon-transitive epsilon-connected ordinal set
s . (union (dom s)) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
succ c3 is non empty epsilon-transitive epsilon-connected ordinal set
s . {} is epsilon-transitive epsilon-connected ordinal set
(c3) is epsilon-transitive epsilon-connected ordinal set
a is epsilon-transitive epsilon-connected ordinal set
succ a is non empty epsilon-transitive epsilon-connected ordinal set
((succ a)) is epsilon-transitive epsilon-connected ordinal set
(a) is epsilon-transitive epsilon-connected ordinal set
((a),NAT) is epsilon-transitive epsilon-connected ordinal set
c3 is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
(A) is epsilon-transitive epsilon-connected ordinal set
succ A is non empty epsilon-transitive epsilon-connected ordinal set
s is epsilon-transitive epsilon-connected <