:: 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₁() is set
{ F₂(b₁) where b₁ is Element of F₁() : P₁[b₁] } is set
{ F₂(b₁) where b₁ is Element of F₁() : P₂[b₁] } is set
M is set
f is Element of F₁()
F₂(f) is set
F₁() is set
F₂() is set
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₁[b₁,b₂] } is set
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₂[b₁,b₂] } is set
M is set
f is Element of F₁()
x is Element of F₂()
F₃(f,x) is set
F₁() is set
{ F₂(b₁) where b₁ is Element of F₁() : P₁[b₁] } is set
{ F₂(b₁) where b₁ is Element of F₁() : P₂[b₁] } is set
x is Element of F₁()
x is Element of F₁()
F₁() is set
F₂() is set
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₁[b₁,b₂] } is set
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₂[b₁,b₂] } is set
x is Element of F₁()
y is Element of F₂()
x is Element of F₁()
y is Element of F₂()
F₁() is set
{ F₂(b₁) where b₁ is Element of F₁() : P₁[b₁] } is set
{ F₃(b₁) where b₁ is Element of F₁() : P₁[b₁] } is set
x is set
y is Element of F₁()
F₃(y) is set
F₂(y) is set
x is set
y is Element of F₁()
F₂(y) is set
F₃(y) is set
F₁() is set
{ F₂(b₁) where b₁ is Element of F₁() : P₁[b₁] } is set
{ F₃(b₁) where b₁ is Element of F₁() : P₁[b₁] } is set
x is set
y is Element of F₁()
F₃(y) is set
F₂(y) is set
x is set
y is Element of F₁()
F₂(y) is set
F₃(y) is set
F₁() is set
F₂() is set
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₁[b₁,b₂] } is set
{ F₄(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₁[b₁,b₂] } is set
x is set
y is Element of F₁()
x is Element of F₂()
F₄(y,x) is set
F₃(y,x) is set
x is set
y is Element of F₁()
x is Element of F₂()
F₃(y,x) is set
F₄(y,x) is set
F₁() is set
F₂() is set
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₁[b₁,b₂] } is set
{ F₃(b₂,b₁) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₂[b₁,b₂] } is set
M is Element of F₁()
f is Element of F₂()
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₂[b₁,b₂] } is set
M is Element of F₁()
f is Element of F₂()
M is Element of F₁()
f is Element of F₂()
F₃(M,f) is set
F₃(f,M) is set
{ H₁(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₂[b₁,b₂] } is set
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₁() is set
F₂() is set
[:F₁(),F₂():] is Relation-like set
bool [:F₁(),F₂():] is non empty cup-closed diff-closed preBoolean set
F₄() is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of bool [:F₁(),F₂():]
F₃() is set
F₄() | F₃() is Relation-like F₁() -defined F₃() -defined F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
F₅() is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of bool [:F₁(),F₂():]
F₅() | F₃() is Relation-like F₁() -defined F₃() -defined F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
{ (F₄() . b₁) where b₁ is Element of F₁() : ( P₁[b₁] & b₁ in F₃() ) } is set
{ (F₅() . b₁) where b₁ is Element of F₁() : ( P₂[b₁] & b₁ in F₃() ) } is set
{ H₂(b₁) where b₁ is Element of F₁() : S₁[b₁] } is set
f is Element of F₁()
x is Element of F₁()
{ H₂(b₁) where b₁ is Element of F₁() : S₂[b₁] } is set
f is Element of F₁()
F₄() . f is set
F₅() . f is set
{ H₁(b₁) where b₁ is Element of F₁() : S₁[b₁] } is set
F₁() is non empty set
{ b₁ where b₁ is Element of F₁() : P₁[b₁] } is set
bool F₁() is non empty cup-closed diff-closed preBoolean set
F₁() is set
F₂() is set
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₁[b₁,b₂] } is set
M is Element of F₁()
f is Element of F₂()
F₃(M,f) is set
F₁() is set
F₂() is set
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₁[b₁,b₂] } is set
M is set
f is Element of F₁()
x is Element of F₂()
F₃(f,x) is set
F₃() is set
F₁() is set
F₂() is set
{ F₄(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₁[b₁,b₂] } is set
{ b₁ where b₁ is Element of F₃() : ( b₁ in { F₄(b₁,b₂) where b₂ is Element of F₁(), b₃ is Element of F₂() : P₁[b₁,b₂] } & P₂[b₁] ) } is set
{ F₄(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : ( P₁[b₁,b₂] & P₂[F₄(b₁,b₂)] ) } is set
M is set
f is Element of F₃()
x is Element of F₁()
y is Element of F₂()
F₄(x,y) is Element of F₃()
M is set
f is Element of F₁()
x is Element of F₂()
F₄(f,x) is Element of F₃()
F₁() is set
{ b₁ where b₁ is Element of F₁() : P₂[b₁] } is set
{ F₂(b₁) where b₁ is Element of F₁() : ( b₁ in { b₁ where b₂ is Element of F₁() : P₂[b₁] } & P₁[b₁] ) } is set
{ F₂(b₁) where b₁ is Element of F₁() : ( P₂[b₁] & P₁[b₁] ) } is set
M is Element of F₁()
f is Element of F₁()
{ F₂(b₁) where b₁ is Element of F₁() : S₂[b₁] } is set
{ F₂(b₁) where b₁ is Element of F₁() : S₁[b₁] } is set
F₁() is set
F₂() is set
{ b₁ where b₁ is Element of F₁() : P₂[b₁] } is set
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : ( b₁ in { b₁ where b₃ is Element of F₁() : P₂[b₁] } & P₁[b₁,b₂] ) } is set
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : ( P₂[b₁] & P₁[b₁,b₂] ) } is set
M is Element of F₁()
f is Element of F₂()
x is Element of F₁()
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : S₂[b₁,b₂] } is set
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : S₁[b₁,b₂] } is set
F₁() is set
F₂() is set
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₁[b₁,b₂] } is set
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₂[b₁,b₂] } is set
M is set
f is Element of F₁()
x is Element of F₂()
F₃(f,x) is set
y is Element of F₁()
F₃(y,x) is set
F₁() is set
F₂() is set
{ F₃(b₁) where b₁ is Element of F₁() : ( F₃(b₁) in F₂() & P₁[b₁] ) } is set
M is set
f is Element of F₁()
F₃(f) is set
F₁() is set
F₂() is set
{ F₃(b₁) where b₁ is Element of F₁() : ( P₁[b₁] & not F₃(b₁) in F₂() ) } is set
M is set
f is Element of F₁()
F₃(f) is set
F₂() is set
F₁() is set
F₄() is Element of F₂()
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : P₂[b₁,b₂] } is set
{ F₃(b₁,F₄()) where b₁ is Element of F₁() : P₁[b₁,F₄()] } is set
M is set
f is Element of F₁()
x is Element of F₂()
F₃(f,x) is set
M is set
f is Element of F₁()
F₃(f,F₄()) is set
F₂() is set
F₁() is set
F₄() is Element of F₂()
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : ( b₂ = F₄() & P₁[b₁,b₂] ) } is set
{ F₃(b₁,F₄()) where b₁ is Element of F₁() : P₁[b₁,F₄()] } is set
f is Element of F₂()
M is Element of F₁()
y is Element of F₂()
x is Element of F₁()
{ F₃(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : S₁[b₁,b₂] } is set
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₂() is set
F₁() is set
{ F₃(b₁) where b₁ is Element of F₁() : b₁ in F₂() } is set
F₃({}) is set
{F₃({})} is finite set
f is set
x is Element of F₁()
F₃(x) is set
F₂() /\ F₁() is set
f is Relation-like Function-like set
proj1 f is set
f .: F₂() is set
x is set
y is Element of F₁()
F₃(y) is set
f . y is set
x is set
y is set
f . y is set
x is Element of F₁()
F₃(x) is set
F₃() is set
F₄() is set
F₁() is non empty set
F₂() is non empty set
{ F₅(b₁,b₂) where b₁ is Element of F₁(), b₂ is Element of F₂() : ( b₁ in F₃() & b₂ in F₄() ) } is set
F₃() /\ F₁() is set
F₄() /\ F₂() is set
[:(F₃() /\ F₁()),(F₄() /\ F₂()):] is Relation-like set
f is Relation-like Function-like set
proj1 f is set
[:F₃(),F₄():] is Relation-like set
[:F₁(),F₂():] is Relation-like non empty set
[:F₃(),F₄():] /\ [:F₁(),F₂():] is Relation-like set
f .: [:F₃(),F₄():] is set
x is set
y is Element of F₁()
x is Element of F₂()
F₅(y,x) is set
[y,x] is V15() Element of [:F₁(),F₂():]
{y,x} is finite set
{y} is finite set
{{y,x},{y}} is finite V28() set
[y,x] `2 is Element of F<sub>2</sub>()
[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₁(),F₂():]
x `1 is Element of F<sub>1</sub>()
x `2 is Element of F₂()
[(x `1),(x `2)] is V15() Element of [:F₁(),F₂():]
{(x `1),(x `2)} is finite set
{(x `1)} is finite set
{{(x `1),(x `2)},{(x `1)}} is finite V28() set
F₅((x `1),(x `2)) is set
F₁() is non empty set
Fin F₁() is non empty cup-closed diff-closed preBoolean set
F₂() is finite Element of Fin 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₁() is non empty cup-closed diff-closed preBoolean set
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₁() is Relation-like non-empty empty-yielding empty finite finite-yielding V28() Element of Fin F₁()
M is Element of F₁()
M is Element of F₁()
F₂() is non empty set
Fin F₂() is non empty cup-closed diff-closed preBoolean set
F₁() is non empty set
Fin F₁() is non empty cup-closed diff-closed preBoolean set
F₃() is finite Element of Fin F₂()
{ F₄(b₁) where b₁ is Element of F₂() : b₁ in F₃() } is set
{ b₁ where b₁ is Element of F₁() : S₁[b₁] } is set
x is set
y is Element of F₁()
x is Element of F₂()
F₄(x) is Element of F₁()
x is finite Element of Fin F₁()
y is Element of F₁()
x is Element of F₂()
F₄(x) is Element of F₁()
Choice is Element of F₁()
f is Element of F₂()
F₄(f) is Element of 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₃() is set
F₄() is set
F₁() is set
F₂() is non empty set
Funcs (F₁(),F₂()) is non empty FUNCTION_DOMAIN of F₁(),F₂()
{ F₅(b₁) where b₁ is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of Funcs (F₁(),F₂()) : b₁ .: F₃() c= F₄() } is set
the Element of { F₅(b₁) where b₁ is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of Funcs (F₁(),F₂()) : b₁ .: F₃() c= F₄() } is Element of { F₅(b₁) where b₁ is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of Funcs (F₁(),F₂()) : b₁ .: F₃() c= F₄() }
F₂() /\ F₄() is set
x is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of Funcs (F₁(),F₂())
F₅(x) is set
x .: F₃() is Element of bool F₂()
bool F₂() is non empty cup-closed diff-closed preBoolean set
dom x is Element of bool F₁()
bool F₁() is non empty cup-closed diff-closed preBoolean set
F₁() /\ F₃() is set
Funcs ((F₁() /\ F₃()),(F₂() /\ F₄())) is set
y is non empty set
Choice is Element of y
f is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of Funcs (F₁(),F₂())
f | (F₁() /\ F₃()) is Relation-like F₁() -defined F₁() /\ F₃() -defined F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
[:F₁(),F₂():] is Relation-like set
bool [:F₁(),F₂():] is non empty cup-closed diff-closed preBoolean set
f | F₃() is Relation-like F₃() -defined F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
rng (f | F₃()) is Element of bool F₂()
t is Relation-like Function-like set
proj1 t is set
proj2 t is set
f .: F₃() is Element of bool F₂()
F₅(f) is set
x is non empty set
t is Element of x
x is Element of x
c₁₀ is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of Funcs (F₁(),F₂())
c₁₀ | F₃() is Relation-like F₃() -defined F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
F₅(c₁₀) is set
[: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₁() /\ F₃()),(F₂() /\ F₄()))) is Element of bool x
bool x is non empty cup-closed diff-closed preBoolean set
f is set
t is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of Funcs (F₁(),F₂())
F₅(t) is set
t .: F₃() is Element of bool F₂()
t | F₃() is Relation-like F₃() -defined F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
rng (t | F₃()) is Element of bool F₂()
dom (t | F₃()) is Element of bool F₁()
dom t is Element of bool F₁()
(dom t) /\ F₃() is Element of bool F₁()
x is Element of Funcs ((F₁() /\ F₃()),(F₂() /\ F₄()))
dom Choice is Element of bool y
bool y is non empty cup-closed diff-closed preBoolean set
Choice . x is set
F₁() is non empty set
F₂() is non empty set
Fin F₁() is non empty cup-closed diff-closed preBoolean set
F₃() is finite Element of Fin F₁()
[:F₁(),F₂():] is Relation-like non empty set
bool [:F₁(),F₂():] is non empty cup-closed diff-closed preBoolean set
the Element of F₂() is Element of F₂()
{ { b₂ where b₂ is Element of F₂() : P₁[b₁,b₂] } where b₁ is Element of F₁() : b₁ in F₃() } is set
the Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of bool [:F₁(),F₂():] is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of bool [:F₁(),F₂():]
y is Element of F₁()
the Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of bool [:F₁(),F₂():] . y is Element of F₂()
{ b₁ where b₁ is Element of F₂() : P₁[y,b₁] } is set
Choice is set
x is non empty set
f is Element of F₁()
{ b₁ where b₁ is Element of F₂() : P₁[f,b₁] } is set
t is Element of F₂()
Choice is Relation-like Function-like set
proj1 Choice is set
{ b₁ where b₁ is Element of F₂() : P₁[a₁,b₁] } is set
Choice . { b₁ where b₁ is Element of F₂() : P₁[a₁,b₁] } is set
f is Element of F₁()
{ b₁ where b₁ is Element of F₂() : P₁[f,b₁] } is set
Choice . { b₁ where b₁ is Element of F₂() : P₁[f,b₁] } is set
x is Element of F₂()
f is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of bool [:F₁(),F₂():]
t is Element of F₁()
{ b₁ where b₁ is Element of F₂() : P₁[t,b₁] } is set
f . t is Element of F₂()
Choice . { b₁ where b₁ is Element of F₂() : P₁[t,b₁] } is set
x is Element of F₂()
F₁() is non empty set
F₂() is non empty set
Fin F₁() is non empty cup-closed diff-closed preBoolean set
F₃() is finite Element of Fin F₁()
Funcs (F₁(),F₂()) is non empty FUNCTION_DOMAIN of F₁(),F₂()
M is Element of F₁()
[:F₁(),F₂():] is Relation-like non empty set
bool [:F₁(),F₂():] is non empty cup-closed diff-closed preBoolean set
M is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of bool [:F₁(),F₂():]
f is Relation-like F₁() -defined F₂() -valued Function-like quasi_total Element of Funcs (F₁(),F₂())
x is Element of F₁()
f . x is Element of F₂()
F₃() is set
F₁() is non empty set
F₂() is non empty set
{ b₁ where b₁ is Element of F₂() : ex b₂ being Element of F₁() st
( P₁[b₂,b₁] & b₂ in F₃() ) } is set
f is set
x is set
f is set
x is set
y is set
[:F₁(),F₂():] is Relation-like non empty set
bool [:F₁(),F₂():] is non empty cup-closed diff-closed preBoolean set
f is Relation-like F₁() -defined F₂() -valued Function-like Element of bool [:F₁(),F₂():]
dom f is Element of bool F₁()
bool F₁() is non empty cup-closed diff-closed preBoolean set
f .: F₃() is Element of bool F₂()
bool F₂() is non empty cup-closed diff-closed preBoolean set
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₂()