:: CARD_5 semantic presentation

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

{ b

card { b

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

{ b

{ b

{(exp (n,F))} is non empty trivial finite 1 -element countable set

[: { b

bool [: { b

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 ( { b

disjoin ( { b

Union (disjoin ( { b

rng (disjoin ( { b

union (rng (disjoin ( { b

card (Union (disjoin ( { b

dom ( { b

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

( { b

(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