:: CARD_1 semantic presentation

f is set

f is set

f is set

dom y1 is set
rng y1 is set
field (x |_2 f) is set
dom (x |_2 f) is set
rng (x |_2 f) is set
(dom (x |_2 f)) \/ (rng (x |_2 f)) is set
field () is set
dom () is set
rng () is set
(dom ()) \/ (rng ()) is set

f is set

f is set

f is set

f is non empty set

dom x is set
rng x is set
f is set

x is set

field f is set
dom f is set
rng f is set
(dom f) \/ (rng f) is set

dom x is set
rng x is set
field () is set
dom () is set
rng () is set
(dom ()) \/ (rng ()) is set
f is set

field () is set
dom () is set
rng () is set
(dom ()) \/ (rng ()) is set

f is set

f is set

x is set

dom f is set
rng f is set

dom y is set
rng y is set

dom y1 is set
rng y1 is set
dom (y ") is set
rng (y ") is set

dom f is set
rng f is set

dom y is set
rng y is set

rng (f * y) is set
dom (f * y) is set
((rng (f * y))) is epsilon-transitive epsilon-connected ordinal () set
f is set

x is set

dom (id f) is set
rng (id f) is set

dom f is set
rng f is set
f is set

x is set

dom f is set
rng f is set

y is set
(f ") . y is set
y1 is set
y2 is set
y is set
y1 is set
(f ") . y is set
y2 is set

dom y is set
rng y is set
y1 is set
f . y1 is set
(f ") . (f . y1) is set
y . (f . y1) is set

dom f is set
rng f is set

dom y is set
rng y is set
y1 is non empty set
y2 is set
h is set
y . h is set
{h} is non empty trivial finite set
f " {h} is set
x is set
f . x is set

dom y2 is set

dom (y * y2) is set
h is set
(y * y2) . h is set
x is set
(y * y2) . x is set
y . x is set
{x} is non empty trivial finite set
f " {x} is set
y2 . (f " {x}) is set
f . (y2 . (f " {x})) is set
y . h is set
{h} is non empty trivial finite set
f " {h} is set
y2 . (f " {h}) is set
f . (y2 . (f " {h})) is set
y2 . (y . h) is set
y2 . (y . x) is set
rng (y * y2) is set
h is set
x is set
(y * y2) . x is set
y . x is set
y2 . (y . x) is set
{x} is non empty trivial finite set
f " {x} is set
f is set
bool f is non empty set

dom x is set
rng x is set
f is set
y is set
y is set
x . y is set
y1 is set
f is set

bool f is non empty set
((bool f)) is epsilon-transitive epsilon-connected ordinal non empty () set

dom x is set
rng x is set
f is set
y is set
x . y is set
{y} is non empty trivial finite set
y1 is set
f is set
x . f is set
y is set
x . y is set
{f} is non empty trivial finite set
{y} is non empty trivial finite set
f is set

bool f is non empty set
((bool f)) is epsilon-transitive epsilon-connected ordinal non empty () set

f is set

f is set

x is set

f is set

x is set

{f} is non empty trivial finite set
f \/ {f} is non empty set

x is set

(f) is set

{f} is non empty trivial finite set
f \/ {f} is non empty set
y is set

last y1 is set

{f} is non empty trivial finite set
f \/ {f} is non empty set
y1 . {} is set
(f) is set
({}) is set

(f) is set

(f) is set

{x} is non empty trivial finite set
x \/ {x} is non empty set
(x) is set
{(x)} is non empty trivial finite set
union {(x)} is set
((union {(x)})) is epsilon-transitive epsilon-connected ordinal () set

{x} is non empty trivial finite set
x \/ {x} is non empty set

{f} is non empty trivial finite set
f \/ {f} is non empty set

{(f)} is non empty trivial finite set
union {(f)} is set
((union {(f)})) is epsilon-transitive epsilon-connected ordinal () set

{f} is non empty trivial finite set
f \/ {f} is non empty set

{y} is non empty trivial finite set
y \/ {y} is non empty set
y1 . (succ y) is set
rng y1 is set

(((succ y))) is epsilon-transitive epsilon-connected ordinal () set

((sup y1)) is epsilon-transitive epsilon-connected ordinal () set

f is set
x is set
f is set

f is set
bool f is non empty set

x is set

((bool f)) is epsilon-transitive epsilon-connected ordinal non empty () set
f is set

dom x is set
rng x is set

f is set
x is set
{x} is non empty trivial finite set

dom f is set
rng f is set
f . x is set
{(f . x)} is non empty trivial finite set
f is set
{f} is non empty trivial finite set
[:f,{x}:] is set
bool [:f,{x}:] is non empty set
f --> x is Relation-like f -defined Function-like constant V23(f) V27(f,{x}) Element of bool [:f,{x}:]
y is Relation-like f -defined Function-like constant V23(f) V27(f,{x}) Element of bool [:f,{x}:]
dom y is set

y1 is set
y . y1 is set
y2 is set
y . y2 is set
y1 is set
y . f is set
f is set

x is set
{x} is non empty trivial finite set

f is set
{f} is non empty trivial finite set

f is set
{f} is non empty trivial finite set

is non empty trivial finite V39() set
{} \/ is non empty finite V39() set

y is set
{y} is non empty trivial finite set

f is set
x is set
f \/ x is set
f is set
y is set
f \/ y is set
f /\ x is set
f /\ y is set

dom y1 is set
rng y1 is set

dom y2 is set
rng y2 is set
h is set
y1 . h is set
y2 . h is set
h is set
x is set
y1 . h is set
y2 . h is set
y is set

dom h is set
rng h is set
x is set
h . x is set
y is set
h . y is set
y1 . y is set
y2 . y is set
y1 . x is set
y2 . x is set
x is set
y is set
h . y is set
y1 . y is set
y2 . y is set
x is set
y is set
y2 . y is set
h . y is set
y1 . y is set
y is set
y1 . y is set
h . y is set
y2 . y is set
f is set
{f} is non empty trivial finite set
x is set
x \ {f} is Element of bool x
bool x is non empty set
f is set
{f} is non empty trivial finite set
x \ {f} is Element of bool x
y is set
y1 is set
y2 is set
y is set
y1 is set
y2 is set

dom y is set
rng y is set
y1 is set
y . y1 is set
y2 is set
y . y2 is set
y1 is set
y2 is set
y . y2 is set
y1 is set
y . y1 is set
y . f is set
f is set

dom x is set
x .: f is set

dom f is set
rng f is set
f is set
x is set
f is set
{f} is non empty trivial finite set
f \ {f} is Element of bool f
bool f is non empty set
y is set
{y} is non empty trivial finite set
x \ {y} is Element of bool x
bool x is non empty set

dom y1 is set
rng y1 is set
y1 .: (f \ {f}) is set
y1 . f is set
{(y1 . f)} is non empty trivial finite set
x \ {(y1 . f)} is Element of bool x
y1 .: f is set
Im (y1,f) is set
y1 .: {f} is finite set
(y1 .: f) \ (Im (y1,f)) is Element of bool (y1 .: f)
bool (y1 .: f) is non empty set
x \ (Im (y1,f)) is Element of bool x
f is set
succ f is non empty set
{f} is non empty trivial finite set
f \/ {f} is non empty set
x is set
succ x is non empty set
{x} is non empty trivial finite set
x \/ {x} is non empty set
(succ f) \ {f} is Element of bool (succ f)
bool (succ f) is non empty set
(succ x) \ {x} is Element of bool (succ x)
bool (succ x) is non empty set

{f} is non empty trivial finite set
f \/ {f} is non empty set

{x} is non empty trivial finite set
x \/ {x} is non empty set

{f} is non empty trivial finite set
f \/ {f} is non empty set

{y1} is non empty trivial finite set
y1 \/ {y1} is non empty set

f is set

f is set
f is set
x is set

dom f is set
rng f is set

rng y is set
dom y is set

rng (y * f) is set
dom (y * f) is set

rng (id x) is set
dom (id x) is set

f is set
x is set
{x} is non empty trivial finite set
f is set
f \/ {x} is non empty set

f /\ {x} is finite set
the Element of f /\ {x} is Element of f /\ {x}
{y} is non empty trivial finite set
y1 is set

y \/ {y} is non empty set

{f} is non empty trivial finite set
f \/ {f} is non empty set
((succ f)) is epsilon-transitive epsilon-connected ordinal non empty () set

{f} is non empty trivial finite set
f \/ {f} is non empty set
f is finite set

f is set

x is finite set

{(x)} is non empty trivial finite set
(x) \/ {(x)} is non empty set
(((x))) is epsilon-transitive epsilon-connected ordinal non empty () set

f is set

{f} is non empty trivial finite set
f \/ {f} is non empty set
((f)) is epsilon-transitive epsilon-connected ordinal non empty () set
f is set

{f} is non empty trivial finite set
f \/ {f} is non empty set

{x} is non empty trivial finite set
x \/ {x} is non empty set
((x)) is epsilon-transitive epsilon-connected ordinal non empty () set

f is finite set

{f} is non empty trivial finite set
f \/ {f} is non empty set

(f) \ {f} is finite Element of bool (f)
bool (f) is non empty finite V39() set

{y1} is non empty trivial finite set
y1 \/ {y1} is non empty set
y \ {y1} is Element of bool y
bool y is non empty set

f is non empty non trivial non finite set

is non empty trivial finite V39() set

{} \/ is non empty finite V39() set

{{},1} is non empty finite V39() set

{1} is non empty trivial finite V39() set
1 \/ {1} is non empty finite set

{{},1,2} is non empty finite set

{2} is non empty trivial finite V39() set
2 \/ {2} is non empty finite set

{{},1,2,3} is non empty finite set

{3} is non empty trivial finite V39() set
3 \/ {3} is non empty finite set

{{},1,2,3,4} is non empty finite set

{4} is non empty trivial finite V39() set
4 \/ {4} is non empty finite set

{{},1,2,3,4,5} is non empty finite set

{5} is non empty trivial finite V39() set
5 \/ {5} is non empty finite set

{{},1,2,3,4,5,6} is non empty finite set

{6} is non empty trivial finite V39() set
6 \/ {6} is non empty finite set

{{},1,2,3,4,5,6,7} is non empty finite set

{7} is non empty trivial finite V39() set
7 \/ {7} is non empty finite set

{{},1,2,3,4,5,6,7,8} is non empty set

{8} is non empty trivial finite V39() set
8 \/ {8} is non empty finite set

{{},1,2,3,4,5,6,7,8,9} is non empty set

{9} is non empty trivial finite V39() set
9 \/ {9} is non empty finite set

dom f is set
rng f is set

(f) is set
bool omega is non empty set

f is set
f is non empty non trivial non finite set
bool f is non empty set
x is set
union x is set
f is set
y is set
{f} is non empty trivial finite set
f is set
y is set
{y} is non empty trivial finite set
f is set
x is non empty set
[:f,x:] is non empty set

dom f is set
rng f is set
y is set
y1 is set
f . y1 is set
y1 `1 is set
the Element of x is Element of x
[y, the Element of x] is non empty V24() set
{y, the Element of x} is non empty finite set
{y} is non empty trivial finite set
{{y, the Element of x},{y}} is non empty finite V39() set
f . [y, the Element of x] is set
[y, the Element of x] `1 is set
f .: [:f,x:] is set
[:x,f:] is non empty set

dom f is set
rng f is set
y is set
y1 is set
f . y1 is set
y1 `2 is set
the Element of x is Element of x
[ the Element of x,y] is non empty V24() set
{ the Element of x,y} is non empty finite set
{ the Element of x} is non empty trivial finite set
{{ the Element of x,y},{ the Element of x}} is non empty finite V39() set
[ the Element of x,y] `2 is set
f . [ the Element of x,y] is set
f .: [:x,f:] is set
f is non empty non trivial non finite set
bool f is non empty non trivial non finite set
f is set

dom f is set

dom x is set
rng x is set
f is set
x . f is set
y is set
x . y is set
f . f is set
[f,(f . f)] is non empty V24() set
{f,(f . f)} is non empty finite set
{f} is non empty trivial finite set
{{f,(f . f)},{f}} is non empty finite V39() set
f . y is set
[y,(f . y)] is non empty V24() set
{y,(f . y)} is non empty finite set
{y} is non empty trivial finite set
{{y,(f . y)},{y}} is non empty finite V39() set
f is set
y is set
x . y is set
f . y is set
[y,(f . y)] is non empty V24() set
{y,(f . y)} is non empty finite set
{y} is non empty trivial finite set
{{y,(f . y)},{y}} is non empty finite V39() set
f is set
y is set
[f,y] is non empty V24() set
{f,y} is non empty finite set
{f} is non empty trivial finite set
{{f,y},{f}} is non empty finite V39() set
f . f is set
x . f is set
f is finite set

[:f,f:] is finite set
f is set

dom f is finite set
rng f is finite set
(dom f) \/ (rng f) is finite set
f is set

{f} is non empty trivial finite set
[:x,{f}:] is finite set
bool [:x,{f}:] is non empty finite V39() set

dom (x --> f) is finite set

f is set

f is set

f is set
{f} is non empty trivial finite set

{} \/ is non empty finite V39() set

is non empty trivial finite V39() (1) set
is set
bool is non empty set

dom x is set

dom x is set

f is set

x is set
{x} is non empty trivial finite (1) set
f is set
x is set
{x} is non empty trivial finite (1) set
f is non empty set
bool f is non empty set
the non empty trivial finite (1) Element of bool f is non empty trivial finite (1) Element of bool f
f is non empty set
bool f is non empty set
x is non empty trivial finite (1) Element of bool f
f is set
{f} is non empty trivial finite (1) set
y is Element of f
{y} is non empty trivial finite (1) set
f is set

x is set

dom f is set
rng f is set
f .: x is set

f .: x is set
dom f is set

dom y is set
rng y is set
y1 is set
y2 is set
f . y2 is set
y . y2 is set

f is set
x .: f is set
((x .: f)) is epsilon-transitive epsilon-connected ordinal () set

f is set

x is set

x \ f is Element of bool x
bool x is non empty set
f is set

x is set
{x} is non empty trivial finite (1) set
[:f,{x}:] is set

dom f is set
rng f is set
y is set
f . y is set
y1 is set
f . y1 is set
[y,x] is non empty V24() set
{y,x} is non empty finite set
{y} is non empty trivial finite (1) set
{{y,x},{y}} is non empty finite V39() set
[y,x] `1 is set
[y1,x] is non empty V24() set
{y1,x} is non empty finite set
{y1} is non empty trivial finite (1) set
{{y1,x},{y1}} is non empty finite V39() set
y is set
y1 is set
f . y1 is set
[y1,x] is non empty V24() set
{y1,x} is non empty finite set
{y1} is non empty trivial finite (1) set
{{y1,x},{y1}} is non empty finite V39() set
y is set
y1 is set
y2 is set
[y1,y2] is non empty V24() set
{y1,y2} is non empty finite set
{y1} is non empty trivial finite (1) set
{{y1,y2},{y1}} is non empty finite V39() set
f . y1 is set

dom f is set

rng f is set

f .: (dom f) is set