:: CARD_5 semantic presentation

bool NAT is non trivial non finite set
bool NAT is non trivial non finite set

F is set

F is 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

X is set
phi is set

dom phi is set
C is set
rng phi is set
x is set
phi . x is set

g1 is set

phi . (alef h1) is set

g1 is set
phi . g1 is set

phi . (alef (succ h1)) is set

rng x is set

M is set

g2 is set
x . g2 is set

x1 is set
phi . x1 is set

phi . (card (sup x)) is set

Union F is set
rng F is set
union (rng F) is set
On (rng F) is set

n is set

field (RelIncl ()) is set
dom (canonical_isomorphism_of ((RelIncl ()),())) is set
field () is set
rng (canonical_isomorphism_of ((RelIncl ()),())) is set

rng M is 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,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

n is set

rng X is set

On n is set

n is set

field () is set
rng (canonical_isomorphism_of ((RelIncl ()),())) is set
field (RelIncl ()) is set
dom (canonical_isomorphism_of ((RelIncl ()),())) is set

dom X is set
rng X is set

x is set

h1 is set

field (RelIncl ()) is set
dom (canonical_isomorphism_of ((RelIncl ()),())) is set
field () is set
rng (canonical_isomorphism_of ((RelIncl ()),())) is set

dom (h2 * C) is set
rng (h2 * C) is set

rng X is set

rng C is 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

A1 is set

A2 is set
C . A2 is set

rng C is set

rng (C | B) is set
union (rng (C | B)) is set
x2 is set
h2 . x2 is set

X . x2 is set

rng C is set

rng (C | B) is set
union (rng (C | B)) is set

x2 is set
(C | B) . x2 is set

rng (C | f2) is set
union (rng (C | f2)) is set

z is set
(C | f2) . z is set

z is set
h2 . z is set

rng C is set

rng (C | B) is set
union (rng (C | B)) is set

rng F is set

rng n is set

phi is set
n . phi is set

x is set
F . x is set

rng F is set

rng n is set

X is set
X is set
X is set
F . X is set
n . X is set

n is set
F . n is set
X is set
F . X is set

rng (F ^ n) is 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

{ 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

dom phi is set
rng phi is set
C is set
phi .: C is set
RelIncl (phi .: C) is Relation-like 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

rng g1 is 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

(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

h2 is Element of bool F

(order_type_of (RelIncl (phi .: C))) +^ (n -^ (order_type_of (RelIncl (phi .: C)))) 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

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,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

rng h1 is set
rng (h1 | g1) is set
g2 is set
h2 is set
h1 . h2 is set

g2 is Element of bool F

x is set
C . x is set
M is set
C . M is set
phi .: M is 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

rng h1 is set
rng (h1 | g1) is set
phi .: x is 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

rng h2 is set
rng (h2 | g2) is set
x1 is set
phi . x1 is set
X is Element of bool F

X is set
phi . X is set
A1 is Element of bool F

x1 is set
phi . x1 is set
X is Element of bool F

X is set
phi . X is set
A1 is Element of bool F

[:n,(card (Funcs (n,(card F)))):] is set

n *` (card (Funcs (n,(card F)))) is epsilon-transitive epsilon-connected ordinal cardinal set

bool F is set

F is set

X is set

dom phi is set
C is set
x is set

phi . C is set

dom X is set

dom phi is set
C is set

X . C is set

phi . C is set

phi is set
X is set
phi is set
X is set
C is set

rng X is set

phi is finite countable set
C is set

rng n is set

union (rng n) is set

Union (disjoin (Card n)) is set
rng (disjoin (Card n)) is set
union (rng (disjoin (Card n))) is set

{F} is non empty trivial finite 1 -element countable set
[:(()),{F}:] is set
bool [:(()),{F}:] is set

disjoin ((()) --> F) is Relation-like Function-like set
Union (disjoin ((()) --> F)) is set
rng (disjoin ((()) --> F)) is set
union (rng (disjoin ((()) --> F))) is set

X is set
n . X is set

(Card n) . X is set
((()) --> F) . X is set
dom (Card n) is set

On (rng n) is set

F is set

union F is set

C is set

x is set
M is set

rng X is set

union (rng X) is set

rng n is set

rng X is set

phi is set
C is set
X . C is set

rng (X | x) is set

(nextcard (n . x)) \/ (nextcard (sup (X | x))) is epsilon-transitive epsilon-connected ordinal set

rng phi is set

rng (phi | C) is set
sup (rng (phi | C)) is epsilon-transitive epsilon-connected ordinal 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

(phi | C) .: C is set

rng phi is set
C is set

x is set
phi . x is set

C is set
x is set
phi . x is set

rng (phi | x) is set

sup (rng (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

g1 is set
n . g1 is 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 set

C is set
phi . C is set

rng (phi | x) is set
sup (rng (phi | x)) is epsilon-transitive epsilon-connected ordinal set

(nextcard (n . x)) \/ (nextcard (sup (phi | x))) is epsilon-transitive epsilon-connected ordinal set
C is set
phi . C is set

rng (phi | x) is set
sup (rng (phi | x)) is epsilon-transitive epsilon-connected ordinal set

(nextcard (n . x)) \/ (nextcard (sup (phi | x))) is epsilon-transitive epsilon-connected ordinal set

bool F is non empty non trivial non finite set

exp ((exp (2,F)),n) is epsilon-transitive epsilon-connected ordinal cardinal set

Funcs (n,()) 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

dom C is set
rng C is set

rng M is set

X . (sup M) is set
Funcs (n,(sup M)) is set

Union (disjoin (Card X)) is set
rng (disjoin (Card X)) is set
union (rng (disjoin (Card X))) is set

(exp ((),n)) *` (exp ((),n)) is epsilon-transitive epsilon-connected ordinal limit_ordinal non empty non trivial non finite cardinal set

phi is 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

{(exp (F,n))} is non empty trivial finite 1 -element countable set
[:(),{(exp (F,n))}:] is non empty non trivial non finite set
bool [:(),{(exp (F,n))}:] is non empty non trivial non finite set
(() --> (exp (F,n))) . phi is set
(Card X) . phi is set
X . phi is set

dom (Card X) is set
dom (() --> (exp (F,n))) is epsilon-transitive epsilon-connected ordinal non trivial set
Sum (() --> (exp (F,n))) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin (() --> (exp (F,n))) is Relation-like Function-like set
Union (disjoin (() --> (exp (F,n)))) is set
rng (disjoin (() --> (exp (F,n)))) is set
union (rng (disjoin (() --> (exp (F,n))))) is set
card (Union (disjoin (() --> (exp (F,n))))) is epsilon-transitive epsilon-connected ordinal cardinal set

Union (disjoin (n,F)) is set
rng (disjoin (n,F)) is set
union (rng (disjoin (n,F))) is set

{ } is set
{ } --> (exp (n,F)) is Relation-like non-empty { } -defined Function-like constant V23( { } ) quasi_total Ordinal-yielding Cardinal-yielding Element of bool [: { } ,{(exp (n,F))}:]
{(exp (n,F))} is non empty trivial finite 1 -element countable set
[: { } ,{(exp (n,F))}:] is set
bool [: { } ,{(exp (n,F))}:] is set
C is set

[: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

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

Sum ( { } --> (exp (n,F))) is epsilon-transitive epsilon-connected ordinal cardinal set
disjoin ( { } --> (exp (n,F))) is Relation-like Function-like set
Union (disjoin ( { } --> (exp (n,F)))) is set
rng (disjoin ( { } --> (exp (n,F)))) is set
union (rng (disjoin ( { } --> (exp (n,F))))) is set
card (Union (disjoin ( { } --> (exp (n,F))))) is epsilon-transitive epsilon-connected ordinal cardinal set
dom ( { } --> (exp (n,F))) is set
dom (n,F) is set
C is set
C is set

C is set

( { } --> (exp (n,F))) . C is set
(n,F) . C is set

Union (disjoin (F,n)) is set
rng (disjoin (F,n)) is set
union (rng (disjoin (F,n))) is set

Union (F,n) is set
rng (F,n) is set
union (rng (F,n)) is set

phi is set

dom (F,n) is set

(F,n) . (card phi) is set
Funcs (n,C) is set

Funcs (n,(card C)) is set

X . phi is set

(Card X) . phi is set

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

Union (disjoin (Card X)) is set
rng (disjoin (Card X)) is set
union (rng (disjoin (Card X))) is 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

(F,n) . (nextcard (card C)) is 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

dom C is set
rng C is set

rng M is set

Funcs (n,(sup M)) is set
X . (sup M) is set

Union (disjoin (F,n)) is set
rng (disjoin (F,n)) is set
union (rng (disjoin (F,n))) is set

exp ((Sum (F,n)),(F)) is epsilon-transitive epsilon-connected ordinal cardinal set

rng X is set

Funcs (n,F) is non empty FUNCTION_DOMAIN of n,F
phi is set

dom C is set
rng C is set
x is set
X . x is set

dom M is set
[M,(X . x)] is non natural V24() set
{M,(X . x)} is non empty finite countable set

{{M,(X . x)},{M}} is non empty finite V43() countable set
g1 is set
C . g1 is set
M . g1 is set

dom x is set
M is set
x . M is set
X . M is set

dom phi is set
dom (F,n) is set

dom C is set
rng phi is set

Union () is set
rng () is set
union (rng ()) is set
Funcs ((F),(Union ())) is set
x is set
M is set
phi . M is 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,(X . h2)] is non natural V24() set
{x1,(X . h2)} is non empty finite countable set

{{x1,(X . h2)},{x1}} is non empty finite V43() countable set
dom x1 is set
rng x1 is set
A1 is set

A is set
x1 . A is set
g1 . A is set

Funcs (n,(X . h2)) is set
[x1,(X . h2)] `1 is set
[x1,(X . h2)] `2 is set
C . (X . h2) is set

Funcs ((F),(card (Union ()))) is set
card (Funcs ((F),(card (Union ())))) is epsilon-transitive epsilon-connected ordinal cardinal set
exp ((card (Union ())),(F)) is epsilon-transitive epsilon-connected ordinal cardinal set

dom (Card C) is set
x is set
phi . x is set
M is set
phi . M is set

dom g1 is set
rng g1 is set
dom h1 is set

dom g2 is set
rng g2 is set
dom h2 is set
x1 is set

g1 . X is set
g2 . X is set
g1 . x1 is set
g2 . x1 is set

x2 is set
X . x2 is set
h1 . x2 is set

[f1,(X . x2)] is non natural V24() set
{f1,(X . x2)} is non empty finite 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,(X . x2)] is non natural V24() set
{f2,(X . x2)} is non empty finite countable set

{{f2,(X . x2)},{f2}} is non empty finite V43() countable set
dom f2 is set
dom () is set
x is set
() . 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 ()) . x is set

x is set

(F,n) . M is set

(Card C) . x is set
C . x is set

Funcs (n,x) is set
(F,n) . x is set
dom (Card ()) is set

exp ((exp (F,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 set
{F} is non empty trivial finite 1 -element countable set

F is set
{F} is non empty trivial finite 1 -element countable set

[0,0] is non natural V24() set

is non empty finite V43() countable set

rng () is set

dom () is set

bool F is set
n is Element of bool F

X is set
(canonical_isomorphism_of ((RelIncl ()),())) . X is set

rng phi is set
phi . X is set

n is set
(canonical_isomorphism_of ((RelIncl ()),())) . n is set
X is set

rng phi is set
phi . n is set