:: FRAENKEL semantic presentation

{} is set

the Relation-like non-empty empty-yielding empty finite finite-yielding V28() set is Relation-like non-empty empty-yielding empty finite finite-yielding V28() set

F

{ F

{ F

M is set

f is Element of F

F

F

F

{ F

{ F

M is set

f is Element of F

x is Element of F

F

F

{ F

{ F

x is Element of F

x is Element of F

F

F

{ F

{ F

x is Element of F

y is Element of F

x is Element of F

y is Element of F

F

{ F

{ F

x is set

y is Element of F

F

F

x is set

y is Element of F

F

F

F

{ F

{ F

x is set

y is Element of F

F

F

x is set

y is Element of F

F

F

F

F

{ F

{ F

x is set

y is Element of F

x is Element of F

F

F

x is set

y is Element of F

x is Element of F

F

F

F

F

{ F

{ F

M is Element of F

f is Element of F

{ F

M is Element of F

f is Element of F

M is Element of F

f is Element of F

F

F

{ H

M is set

f is set

[:M,f:] is Relation-like set

bool [:M,f:] is non empty cup-closed diff-closed preBoolean set

x is Relation-like M -defined f -valued Function-like quasi_total Element of bool [:M,f:]

y is Relation-like M -defined f -valued Function-like quasi_total Element of bool [:M,f:]

x is set

x | x is Relation-like M -defined x -defined M -defined f -valued Function-like Element of bool [:M,f:]

y | x is Relation-like M -defined x -defined M -defined f -valued Function-like Element of bool [:M,f:]

Choice is Element of M

x . Choice is set

y . Choice is set

(y | x) . Choice is set

M is set

f is set

Funcs (M,f) is set

[:M,f:] is Relation-like set

bool [:M,f:] is non empty cup-closed diff-closed preBoolean set

x is set

y is Relation-like Function-like set

proj1 y is set

proj2 y is set

[:(proj1 y),(proj2 y):] is Relation-like set

M is non empty set

f is set

[:f,M:] is Relation-like set

bool [:f,M:] is non empty cup-closed diff-closed preBoolean set

x is set

y is set

Funcs (x,y) is set

x is Element of Funcs (x,y)

Choice is Relation-like Function-like set

proj1 Choice is set

proj2 Choice is set

F

F

[:F

bool [:F

F

F

F

F

F

{ (F

{ (F

{ H

f is Element of F

x is Element of F

{ H

f is Element of F

F

F

{ H

F

{ b

bool F

F

F

{ F

M is Element of F

f is Element of F

F

F

F

{ F

M is set

f is Element of F

x is Element of F

F

F

F

F

{ F

{ b

{ F

M is set

f is Element of F

x is Element of F

y is Element of F

F

M is set

f is Element of F

x is Element of F

F

F

{ b

{ F

{ F

M is Element of F

f is Element of F

{ F

{ F

F

F

{ b

{ F

{ F

M is Element of F

f is Element of F

x is Element of F

{ F

{ F

F

F

{ F

{ F

M is set

f is Element of F

x is Element of F

F

y is Element of F

F

F

F

{ F

M is set

f is Element of F

F

F

F

{ F

M is set

f is Element of F

F

F

F

F

{ F

{ F

M is set

f is Element of F

x is Element of F

F

M is set

f is Element of F

F

F

F

F

{ F

{ F

f is Element of F

M is Element of F

y is Element of F

x is Element of F

{ F

M is non empty set

f is set

Funcs (f,M) is non empty FUNCTION_DOMAIN of f,M

x is set

y is set

Funcs (x,y) is set

x is Element of Funcs (x,y)

[:f,M:] is Relation-like set

bool [:f,M:] is non empty cup-closed diff-closed preBoolean set

Choice is Relation-like f -defined M -valued Function-like Element of bool [:f,M:]

dom Choice is Element of bool f

bool f is non empty cup-closed diff-closed preBoolean set

f is Relation-like f -defined M -valued Function-like quasi_total Element of bool [:f,M:]

t is Relation-like f -defined M -valued Function-like quasi_total Element of Funcs (f,M)

t | x is Relation-like f -defined x -defined f -defined M -valued Function-like Element of bool [:f,M:]

f /\ x is set

dom t is Element of bool f

(dom t) /\ x is Element of bool f

x is Relation-like Function-like set

proj1 x is set

proj2 x is set

M is non empty set

f is set

x is set

Funcs (x,M) is non empty FUNCTION_DOMAIN of x,M

x /\ f is set

y is Relation-like x -defined M -valued Function-like quasi_total Element of Funcs (x,M)

y | f is Relation-like f -defined x -defined M -valued Function-like Element of bool [:x,M:]

[:x,M:] is Relation-like set

bool [:x,M:] is non empty cup-closed diff-closed preBoolean set

y | (x /\ f) is Relation-like x -defined x /\ f -defined x -defined M -valued Function-like Element of bool [:x,M:]

dom y is Element of bool x

bool x is non empty cup-closed diff-closed preBoolean set

dom (y | f) is Element of bool f

bool f is non empty cup-closed diff-closed preBoolean set

(dom y) /\ x is Element of bool x

((dom y) /\ x) /\ f is Element of bool x

(dom y) /\ (x /\ f) is Element of bool x

x is set

(y | f) . x is set

y . x is set

F

F

{ F

F

{F

f is set

x is Element of F

F

F

f is Relation-like Function-like set

proj1 f is set

f .: F

x is set

y is Element of F

F

f . y is set

x is set

y is set

f . y is set

x is Element of F

F

F

F

F

F

{ F

F

F

[:(F

f is Relation-like Function-like set

proj1 f is set

[:F

[:F

[:F

f .: [:F

x is set

y is Element of F

x is Element of F

F

[y,x] is V15() Element of [:F

{y,x} is finite set

{y} is finite set

{{y,x},{y}} is finite V28() set

[y,x] `2 is Element of F

[y,x] `1 is Element of F

f . (y,x) is set

[y,x] is V15() set

f . [y,x] is set

x is set

y is set

f . y is set

x is Element of [:F

x `1 is Element of F

x `2 is Element of F

[(x `1),(x `2)] is V15() Element of [:F

{(x `1),(x `2)} is finite set

{(x `1)} is finite set

{{(x `1),(x `2)},{(x `1)}} is finite V28() set

F

F

Fin F

F

M is finite Element of Fin F

f is Element of F

{.f.} is finite Element of Fin F

M \/ {.f.} is finite Element of Fin F

x is Element of F

{f} is finite Element of bool F

bool F

M \/ {f} is finite set

y is Element of F

x is Element of F

x is Element of F

y is Element of F

y is Element of F

x is Element of F

Choice is Element of F

f is Element of F

y is Element of F

y is Element of F

y is Element of F

x is Element of F

y is Element of F

{}. F

M is Element of F

M is Element of F

F

Fin F

F

Fin F

F

{ F

{ b

x is set

y is Element of F

x is Element of F

F

x is finite Element of Fin F

y is Element of F

x is Element of F

F

Choice is Element of F

f is Element of F

F

M is finite set

f is finite set

Funcs (M,f) is set

[:M,f:] is Relation-like finite set

bool [:M,f:] is non empty finite V28() cup-closed diff-closed preBoolean set

M is set

f is set

Funcs (M,f) is set

F

F

F

F

Funcs (F

{ F

the Element of { F

F

x is Relation-like F

F

x .: F

bool F

dom x is Element of bool F

bool F

F

Funcs ((F

y is non empty set

Choice is Element of y

f is Relation-like F

f | (F

[:F

bool [:F

f | F

rng (f | F

t is Relation-like Function-like set

proj1 t is set

proj2 t is set

f .: F

F

x is non empty set

t is Element of x

x is Element of x

c

c

F

[:y,x:] is Relation-like non empty set

bool [:y,x:] is non empty cup-closed diff-closed preBoolean set

Choice is Relation-like y -defined x -valued Function-like quasi_total Element of bool [:y,x:]

Choice .: (Funcs ((F

bool x is non empty cup-closed diff-closed preBoolean set

f is set

t is Relation-like F

F

t .: F

t | F

rng (t | F

dom (t | F

dom t is Element of bool F

(dom t) /\ F

x is Element of Funcs ((F

dom Choice is Element of bool y

bool y is non empty cup-closed diff-closed preBoolean set

Choice . x is set

F

F

Fin F

F

[:F

bool [:F

the Element of F

{ { b

the Relation-like F

y is Element of F

the Relation-like F

{ b

Choice is set

x is non empty set

f is Element of F

{ b

t is Element of F

Choice is Relation-like Function-like set

proj1 Choice is set

{ b

Choice . { b

f is Element of F

{ b

Choice . { b

x is Element of F

f is Relation-like F

t is Element of F

{ b

f . t is Element of F

Choice . { b

x is Element of F

F

F

Fin F

F

Funcs (F

M is Element of F

[:F

bool [:F

M is Relation-like F

f is Relation-like F

x is Element of F

f . x is Element of F

F

F

F

{ b

( P

f is set

x is set

f is set

x is set

y is set

[:F

bool [:F

f is Relation-like F

dom f is Element of bool F

bool F

f .: F

bool F

x is set

y is Element of F

x is Element of F

x is Element of F

f . x is set

x is set

y is set

f . y is set

x is Element of F