REAL is complex-membered ext-real-membered real-membered V65() set
NAT is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal limit_cardinal countable denumerable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V65() Element of bool REAL
bool REAL is set
NAT is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal limit_cardinal countable denumerable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V65() set
bool NAT is non trivial non finite set
bool NAT is non trivial non finite set
{} is Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V37() finite V43() cardinal {} -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V65() set
the Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V37() finite V43() cardinal {} -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V65() set is Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V37() finite V43() cardinal {} -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V65() set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V35() V36() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
alef {} is epsilon-transitive epsilon-connected ordinal cardinal set
{{}} is non empty trivial finite V43() 1 -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
0 is Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V35() V37() V38() finite V43() cardinal {} -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V65() V69() Element of NAT
2 is epsilon-transitive epsilon-connected ordinal natural non empty V35() V36() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
card 1 is epsilon-transitive epsilon-connected ordinal natural non empty V35() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
card 2 is epsilon-transitive epsilon-connected ordinal natural non empty V35() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard (card F) is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard F is epsilon-transitive epsilon-connected ordinal cardinal set
card (card F) is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
n is Relation-like Function-like set
Union n is set
rng n is set
union (rng n) is set
dom n is set
X is set
phi is set
n . phi is set
X is set
n . X is set
F is epsilon-transitive epsilon-connected ordinal set
alef F is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard n is epsilon-transitive epsilon-connected ordinal cardinal set
card n is epsilon-transitive epsilon-connected ordinal cardinal set
X is finite countable set
card X is epsilon-transitive epsilon-connected ordinal natural V35() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
(card X) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V35() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
card ((card X) + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V35() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
X is epsilon-transitive epsilon-connected ordinal set
alef X is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal set
alef X is epsilon-transitive epsilon-connected ordinal cardinal set
succ X is epsilon-transitive epsilon-connected ordinal non empty set
alef (succ X) is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
phi is set
C is epsilon-transitive epsilon-connected ordinal cardinal set
x is epsilon-transitive epsilon-connected ordinal set
alef x is epsilon-transitive epsilon-connected ordinal cardinal set
phi is Relation-like Function-like set
dom phi is set
C is set
rng phi is set
x is set
phi . x is set
M is epsilon-transitive epsilon-connected ordinal set
alef M is epsilon-transitive epsilon-connected ordinal cardinal set
g1 is set
h1 is epsilon-transitive epsilon-connected ordinal set
alef h1 is epsilon-transitive epsilon-connected ordinal cardinal set
phi . (alef h1) is set
g2 is epsilon-transitive epsilon-connected ordinal set
alef g2 is epsilon-transitive epsilon-connected ordinal cardinal set
C is epsilon-transitive epsilon-connected ordinal set
x is Relation-like Function-like T-Sequence-like set
dom x is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal set
g1 is set
phi . g1 is set
h1 is epsilon-transitive epsilon-connected ordinal set
alef h1 is epsilon-transitive epsilon-connected ordinal cardinal set
succ h1 is epsilon-transitive epsilon-connected ordinal non empty set
alef (succ h1) is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard (alef h1) is epsilon-transitive epsilon-connected ordinal cardinal set
phi . (alef (succ h1)) is set
g2 is epsilon-transitive epsilon-connected ordinal set
alef g2 is epsilon-transitive epsilon-connected ordinal cardinal set
succ M is epsilon-transitive epsilon-connected ordinal non empty set
alef C is epsilon-transitive epsilon-connected ordinal cardinal set
sup x is epsilon-transitive epsilon-connected ordinal set
rng x is set
sup (rng x) is epsilon-transitive epsilon-connected ordinal set
card (sup x) is epsilon-transitive epsilon-connected ordinal cardinal set
M is set
g1 is epsilon-transitive epsilon-connected ordinal set
h1 is epsilon-transitive epsilon-connected ordinal set
g2 is set
x . g2 is set
h2 is epsilon-transitive epsilon-connected ordinal set
alef h2 is epsilon-transitive epsilon-connected ordinal cardinal set
x1 is set
phi . x1 is set
X is epsilon-transitive epsilon-connected ordinal set
alef X is epsilon-transitive epsilon-connected ordinal cardinal set
card n is epsilon-transitive epsilon-connected ordinal cardinal set
phi . (card (sup x)) is set
M is epsilon-transitive epsilon-connected ordinal set
alef M is epsilon-transitive epsilon-connected ordinal cardinal set
F is Relation-like Function-like T-Sequence-like Ordinal-yielding set
Union F is set
rng F is set
union (rng F) is set
On (rng F) is set
n is epsilon-transitive epsilon-connected ordinal set
F is epsilon-transitive epsilon-connected ordinal set
n is set
RelIncl n is Relation-like set
order_type_of (RelIncl n) is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of (RelIncl n)) is Relation-like well_founded set
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl n))),(RelIncl n)) is Relation-like Function-like set
field (RelIncl (order_type_of (RelIncl n))) is set
dom (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl n))),(RelIncl n))) is set
field (RelIncl n) is set
rng (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl n))),(RelIncl n))) is set
x is Relation-like Function-like T-Sequence-like set
M is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom M is epsilon-transitive epsilon-connected ordinal set
rng M is set
g1 is epsilon-transitive epsilon-connected ordinal set
h1 is epsilon-transitive epsilon-connected ordinal set
M . g1 is epsilon-transitive epsilon-connected ordinal set
M . h1 is epsilon-transitive epsilon-connected ordinal set
h2 is epsilon-transitive epsilon-connected ordinal set
[g1,h1] is non natural V24() set
{g1,h1} is non empty finite countable set
{g1} is non empty trivial finite 1 -element countable set
{{g1,h1},{g1}} is non empty finite V43() countable set
g2 is epsilon-transitive epsilon-connected ordinal set
[g2,h2] is non natural V24() set
{g2,h2} is non empty finite countable set
{g2} is non empty trivial finite 1 -element countable set
{{g2,h2},{g2}} is non empty finite V43() countable set
F is epsilon-transitive epsilon-connected ordinal set
n is set
sup n is epsilon-transitive epsilon-connected ordinal set
RelIncl n is Relation-like set
order_type_of (RelIncl n) is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of (RelIncl n)) is Relation-like well_founded set
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl n))),(RelIncl n)) is Relation-like Function-like set
X is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom X is epsilon-transitive epsilon-connected ordinal set
rng X is set
sup X is epsilon-transitive epsilon-connected ordinal set
sup (rng X) is epsilon-transitive epsilon-connected ordinal set
On n is set
F is epsilon-transitive epsilon-connected ordinal set
n is set
card n is epsilon-transitive epsilon-connected ordinal cardinal set
RelIncl n is Relation-like set
order_type_of (RelIncl n) is epsilon-transitive epsilon-connected ordinal set
card (order_type_of (RelIncl n)) is epsilon-transitive epsilon-connected ordinal cardinal set
RelIncl (order_type_of (RelIncl n)) is Relation-like well_founded set
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl n))),(RelIncl n)) is Relation-like Function-like set
field (RelIncl n) is set
rng (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl n))),(RelIncl n))) is set
field (RelIncl (order_type_of (RelIncl n))) is set
dom (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl n))),(RelIncl n))) is set
F is epsilon-transitive epsilon-connected ordinal set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like Function-like set
dom X is set
rng X is set
phi is Relation-like Function-like T-Sequence-like set
x is set
RelIncl x is Relation-like set
order_type_of (RelIncl x) is epsilon-transitive epsilon-connected ordinal set
h1 is set
RelIncl (order_type_of (RelIncl x)) is Relation-like well_founded set
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl x))),(RelIncl x)) is Relation-like Function-like set
field (RelIncl (order_type_of (RelIncl x))) is set
dom (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl x))),(RelIncl x))) is set
field (RelIncl x) is set
rng (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl x))),(RelIncl x))) is set
g2 is Relation-like Function-like T-Sequence-like set
h2 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
C is Relation-like Function-like T-Sequence-like Ordinal-yielding set
h2 * C is Relation-like Function-like set
dom (h2 * C) is set
rng (h2 * C) is set
x1 is Relation-like Function-like T-Sequence-like set
X is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom X is epsilon-transitive epsilon-connected ordinal set
rng X is set
sup X is epsilon-transitive epsilon-connected ordinal set
sup (rng X) is epsilon-transitive epsilon-connected ordinal set
A1 is epsilon-transitive epsilon-connected ordinal set
A2 is epsilon-transitive epsilon-connected ordinal set
X . A1 is epsilon-transitive epsilon-connected ordinal set
X . A2 is epsilon-transitive epsilon-connected ordinal set
h2 . A1 is epsilon-transitive epsilon-connected ordinal set
h2 . A2 is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
C . A is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
C . B is epsilon-transitive epsilon-connected ordinal set
f1 is epsilon-transitive epsilon-connected ordinal set
C | B is Relation-like rng C -valued Function-like T-Sequence-like Ordinal-yielding set
rng C is set
Union (C | B) is epsilon-transitive epsilon-connected ordinal set
rng (C | B) is set
union (rng (C | B)) is set
[A1,A2] is non natural V24() set
{A1,A2} is non empty finite countable set
{A1} is non empty trivial finite 1 -element countable set
{{A1,A2},{A1}} is non empty finite V43() countable set
[(h2 . A1),(h2 . A2)] is non natural V24() set
{(h2 . A1),(h2 . A2)} is non empty finite countable set
{(h2 . A1)} is non empty trivial finite 1 -element countable set
{{(h2 . A1),(h2 . A2)},{(h2 . A1)}} is non empty finite V43() countable set
x2 is epsilon-transitive epsilon-connected ordinal set
A1 is set
dom C is epsilon-transitive epsilon-connected ordinal set
A2 is set
C . A2 is set
B is epsilon-transitive epsilon-connected ordinal set
C . B is epsilon-transitive epsilon-connected ordinal set
C | B is Relation-like rng C -valued Function-like T-Sequence-like Ordinal-yielding set
rng C is set
Union (C | B) is epsilon-transitive epsilon-connected ordinal set
rng (C | B) is set
union (rng (C | B)) is set
x2 is set
h2 . x2 is set
A is epsilon-transitive epsilon-connected ordinal set
X . x2 is set
B is epsilon-transitive epsilon-connected ordinal set
C . B is epsilon-transitive epsilon-connected ordinal set
C | B is Relation-like rng C -valued Function-like T-Sequence-like Ordinal-yielding set
rng C is set
Union (C | B) is epsilon-transitive epsilon-connected ordinal set
rng (C | B) is set
union (rng (C | B)) is set
dom (C | B) is epsilon-transitive epsilon-connected ordinal set
x2 is set
(C | B) . x2 is set
f1 is epsilon-transitive epsilon-connected ordinal set
(C | B) . f1 is epsilon-transitive epsilon-connected ordinal set
C . f1 is epsilon-transitive epsilon-connected ordinal set
(dom C) /\ B is epsilon-transitive epsilon-connected ordinal set
f2 is epsilon-transitive epsilon-connected ordinal set
C . f2 is epsilon-transitive epsilon-connected ordinal set
C | f2 is Relation-like rng C -valued Function-like T-Sequence-like Ordinal-yielding set
Union (C | f2) is epsilon-transitive epsilon-connected ordinal set
rng (C | f2) is set
union (rng (C | f2)) is set
dom (C | f2) is epsilon-transitive epsilon-connected ordinal set
z is set
(C | f2) . z is set
z is epsilon-transitive epsilon-connected ordinal set
(C | f2) . z is epsilon-transitive epsilon-connected ordinal set
C . z is epsilon-transitive epsilon-connected ordinal set
xz is epsilon-transitive epsilon-connected ordinal set
fy is epsilon-transitive epsilon-connected ordinal set
(dom C) /\ f2 is epsilon-transitive epsilon-connected ordinal set
z is set
h2 . z is set
z is epsilon-transitive epsilon-connected ordinal set
X . z is epsilon-transitive epsilon-connected ordinal set
xz is epsilon-transitive epsilon-connected ordinal set
A is epsilon-transitive epsilon-connected ordinal set
B is epsilon-transitive epsilon-connected ordinal set
C . B is epsilon-transitive epsilon-connected ordinal set
C | B is Relation-like rng C -valued Function-like T-Sequence-like Ordinal-yielding set
rng C is set
Union (C | B) is epsilon-transitive epsilon-connected ordinal set
rng (C | B) is set
union (rng (C | B)) is set
sup F is epsilon-transitive epsilon-connected ordinal set
F is epsilon-transitive epsilon-connected ordinal set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal set
card n is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal cardinal set
phi is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
F is Relation-like Function-like T-Sequence-like Ordinal-yielding set
rng F is set
dom F is epsilon-transitive epsilon-connected ordinal set
n is Relation-like Function-like T-Sequence-like Ordinal-yielding set
rng n is set
dom n is epsilon-transitive epsilon-connected ordinal set
X is epsilon-transitive epsilon-connected ordinal set
F . X is epsilon-transitive epsilon-connected ordinal set
n . X is epsilon-transitive epsilon-connected ordinal set
phi is set
n . phi is set
C is epsilon-transitive epsilon-connected ordinal set
x is set
F . x is set
n . C is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal set
n . M is epsilon-transitive epsilon-connected ordinal set
F . M is epsilon-transitive epsilon-connected ordinal set
F . C is epsilon-transitive epsilon-connected ordinal set
F is Relation-like Function-like T-Sequence-like Ordinal-yielding set
rng F is set
n is Relation-like Function-like T-Sequence-like Ordinal-yielding set
rng n is set
dom F is epsilon-transitive epsilon-connected ordinal set
dom n is epsilon-transitive epsilon-connected ordinal set
X is set
X is set
X is set
F . X is set
n . X is set
F is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom F is epsilon-transitive epsilon-connected ordinal set
n is set
F . n is set
X is set
F . X is set
phi is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
F . phi is epsilon-transitive epsilon-connected ordinal set
F . C is epsilon-transitive epsilon-connected ordinal set
F is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom F is epsilon-transitive epsilon-connected ordinal set
n is Relation-like Function-like T-Sequence-like Ordinal-yielding set
F ^ n is Relation-like Function-like T-Sequence-like Ordinal-yielding set
(F ^ n) | (dom F) is Relation-like rng (F ^ n) -valued Function-like T-Sequence-like Ordinal-yielding set
rng (F ^ n) is set
dom (F ^ n) is epsilon-transitive epsilon-connected ordinal set
dom n is epsilon-transitive epsilon-connected ordinal set
(dom F) +^ (dom n) is epsilon-transitive epsilon-connected ordinal set
(dom (F ^ n)) /\ (dom F) is epsilon-transitive epsilon-connected ordinal set
X is set
F . X is set
(F ^ n) . X is set
F is set
bool F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal cardinal set
{ b1 where b1 is Element of bool F : card b1 in n } is set
card { b1 where b1 is Element of bool F : card b1 in n } is epsilon-transitive epsilon-connected ordinal cardinal set
exp ((card F),n) is epsilon-transitive epsilon-connected ordinal cardinal set
n *` (exp ((card F),n)) is epsilon-transitive epsilon-connected ordinal cardinal set
phi is Relation-like Function-like set
dom phi is set
rng phi is set
C is set
phi .: C is set
RelIncl (phi .: C) is Relation-like set
order_type_of (RelIncl (phi .: C)) is epsilon-transitive epsilon-connected ordinal set
n -^ (order_type_of (RelIncl (phi .: C))) is epsilon-transitive epsilon-connected ordinal set
M is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom M is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of (RelIncl (phi .: C))) is Relation-like well_founded set
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl (phi .: C)))),(RelIncl (phi .: C))) is Relation-like Function-like set
g1 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom g1 is epsilon-transitive epsilon-connected ordinal set
rng g1 is set
g1 ^ M is Relation-like Function-like T-Sequence-like Ordinal-yielding set
[(order_type_of (RelIncl (phi .: C))),(g1 ^ M)] is non natural V24() set
{(order_type_of (RelIncl (phi .: C))),(g1 ^ M)} is non empty finite countable set
{(order_type_of (RelIncl (phi .: C)))} is non empty trivial finite 1 -element countable set
{{(order_type_of (RelIncl (phi .: C))),(g1 ^ M)},{(order_type_of (RelIncl (phi .: C)))}} is non empty finite V43() countable set
g2 is non natural V24() set
dom (g1 ^ M) is epsilon-transitive epsilon-connected ordinal set
(g1 ^ M) | (order_type_of (RelIncl (phi .: C))) is Relation-like rng (g1 ^ M) -valued Function-like T-Sequence-like Ordinal-yielding set
rng (g1 ^ M) is set
rng ((g1 ^ M) | (order_type_of (RelIncl (phi .: C)))) is set
card (phi .: C) is epsilon-transitive epsilon-connected ordinal cardinal set
card (order_type_of (RelIncl (phi .: C))) is epsilon-transitive epsilon-connected ordinal cardinal set
h2 is Element of bool F
card h2 is epsilon-transitive epsilon-connected ordinal cardinal set
(order_type_of (RelIncl (phi .: C))) +^ (n -^ (order_type_of (RelIncl (phi .: C)))) is epsilon-transitive epsilon-connected ordinal set
h2 is epsilon-transitive epsilon-connected ordinal set
(g1 ^ M) . h2 is epsilon-transitive epsilon-connected ordinal set
h2 -^ (order_type_of (RelIncl (phi .: C))) is epsilon-transitive epsilon-connected ordinal set
(order_type_of (RelIncl (phi .: C))) +^ (h2 -^ (order_type_of (RelIncl (phi .: C)))) is epsilon-transitive epsilon-connected ordinal set
M . (h2 -^ (order_type_of (RelIncl (phi .: C)))) is epsilon-transitive epsilon-connected ordinal set
C is Relation-like Function-like set
dom C is set
rng C is set
Funcs (n,(card F)) is set
[:n,(Funcs (n,(card F))):] is set
x is set
M is set
C . M is set
phi .: M is set
g1 is epsilon-transitive epsilon-connected ordinal set
h1 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
[g1,h1] is non natural V24() set
{g1,h1} is non empty finite countable set
{g1} is non empty trivial finite 1 -element countable set
{{g1,h1},{g1}} is non empty finite V43() countable set
dom h1 is epsilon-transitive epsilon-connected ordinal set
h1 | g1 is Relation-like rng h1 -valued Function-like T-Sequence-like Ordinal-yielding set
rng h1 is set
rng (h1 | g1) is set
g2 is set
h2 is set
h1 . h2 is set
x1 is epsilon-transitive epsilon-connected ordinal set
dom (h1 | g1) is epsilon-transitive epsilon-connected ordinal set
card (dom (h1 | g1)) is epsilon-transitive epsilon-connected ordinal cardinal set
card (phi .: M) is epsilon-transitive epsilon-connected ordinal cardinal set
g2 is Element of bool F
card g2 is epsilon-transitive epsilon-connected ordinal cardinal set
card (rng C) is epsilon-transitive epsilon-connected ordinal cardinal set
card [:n,(Funcs (n,(card F))):] is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
C . x is set
M is set
C . M is set
phi .: M is set
g1 is epsilon-transitive epsilon-connected ordinal set
h1 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
[g1,h1] is non natural V24() set
{g1,h1} is non empty finite countable set
{g1} is non empty trivial finite 1 -element countable set
{{g1,h1},{g1}} is non empty finite V43() countable set
dom h1 is epsilon-transitive epsilon-connected ordinal set
h1 | g1 is Relation-like rng h1 -valued Function-like T-Sequence-like Ordinal-yielding set
rng h1 is set
rng (h1 | g1) is set
phi .: x is set
g2 is epsilon-transitive epsilon-connected ordinal set
h2 is Relation-like Function-like T-Sequence-like Ordinal-yielding set
[g2,h2] is non natural V24() set
{g2,h2} is non empty finite countable set
{g2} is non empty trivial finite 1 -element countable set
{{g2,h2},{g2}} is non empty finite V43() countable set
dom h2 is epsilon-transitive epsilon-connected ordinal set
h2 | g2 is Relation-like rng h2 -valued Function-like T-Sequence-like Ordinal-yielding set
rng h2 is set
rng (h2 | g2) is set
x1 is set
phi . x1 is set
X is Element of bool F
card X is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
phi . X is set
A1 is Element of bool F
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
x1 is set
phi . x1 is set
X is Element of bool F
card X is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
phi . X is set
A1 is Element of bool F
card A1 is epsilon-transitive epsilon-connected ordinal cardinal set
card (Funcs (n,(card F))) is epsilon-transitive epsilon-connected ordinal cardinal set
[:n,(card (Funcs (n,(card F)))):] is set
card [:n,(card (Funcs (n,(card F)))):] is epsilon-transitive epsilon-connected ordinal cardinal set
n *` (card (Funcs (n,(card F)))) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
exp (2,F) is epsilon-transitive epsilon-connected ordinal cardinal set
bool F is set
card (bool F) is epsilon-transitive epsilon-connected ordinal cardinal set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
exp (2,(card F)) is epsilon-transitive epsilon-connected ordinal cardinal set
F is set
F is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal set
X is epsilon-transitive epsilon-connected ordinal cardinal set
phi is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal cardinal set
X is set
phi is Relation-like Function-like Cardinal-yielding set
dom phi is set
C is set
x is set
C is epsilon-transitive epsilon-connected ordinal cardinal set
phi . C is set
exp (C,n) is epsilon-transitive epsilon-connected ordinal cardinal set
card C is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like Function-like Cardinal-yielding set
dom X is set
phi is Relation-like Function-like Cardinal-yielding set
dom phi is set
C is set
x is epsilon-transitive epsilon-connected ordinal cardinal set
X . C is set
exp (x,n) is epsilon-transitive epsilon-connected ordinal cardinal set
phi . C is set
F is epsilon-transitive epsilon-connected ordinal set
alef F is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
F is epsilon-transitive epsilon-connected ordinal natural V35() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
card F is epsilon-transitive epsilon-connected ordinal natural V35() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
n +` F is epsilon-transitive epsilon-connected ordinal cardinal set
F +` n is epsilon-transitive epsilon-connected ordinal cardinal set
n *` F is epsilon-transitive epsilon-connected ordinal cardinal set
F *` n is epsilon-transitive epsilon-connected ordinal cardinal set
card 0 is Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V35() V37() V38() finite V43() cardinal {} -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V65() V69() Element of NAT
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
F +` F is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
n *` n is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
exp (F,n) is epsilon-transitive epsilon-connected ordinal cardinal set
exp (F,1) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
union F is epsilon-transitive epsilon-connected ordinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
n is epsilon-transitive epsilon-connected ordinal cardinal set
F +` n is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
F +` n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
F *` n is epsilon-transitive epsilon-connected ordinal cardinal set
exp (F,n) is epsilon-transitive epsilon-connected ordinal cardinal set
exp (F,1) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
nextcard F is epsilon-transitive epsilon-connected ordinal cardinal set
(NAT) is epsilon-transitive epsilon-connected ordinal cardinal set
F is finite countable set
card F is epsilon-transitive epsilon-connected ordinal natural V35() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
phi is set
X is set
phi is set
X is set
C is set
card (NAT) is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom X is epsilon-transitive epsilon-connected ordinal set
rng X is set
sup X is epsilon-transitive epsilon-connected ordinal set
sup (rng X) is epsilon-transitive epsilon-connected ordinal set
phi is finite countable set
C is set
M is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
succ x is epsilon-transitive epsilon-connected ordinal non empty set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
nextcard F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
((nextcard F)) is epsilon-transitive epsilon-connected ordinal cardinal set
n is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom n is epsilon-transitive epsilon-connected ordinal set
rng n is set
sup n is epsilon-transitive epsilon-connected ordinal set
sup (rng n) is epsilon-transitive epsilon-connected ordinal set
Union n is epsilon-transitive epsilon-connected ordinal set
union (rng n) is set
card (Union n) is epsilon-transitive epsilon-connected ordinal cardinal set
Card n is Relation-like Function-like Cardinal-yielding set
Sum (Card n) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin (Card n) is Relation-like Function-like set
Union (disjoin (Card n)) is set
rng (disjoin (Card n)) is set
union (rng (disjoin (Card n))) is set
card (Union (disjoin (Card n))) is epsilon-transitive epsilon-connected ordinal cardinal set
((nextcard F)) --> F is Relation-like non-empty ((nextcard F)) -defined Function-like constant T-Sequence-like V23(((nextcard F))) quasi_total Ordinal-yielding Cardinal-yielding Element of bool [:((nextcard F)),{F}:]
{F} is non empty trivial finite 1 -element countable set
[:((nextcard F)),{F}:] is set
bool [:((nextcard F)),{F}:] is set
Sum (((nextcard F)) --> F) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin (((nextcard F)) --> F) is Relation-like Function-like set
Union (disjoin (((nextcard F)) --> F)) is set
rng (disjoin (((nextcard F)) --> F)) is set
union (rng (disjoin (((nextcard F)) --> F))) is set
card (Union (disjoin (((nextcard F)) --> F))) is epsilon-transitive epsilon-connected ordinal cardinal set
((nextcard F)) *` F is epsilon-transitive epsilon-connected ordinal cardinal set
card (nextcard F) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
succ (Union n) is epsilon-transitive epsilon-connected ordinal non empty set
(Union n) +^ 1 is epsilon-transitive epsilon-connected ordinal set
X is set
n . X is set
card (n . X) is epsilon-transitive epsilon-connected ordinal cardinal set
(Card n) . X is set
(((nextcard F)) --> F) . X is set
dom (Card n) is set
dom (((nextcard F)) --> F) is epsilon-transitive epsilon-connected ordinal set
(card (Union n)) +` 1 is epsilon-transitive epsilon-connected ordinal cardinal set
(((nextcard F)) *` F) +` 1 is epsilon-transitive epsilon-connected ordinal cardinal set
card ((Union n) +^ 1) is epsilon-transitive epsilon-connected ordinal cardinal set
(card (Union n)) +` (card 1) is epsilon-transitive epsilon-connected ordinal cardinal set
On (rng n) is set
X is epsilon-transitive epsilon-connected ordinal set
card (succ (Union n)) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
0 +` 1 is epsilon-transitive epsilon-connected ordinal cardinal set
F +` 1 is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
((nextcard F)) +` 1 is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
(F) is epsilon-transitive epsilon-connected ordinal cardinal set
(0) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal natural V35() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
F + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V35() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
card (F + 1) is epsilon-transitive epsilon-connected ordinal natural non empty V35() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
((card (F + 1))) is epsilon-transitive epsilon-connected ordinal cardinal set
succ F is epsilon-transitive epsilon-connected ordinal natural non empty V37() finite cardinal countable set
F is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
sup F is epsilon-transitive epsilon-connected ordinal set
union F is set
n is epsilon-transitive epsilon-connected ordinal cardinal set
(n) is epsilon-transitive epsilon-connected ordinal cardinal set
RelIncl F is Relation-like set
order_type_of (RelIncl F) is epsilon-transitive epsilon-connected ordinal set
card (order_type_of (RelIncl F)) is epsilon-transitive epsilon-connected ordinal cardinal set
phi is epsilon-transitive epsilon-connected ordinal cardinal set
C is set
sup n is epsilon-transitive epsilon-connected ordinal set
C is epsilon-transitive epsilon-connected ordinal set
x is set
M is set
g1 is epsilon-transitive epsilon-connected ordinal set
F is epsilon-transitive epsilon-connected ordinal cardinal set
n is epsilon-transitive epsilon-connected ordinal cardinal set
(n) is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom X is epsilon-transitive epsilon-connected ordinal set
rng X is set
sup X is epsilon-transitive epsilon-connected ordinal set
sup (rng X) is epsilon-transitive epsilon-connected ordinal set
Union X is epsilon-transitive epsilon-connected ordinal set
union (rng X) is set
card F is epsilon-transitive epsilon-connected ordinal cardinal set
card (rng X) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
(F) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
(F) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
n is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard n is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
nextcard X is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
(F) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
n is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom n is epsilon-transitive epsilon-connected ordinal set
rng n is set
sup n is epsilon-transitive epsilon-connected ordinal set
sup (rng n) is epsilon-transitive epsilon-connected ordinal set
X is Relation-like Function-like T-Sequence-like set
dom X is epsilon-transitive epsilon-connected ordinal set
rng X is set
sup (rng X) is epsilon-transitive epsilon-connected ordinal set
phi is set
C is set
X . C is set
x is epsilon-transitive epsilon-connected ordinal set
X | x is Relation-like rng X -valued Function-like T-Sequence-like set
dom (X | x) is epsilon-transitive epsilon-connected ordinal set
n . x is epsilon-transitive epsilon-connected ordinal set
nextcard (n . x) is epsilon-transitive epsilon-connected ordinal cardinal set
sup (X | x) is epsilon-transitive epsilon-connected ordinal set
rng (X | x) is set
sup (rng (X | x)) is epsilon-transitive epsilon-connected ordinal set
nextcard (sup (X | x)) is epsilon-transitive epsilon-connected ordinal cardinal set
(nextcard (n . x)) \/ (nextcard (sup (X | x))) is epsilon-transitive epsilon-connected ordinal set
phi is Relation-like Function-like T-Sequence-like Ordinal-yielding set
C is epsilon-transitive epsilon-connected ordinal set
phi . C is epsilon-transitive epsilon-connected ordinal set
card C is epsilon-transitive epsilon-connected ordinal cardinal set
dom phi is epsilon-transitive epsilon-connected ordinal set
phi | C is Relation-like rng phi -valued Function-like T-Sequence-like Ordinal-yielding set
rng phi is set
dom (phi | C) is epsilon-transitive epsilon-connected ordinal set
n . C is epsilon-transitive epsilon-connected ordinal set
nextcard (n . C) is epsilon-transitive epsilon-connected ordinal cardinal set
sup (phi | C) is epsilon-transitive epsilon-connected ordinal set
rng (phi | C) is set
sup (rng (phi | C)) is epsilon-transitive epsilon-connected ordinal set
nextcard (sup (phi | C)) is epsilon-transitive epsilon-connected ordinal cardinal set
(nextcard (n . C)) \/ (nextcard (sup (phi | C))) is epsilon-transitive epsilon-connected ordinal set
x is set
M is set
(phi | C) . M is set
g1 is epsilon-transitive epsilon-connected ordinal set
phi . g1 is epsilon-transitive epsilon-connected ordinal set
(phi | C) .: C is set
card (rng (phi | C)) is epsilon-transitive epsilon-connected ordinal cardinal set
card (sup (phi | C)) is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard (card (sup (phi | C))) is epsilon-transitive epsilon-connected ordinal cardinal set
card (n . C) is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard (card (n . C)) is epsilon-transitive epsilon-connected ordinal cardinal set
rng phi is set
C is set
dom phi is epsilon-transitive epsilon-connected ordinal set
x is set
phi . x is set
dom phi is epsilon-transitive epsilon-connected ordinal set
sup phi is epsilon-transitive epsilon-connected ordinal set
sup (rng phi) is epsilon-transitive epsilon-connected ordinal set
C is set
x is set
phi . x is set
C is epsilon-transitive epsilon-connected ordinal set
phi . C is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
phi . x is epsilon-transitive epsilon-connected ordinal set
M is epsilon-transitive epsilon-connected ordinal set
phi | x is Relation-like rng phi -valued Function-like T-Sequence-like Ordinal-yielding set
rng (phi | x) is set
sup (phi | x) is epsilon-transitive epsilon-connected ordinal set
sup (rng (phi | x)) is epsilon-transitive epsilon-connected ordinal set
nextcard (sup (phi | x)) is epsilon-transitive epsilon-connected ordinal cardinal set
dom (phi | x) is epsilon-transitive epsilon-connected ordinal set
n . (dom (phi | x)) is epsilon-transitive epsilon-connected ordinal set
nextcard (n . (dom (phi | x))) is epsilon-transitive epsilon-connected ordinal cardinal set
(nextcard (n . (dom (phi | x)))) \/ (nextcard (sup (phi | x))) is epsilon-transitive epsilon-connected ordinal set
C is set
x is epsilon-transitive epsilon-connected ordinal Element of F
M is epsilon-transitive epsilon-connected ordinal set
g1 is set
n . g1 is set
h1 is epsilon-transitive epsilon-connected ordinal set
phi | h1 is Relation-like rng phi -valued Function-like T-Sequence-like Ordinal-yielding set
dom (phi | h1) is epsilon-transitive epsilon-connected ordinal set
nextcard M is epsilon-transitive epsilon-connected ordinal cardinal set
phi . h1 is epsilon-transitive epsilon-connected ordinal set
sup (phi | h1) is epsilon-transitive epsilon-connected ordinal set
rng (phi | h1) is set
sup (rng (phi | h1)) is epsilon-transitive epsilon-connected ordinal set
nextcard (sup (phi | h1)) is epsilon-transitive epsilon-connected ordinal cardinal set
(nextcard M) \/ (nextcard (sup (phi | h1))) is epsilon-transitive epsilon-connected ordinal set
sup F is epsilon-transitive epsilon-connected ordinal set
C is set
phi . C is set
x is epsilon-transitive epsilon-connected ordinal set
phi | x is Relation-like rng phi -valued Function-like T-Sequence-like Ordinal-yielding set
dom (phi | x) is epsilon-transitive epsilon-connected ordinal set
phi . x is epsilon-transitive epsilon-connected ordinal set
n . x is epsilon-transitive epsilon-connected ordinal set
nextcard (n . x) is epsilon-transitive epsilon-connected ordinal cardinal set
sup (phi | x) is epsilon-transitive epsilon-connected ordinal set
rng (phi | x) is set
sup (rng (phi | x)) is epsilon-transitive epsilon-connected ordinal set
nextcard (sup (phi | x)) is epsilon-transitive epsilon-connected ordinal cardinal set
(nextcard (n . x)) \/ (nextcard (sup (phi | x))) is epsilon-transitive epsilon-connected ordinal set
C is set
phi . C is set
x is epsilon-transitive epsilon-connected ordinal set
phi | x is Relation-like rng phi -valued Function-like T-Sequence-like Ordinal-yielding set
dom (phi | x) is epsilon-transitive epsilon-connected ordinal set
n . x is epsilon-transitive epsilon-connected ordinal set
nextcard (n . x) is epsilon-transitive epsilon-connected ordinal cardinal set
sup (phi | x) is epsilon-transitive epsilon-connected ordinal set
rng (phi | x) is set
sup (rng (phi | x)) is epsilon-transitive epsilon-connected ordinal set
nextcard (sup (phi | x)) is epsilon-transitive epsilon-connected ordinal cardinal set
(nextcard (n . x)) \/ (nextcard (sup (phi | x))) is epsilon-transitive epsilon-connected ordinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
nextcard F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
((nextcard F)) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
exp (F,n) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
exp (2,n) is epsilon-transitive epsilon-connected ordinal cardinal set
bool F is non empty non trivial non finite set
card (bool F) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
card F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
exp (2,(card F)) is epsilon-transitive epsilon-connected ordinal cardinal set
exp (2,F) is epsilon-transitive epsilon-connected ordinal cardinal set
exp ((exp (2,F)),n) is epsilon-transitive epsilon-connected ordinal cardinal set
F *` n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
exp (2,(F *` n)) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
nextcard F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
exp ((nextcard F),n) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
exp (F,n) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
(exp (F,n)) *` (nextcard F) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
exp (2,n) is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like Function-like T-Sequence-like set
dom X is epsilon-transitive epsilon-connected ordinal set
((nextcard F)) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
Funcs (n,(nextcard F)) is non empty FUNCTION_DOMAIN of n, nextcard F
Union X is set
rng X is set
union (rng X) is set
phi is set
C is Relation-like Function-like set
dom C is set
rng C is set
x is Relation-like Function-like T-Sequence-like set
M is Relation-like Function-like T-Sequence-like Ordinal-yielding set
sup M is epsilon-transitive epsilon-connected ordinal set
rng M is set
sup (rng M) is epsilon-transitive epsilon-connected ordinal set
X . (sup M) is set
Funcs (n,(sup M)) is set
card (Funcs (n,(nextcard F))) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
card (Union X) is epsilon-transitive epsilon-connected ordinal cardinal set
Card X is Relation-like Function-like Cardinal-yielding set
Sum (Card X) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin (Card X) is Relation-like Function-like set
Union (disjoin (Card X)) is set
rng (disjoin (Card X)) is set
union (rng (disjoin (Card X))) is set
card (Union (disjoin (Card X))) is epsilon-transitive epsilon-connected ordinal cardinal set
(exp ((nextcard F),n)) *` (exp ((nextcard F),n)) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
exp ((nextcard F),1) is epsilon-transitive epsilon-connected ordinal cardinal set
phi is set
card phi is epsilon-transitive epsilon-connected ordinal cardinal set
card (card phi) is epsilon-transitive epsilon-connected ordinal cardinal set
card n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
C is epsilon-transitive epsilon-connected ordinal set
X . C is set
Funcs (n,C) is set
Funcs (n,(card phi)) is set
Funcs (n,F) is non empty FUNCTION_DOMAIN of n,F
card (Funcs (n,(card phi))) is epsilon-transitive epsilon-connected ordinal cardinal set
card (Funcs (n,F)) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
(nextcard F) --> (exp (F,n)) is Relation-like non-empty nextcard F -defined Function-like constant T-Sequence-like non empty non trivial V23( nextcard F) quasi_total Ordinal-yielding non finite Cardinal-yielding Element of bool [:(nextcard F),{(exp (F,n))}:]
{(exp (F,n))} is non empty trivial finite 1 -element countable set
[:(nextcard F),{(exp (F,n))}:] is non empty non trivial non finite set
bool [:(nextcard F),{(exp (F,n))}:] is non empty non trivial non finite set
((nextcard F) --> (exp (F,n))) . phi is set
(Card X) . phi is set
X . phi is set
card (X . phi) is epsilon-transitive epsilon-connected ordinal cardinal set
dom (Card X) is set
dom ((nextcard F) --> (exp (F,n))) is epsilon-transitive epsilon-connected ordinal non trivial set
Sum ((nextcard F) --> (exp (F,n))) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin ((nextcard F) --> (exp (F,n))) is Relation-like Function-like set
Union (disjoin ((nextcard F) --> (exp (F,n)))) is set
rng (disjoin ((nextcard F) --> (exp (F,n)))) is set
union (rng (disjoin ((nextcard F) --> (exp (F,n))))) is set
card (Union (disjoin ((nextcard F) --> (exp (F,n))))) is epsilon-transitive epsilon-connected ordinal cardinal set
(nextcard F) *` (exp (F,n)) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
(n,F) is Relation-like Function-like Cardinal-yielding set
Sum (n,F) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin (n,F) is Relation-like Function-like set
Union (disjoin (n,F)) is set
rng (disjoin (n,F)) is set
union (rng (disjoin (n,F))) is set
card (Union (disjoin (n,F))) is epsilon-transitive epsilon-connected ordinal cardinal set
exp (n,F) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } --> (exp (n,F)) is Relation-like non-empty { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } -defined Function-like constant V23( { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } ) quasi_total Ordinal-yielding Cardinal-yielding Element of bool [: { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } ,{(exp (n,F))}:]
{(exp (n,F))} is non empty trivial finite 1 -element countable set
[: { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } ,{(exp (n,F))}:] is set
bool [: { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } ,{(exp (n,F))}:] is set
C is set
x is epsilon-transitive epsilon-connected ordinal Element of n
n --> (exp (n,F)) is Relation-like non-empty n -defined Function-like constant T-Sequence-like non empty non trivial V23(n) quasi_total Ordinal-yielding non finite Cardinal-yielding Element of bool [:n,{(exp (n,F))}:]
[:n,{(exp (n,F))}:] is non empty non trivial non finite set
bool [:n,{(exp (n,F))}:] is non empty non trivial non finite set
Sum (n --> (exp (n,F))) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin (n --> (exp (n,F))) is Relation-like Function-like set
Union (disjoin (n --> (exp (n,F)))) is set
rng (disjoin (n --> (exp (n,F)))) is set
union (rng (disjoin (n --> (exp (n,F))))) is set
card (Union (disjoin (n --> (exp (n,F))))) is epsilon-transitive epsilon-connected ordinal cardinal set
n *` (exp (n,F)) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
Sum ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } --> (exp (n,F))) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } --> (exp (n,F))) is Relation-like Function-like set
Union (disjoin ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } --> (exp (n,F)))) is set
rng (disjoin ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } --> (exp (n,F)))) is set
union (rng (disjoin ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } --> (exp (n,F))))) is set
card (Union (disjoin ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } --> (exp (n,F))))) is epsilon-transitive epsilon-connected ordinal cardinal set
dom ( { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } --> (exp (n,F))) is set
dom (n,F) is set
C is set
C is set
x is epsilon-transitive epsilon-connected ordinal Element of n
exp (n,1) is epsilon-transitive epsilon-connected ordinal cardinal set
C is set
x is epsilon-transitive epsilon-connected ordinal Element of n
( { b1 where b1 is epsilon-transitive epsilon-connected ordinal Element of n : b1 is epsilon-transitive epsilon-connected ordinal cardinal set } --> (exp (n,F))) . C is set
(n,F) . C is set
M is epsilon-transitive epsilon-connected ordinal cardinal set
exp (M,F) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
(F) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
exp (F,n) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
(F,n) is Relation-like Function-like Cardinal-yielding set
Sum (F,n) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin (F,n) is Relation-like Function-like set
Union (disjoin (F,n)) is set
rng (disjoin (F,n)) is set
union (rng (disjoin (F,n))) is set
card (Union (disjoin (F,n))) is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like Function-like T-Sequence-like set
dom X is epsilon-transitive epsilon-connected ordinal set
Union (F,n) is set
rng (F,n) is set
union (rng (F,n)) is set
card (Union (F,n)) is epsilon-transitive epsilon-connected ordinal cardinal set
phi is set
C is epsilon-transitive epsilon-connected ordinal set
card C is epsilon-transitive epsilon-connected ordinal cardinal set
dom (F,n) is set
card phi is epsilon-transitive epsilon-connected ordinal cardinal set
(F,n) . (card phi) is set
Funcs (n,C) is set
card (Funcs (n,C)) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (n,(card C)) is set
card (Funcs (n,(card C))) is epsilon-transitive epsilon-connected ordinal cardinal set
X . phi is set
Card X is Relation-like Function-like Cardinal-yielding set
(Card X) . phi is set
card (X . phi) is epsilon-transitive epsilon-connected ordinal cardinal set
exp ((card C),n) is epsilon-transitive epsilon-connected ordinal cardinal set
exp ((card phi),n) is epsilon-transitive epsilon-connected ordinal cardinal set
card (exp ((card phi),n)) is epsilon-transitive epsilon-connected ordinal cardinal set
F --> (Sum (F,n)) is Relation-like F -defined Function-like constant T-Sequence-like non empty non trivial V23(F) quasi_total Ordinal-yielding non finite Cardinal-yielding Element of bool [:F,{(Sum (F,n))}:]
{(Sum (F,n))} is non empty trivial finite 1 -element countable set
[:F,{(Sum (F,n))}:] is non empty non trivial non finite set
bool [:F,{(Sum (F,n))}:] is non empty non trivial non finite set
(F --> (Sum (F,n))) . phi is set
dom (F --> (Sum (F,n))) is epsilon-transitive epsilon-connected ordinal non trivial set
dom (Card X) is set
Sum (Card X) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin (Card X) is Relation-like Function-like set
Union (disjoin (Card X)) is set
rng (disjoin (Card X)) is set
union (rng (disjoin (Card X))) is set
card (Union (disjoin (Card X))) is epsilon-transitive epsilon-connected ordinal cardinal set
Sum (F --> (Sum (F,n))) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin (F --> (Sum (F,n))) is Relation-like Function-like set
Union (disjoin (F --> (Sum (F,n)))) is set
rng (disjoin (F --> (Sum (F,n)))) is set
union (rng (disjoin (F --> (Sum (F,n))))) is set
card (Union (disjoin (F --> (Sum (F,n))))) is epsilon-transitive epsilon-connected ordinal cardinal set
phi is set
C is epsilon-transitive epsilon-connected ordinal set
card C is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard (card C) is epsilon-transitive epsilon-connected ordinal cardinal set
(F,n) . (nextcard (card C)) is set
exp ((nextcard (card C)),n) is epsilon-transitive epsilon-connected ordinal cardinal set
card (exp ((nextcard (card C)),n)) is epsilon-transitive epsilon-connected ordinal cardinal set
card phi is epsilon-transitive epsilon-connected ordinal cardinal set
card (card phi) is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard C is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard (card phi) is epsilon-transitive epsilon-connected ordinal cardinal set
nextcard phi is epsilon-transitive epsilon-connected ordinal cardinal set
F *` (Sum (F,n)) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (n,F) is non empty FUNCTION_DOMAIN of n,F
Union X is set
rng X is set
union (rng X) is set
phi is set
C is Relation-like Function-like set
dom C is set
rng C is set
x is Relation-like Function-like T-Sequence-like set
M is Relation-like Function-like T-Sequence-like Ordinal-yielding set
rng M is set
sup M is epsilon-transitive epsilon-connected ordinal set
sup (rng M) is epsilon-transitive epsilon-connected ordinal set
Funcs (n,(sup M)) is set
X . (sup M) is set
card (Funcs (n,F)) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
card (Union X) is epsilon-transitive epsilon-connected ordinal cardinal set
F is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
(F) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
n is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
exp (F,n) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
(F,n) is Relation-like Function-like Cardinal-yielding set
Sum (F,n) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin (F,n) is Relation-like Function-like set
Union (disjoin (F,n)) is set
rng (disjoin (F,n)) is set
union (rng (disjoin (F,n))) is set
card (Union (disjoin (F,n))) is epsilon-transitive epsilon-connected ordinal cardinal set
exp ((Sum (F,n)),(F)) is epsilon-transitive epsilon-connected ordinal cardinal set
X is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom X is epsilon-transitive epsilon-connected ordinal set
rng X is set
sup X is epsilon-transitive epsilon-connected ordinal set
sup (rng X) is epsilon-transitive epsilon-connected ordinal set
Funcs (n,F) is non empty FUNCTION_DOMAIN of n,F
phi is set
C is Relation-like Function-like set
dom C is set
rng C is set
x is set
X . x is set
M is Relation-like Function-like set
dom M is set
[M,(X . x)] is non natural V24() set
{M,(X . x)} is non empty finite countable set
{M} is functional non empty trivial finite 1 -element with_common_domain countable set
{{M,(X . x)},{M}} is non empty finite V43() countable set
g1 is set
C . g1 is set
M . g1 is set
x is Relation-like Function-like set
dom x is set
M is set
x . M is set
X . M is set
phi is Relation-like Function-like set
dom phi is set
dom (F,n) is set
C is Relation-like Function-like set
dom C is set
rng phi is set
disjoin C is Relation-like Function-like set
Union (disjoin C) is set
rng (disjoin C) is set
union (rng (disjoin C)) is set
Funcs ((F),(Union (disjoin C))) is set
x is set
M is set
phi . M is set
g1 is Relation-like Function-like set
h1 is Relation-like Function-like set
dom g1 is set
rng g1 is set
dom h1 is set
rng h1 is set
g2 is set
h2 is set
h1 . h2 is set
X . h2 is set
x1 is Relation-like Function-like set
[x1,(X . h2)] is non natural V24() set
{x1,(X . h2)} is non empty finite countable set
{x1} is functional non empty trivial finite 1 -element with_common_domain countable set
{{x1,(X . h2)},{x1}} is non empty finite V43() countable set
dom x1 is set
rng x1 is set
A1 is set
X is epsilon-transitive epsilon-connected ordinal set
X . X is epsilon-transitive epsilon-connected ordinal set
A is set
x1 . A is set
g1 . A is set
A2 is epsilon-transitive epsilon-connected ordinal set
Funcs (n,(X . h2)) is set
[x1,(X . h2)] `1 is set
[x1,(X . h2)] `2 is set
C . (X . h2) is set
card (Union (disjoin C)) is epsilon-transitive epsilon-connected ordinal cardinal set
card (card (Union (disjoin C))) is epsilon-transitive epsilon-connected ordinal cardinal set
card (F) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
card (Funcs ((F),(Union (disjoin C)))) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs ((F),(card (Union (disjoin C)))) is set
card (Funcs ((F),(card (Union (disjoin C))))) is epsilon-transitive epsilon-connected ordinal cardinal set
exp ((card (Union (disjoin C))),(F)) is epsilon-transitive epsilon-connected ordinal cardinal set
Card C is Relation-like Function-like Cardinal-yielding set
dom (Card C) is set
x is set
phi . x is set
M is set
phi . M is set
g1 is Relation-like Function-like set
h1 is Relation-like Function-like set
dom g1 is set
rng g1 is set
dom h1 is set
g2 is Relation-like Function-like set
h2 is Relation-like Function-like set
dom g2 is set
rng g2 is set
dom h2 is set
x1 is set
X is epsilon-transitive epsilon-connected ordinal Element of n
g1 . X is set
g2 . X is set
g1 . x1 is set
g2 . x1 is set
A1 is epsilon-transitive epsilon-connected ordinal Element of F
A2 is epsilon-transitive epsilon-connected ordinal Element of F
A1 \/ A2 is epsilon-transitive epsilon-connected ordinal set
succ (A1 \/ A2) is epsilon-transitive epsilon-connected ordinal non empty set
B is epsilon-transitive epsilon-connected ordinal set
x2 is set
X . x2 is set
h1 . x2 is set
f1 is Relation-like Function-like set
[f1,(X . x2)] is non natural V24() set
{f1,(X . x2)} is non empty finite countable set
{f1} is functional non empty trivial finite 1 -element with_common_domain countable set
{{f1,(X . x2)},{f1}} is non empty finite V43() countable set
dom f1 is set
f1 . X is set
h2 . x2 is set
f2 is Relation-like Function-like set
[f2,(X . x2)] is non natural V24() set
{f2,(X . x2)} is non empty finite countable set
{f2} is functional non empty trivial finite 1 -element with_common_domain countable set
{{f2,(X . x2)},{f2}} is non empty finite V43() countable set
dom f2 is set
dom (disjoin C) is set
x is set
(disjoin C) . x is set
C . x is set
{x} is non empty trivial finite 1 -element countable set
[:(C . x),{x}:] is set
(Card C) . x is set
card (C . x) is epsilon-transitive epsilon-connected ordinal cardinal set
Card (disjoin C) is Relation-like Function-like Cardinal-yielding set
(Card (disjoin C)) . x is set
card ((disjoin C) . x) is epsilon-transitive epsilon-connected ordinal cardinal set
x is set
M is epsilon-transitive epsilon-connected ordinal cardinal set
(F,n) . M is set
exp (M,n) is epsilon-transitive epsilon-connected ordinal cardinal set
(Card C) . x is set
C . x is set
card (C . x) is epsilon-transitive epsilon-connected ordinal cardinal set
Funcs (n,x) is set
(F,n) . x is set
dom (Card (disjoin C)) is set
card (Funcs (n,F)) is epsilon-transitive epsilon-connected ordinal non empty cardinal set
exp ((exp (F,n)),(F)) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
n *` (F) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
exp (F,(n *` (F))) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set
F is epsilon-transitive epsilon-connected ordinal set
n is finite countable set
RelIncl n is Relation-like finite countable set
order_type_of (RelIncl n) is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of (RelIncl n)) is Relation-like well_founded set
F is epsilon-transitive epsilon-connected ordinal set
n is finite countable set
RelIncl n is Relation-like finite countable set
order_type_of (RelIncl n) is epsilon-transitive epsilon-connected ordinal set
card n is epsilon-transitive epsilon-connected ordinal natural V35() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
card (order_type_of (RelIncl n)) is epsilon-transitive epsilon-connected ordinal cardinal set
X is epsilon-transitive epsilon-connected ordinal natural V37() finite cardinal countable set
F is set
{F} is non empty trivial finite 1 -element countable set
RelIncl {F} is Relation-like non empty finite countable set
order_type_of (RelIncl {F}) is epsilon-transitive epsilon-connected ordinal set
n is epsilon-transitive epsilon-connected ordinal set
card {F} is epsilon-transitive epsilon-connected ordinal natural non empty V35() V37() V38() finite cardinal countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V69() Element of NAT
F is set
{F} is non empty trivial finite 1 -element countable set
RelIncl {F} is Relation-like non empty finite countable set
order_type_of (RelIncl {F}) is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of (RelIncl {F})) is Relation-like well_founded set
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl {F}))),(RelIncl {F})) is Relation-like Function-like set
0 .--> F is Relation-like NAT -defined {0} -defined Function-like one-to-one finite countable set
{0} is non empty trivial finite V43() 1 -element countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
n is epsilon-transitive epsilon-connected ordinal set
RelIncl {0} is Relation-like non empty finite countable set
[0,0] is non natural V24() set
{0,0} is non empty finite V43() countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
{{0,0},{0}} is non empty finite V43() countable set
{[0,0]} is Function-like non empty trivial finite 1 -element countable set
canonical_isomorphism_of ((RelIncl {0}),(RelIncl {F})) is Relation-like Function-like set
rng (canonical_isomorphism_of ((RelIncl {0}),(RelIncl {F}))) is set
field (RelIncl {F}) is finite countable set
dom (canonical_isomorphism_of ((RelIncl {0}),(RelIncl {F}))) is set
field (RelIncl {0}) is finite countable set
F is epsilon-transitive epsilon-connected ordinal set
bool F is set
n is Element of bool F
RelIncl n is Relation-like set
order_type_of (RelIncl n) is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of (RelIncl n)) is Relation-like well_founded set
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl n))),(RelIncl n)) is Relation-like Function-like set
X is set
(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl n))),(RelIncl n))) . X is set
phi is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom phi is epsilon-transitive epsilon-connected ordinal set
rng phi is set
phi . X is set
F is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered set
RelIncl F is Relation-like set
order_type_of (RelIncl F) is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of (RelIncl F)) is Relation-like well_founded set
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl F))),(RelIncl F)) is Relation-like Function-like set
n is set
(canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl F))),(RelIncl F))) . n is set
X is set
X is countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
RelIncl X is Relation-like set
order_type_of (RelIncl X) is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of (RelIncl X)) is Relation-like well_founded set
canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl X))),(RelIncl X)) is Relation-like Function-like set
phi is Relation-like Function-like T-Sequence-like Ordinal-yielding set
dom phi is epsilon-transitive epsilon-connected ordinal set
rng phi is set
phi . n is set
F is countable complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
card F is epsilon-transitive epsilon-connected ordinal cardinal set
RelIncl F is Relation-like set
order_type_of (RelIncl F) is epsilon-transitive epsilon-connected ordinal set
card (order_type_of (RelIncl F)) is epsilon-transitive epsilon-connected ordinal cardinal set