:: FRAENKEL semantic presentation

{} is set

F1() is set
{ F2(b1) where b1 is Element of F1() : P1[b1] } is set
{ F2(b1) where b1 is Element of F1() : P2[b1] } is set
M is set
f is Element of F1()
F2(f) is set
F1() is set
F2() is set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P1[b1,b2] } is set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P2[b1,b2] } is set
M is set
f is Element of F1()
x is Element of F2()
F3(f,x) is set
F1() is set
{ F2(b1) where b1 is Element of F1() : P1[b1] } is set
{ F2(b1) where b1 is Element of F1() : P2[b1] } is set
x is Element of F1()
x is Element of F1()
F1() is set
F2() is set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P1[b1,b2] } is set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P2[b1,b2] } is set
x is Element of F1()
y is Element of F2()
x is Element of F1()
y is Element of F2()
F1() is set
{ F2(b1) where b1 is Element of F1() : P1[b1] } is set
{ F3(b1) where b1 is Element of F1() : P1[b1] } is set
x is set
y is Element of F1()
F3(y) is set
F2(y) is set
x is set
y is Element of F1()
F2(y) is set
F3(y) is set
F1() is set
{ F2(b1) where b1 is Element of F1() : P1[b1] } is set
{ F3(b1) where b1 is Element of F1() : P1[b1] } is set
x is set
y is Element of F1()
F3(y) is set
F2(y) is set
x is set
y is Element of F1()
F2(y) is set
F3(y) is set
F1() is set
F2() is set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P1[b1,b2] } is set
{ F4(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P1[b1,b2] } is set
x is set
y is Element of F1()
x is Element of F2()
F4(y,x) is set
F3(y,x) is set
x is set
y is Element of F1()
x is Element of F2()
F3(y,x) is set
F4(y,x) is set
F1() is set
F2() is set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P1[b1,b2] } is set
{ F3(b2,b1) where b1 is Element of F1(), b2 is Element of F2() : P2[b1,b2] } is set
M is Element of F1()
f is Element of F2()
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P2[b1,b2] } is set
M is Element of F1()
f is Element of F2()
M is Element of F1()
f is Element of F2()
F3(M,f) is set
F3(f,M) is set
{ H1(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P2[b1,b2] } is set
M is set
f is set
[:M,f:] is Relation-like set

x is set

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

x is set

proj1 y is set
proj2 y is set
[:(),():] is Relation-like set
M is non empty set
f is set
[:f,M:] is Relation-like 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
F1() is set
F2() is set
[:F1(),F2():] is Relation-like set
bool [:F1(),F2():] is non empty cup-closed diff-closed preBoolean set
F4() is Relation-like F1() -defined F2() -valued Function-like quasi_total Element of bool [:F1(),F2():]
F3() is set
F4() | F3() is Relation-like F1() -defined F3() -defined F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
F5() is Relation-like F1() -defined F2() -valued Function-like quasi_total Element of bool [:F1(),F2():]
F5() | F3() is Relation-like F1() -defined F3() -defined F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
{ (F4() . b1) where b1 is Element of F1() : ( P1[b1] & b1 in F3() ) } is set
{ (F5() . b1) where b1 is Element of F1() : ( P2[b1] & b1 in F3() ) } is set
{ H2(b1) where b1 is Element of F1() : S1[b1] } is set
f is Element of F1()
x is Element of F1()
{ H2(b1) where b1 is Element of F1() : S2[b1] } is set
f is Element of F1()
F4() . f is set
F5() . f is set
{ H1(b1) where b1 is Element of F1() : S1[b1] } is set
F1() is non empty set
{ b1 where b1 is Element of F1() : P1[b1] } is set
bool F1() is non empty cup-closed diff-closed preBoolean set
F1() is set
F2() is set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P1[b1,b2] } is set
M is Element of F1()
f is Element of F2()
F3(M,f) is set
F1() is set
F2() is set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P1[b1,b2] } is set
M is set
f is Element of F1()
x is Element of F2()
F3(f,x) is set
F3() is set
F1() is set
F2() is set
{ F4(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P1[b1,b2] } is set
{ b1 where b1 is Element of F3() : ( b1 in { F4(b1,b2) where b2 is Element of F1(), b3 is Element of F2() : P1[b1,b2] } & P2[b1] ) } is set
{ F4(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : ( P1[b1,b2] & P2[F4(b1,b2)] ) } is set
M is set
f is Element of F3()
x is Element of F1()
y is Element of F2()
F4(x,y) is Element of F3()
M is set
f is Element of F1()
x is Element of F2()
F4(f,x) is Element of F3()
F1() is set
{ b1 where b1 is Element of F1() : P2[b1] } is set
{ F2(b1) where b1 is Element of F1() : ( b1 in { b1 where b2 is Element of F1() : P2[b1] } & P1[b1] ) } is set
{ F2(b1) where b1 is Element of F1() : ( P2[b1] & P1[b1] ) } is set
M is Element of F1()
f is Element of F1()
{ F2(b1) where b1 is Element of F1() : S2[b1] } is set
{ F2(b1) where b1 is Element of F1() : S1[b1] } is set
F1() is set
F2() is set
{ b1 where b1 is Element of F1() : P2[b1] } is set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : ( b1 in { b1 where b3 is Element of F1() : P2[b1] } & P1[b1,b2] ) } is set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : ( P2[b1] & P1[b1,b2] ) } is set
M is Element of F1()
f is Element of F2()
x is Element of F1()
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : S2[b1,b2] } is set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : S1[b1,b2] } is set
F1() is set
F2() is set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P1[b1,b2] } is set
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P2[b1,b2] } is set
M is set
f is Element of F1()
x is Element of F2()
F3(f,x) is set
y is Element of F1()
F3(y,x) is set
F1() is set
F2() is set
{ F3(b1) where b1 is Element of F1() : ( F3(b1) in F2() & P1[b1] ) } is set
M is set
f is Element of F1()
F3(f) is set
F1() is set
F2() is set
{ F3(b1) where b1 is Element of F1() : ( P1[b1] & not F3(b1) in F2() ) } is set
M is set
f is Element of F1()
F3(f) is set
F2() is set
F1() is set
F4() is Element of F2()
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : P2[b1,b2] } is set
{ F3(b1,F4()) where b1 is Element of F1() : P1[b1,F4()] } is set
M is set
f is Element of F1()
x is Element of F2()
F3(f,x) is set
M is set
f is Element of F1()
F3(f,F4()) is set
F2() is set
F1() is set
F4() is Element of F2()
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : ( b2 = F4() & P1[b1,b2] ) } is set
{ F3(b1,F4()) where b1 is Element of F1() : P1[b1,F4()] } is set
f is Element of F2()
M is Element of F1()
y is Element of F2()
x is Element of F1()
{ F3(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : S1[b1,b2] } 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

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

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

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

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

dom y is Element of bool x

dom (y | f) is Element of bool f

(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
F2() is set
F1() is set
{ F3(b1) where b1 is Element of F1() : b1 in F2() } is set
F3({}) is set
{F3({})} is finite set
f is set
x is Element of F1()
F3(x) is set
F2() /\ F1() is set

proj1 f is set
f .: F2() is set
x is set
y is Element of F1()
F3(y) is set
f . y is set
x is set
y is set
f . y is set
x is Element of F1()
F3(x) is set
F3() is set
F4() is set
F1() is non empty set
F2() is non empty set
{ F5(b1,b2) where b1 is Element of F1(), b2 is Element of F2() : ( b1 in F3() & b2 in F4() ) } is set
F3() /\ F1() is set
F4() /\ F2() is set
[:(F3() /\ F1()),(F4() /\ F2()):] is Relation-like set

proj1 f is set
[:F3(),F4():] is Relation-like set
[:F1(),F2():] is Relation-like non empty set
[:F3(),F4():] /\ [:F1(),F2():] is Relation-like set
f .: [:F3(),F4():] is set
x is set
y is Element of F1()
x is Element of F2()
F5(y,x) is set
[y,x] is V15() Element of [:F1(),F2():]
{y,x} is finite set
{y} is finite set
{{y,x},{y}} is finite V28() set
[y,x] `2 is Element of F2()
[y,x] `1 is Element of F1()
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 [:F1(),F2():]
x `1 is Element of F1()
x `2 is Element of F2()
[(x `1),(x `2)] is V15() Element of [:F1(),F2():]
{(x `1),(x `2)} is finite set
{(x `1)} is finite set
{{(x `1),(x `2)},{(x `1)}} is finite V28() set
F5((x `1),(x `2)) is set
F1() is non empty set
Fin F1() is non empty cup-closed diff-closed preBoolean set
F2() is finite Element of Fin F1()
M is finite Element of Fin F1()
f is Element of F1()
{.f.} is finite Element of Fin F1()
M \/ {.f.} is finite Element of Fin F1()
x is Element of F1()
{f} is finite Element of bool F1()
bool F1() is non empty cup-closed diff-closed preBoolean set
M \/ {f} is finite set
y is Element of F1()
x is Element of F1()
x is Element of F1()
y is Element of F1()
y is Element of F1()
x is Element of F1()
Choice is Element of F1()
f is Element of F1()
y is Element of F1()
y is Element of F1()
y is Element of F1()
x is Element of F1()
y is Element of F1()

M is Element of F1()
M is Element of F1()
F2() is non empty set
Fin F2() is non empty cup-closed diff-closed preBoolean set
F1() is non empty set
Fin F1() is non empty cup-closed diff-closed preBoolean set
F3() is finite Element of Fin F2()
{ F4(b1) where b1 is Element of F2() : b1 in F3() } is set
{ b1 where b1 is Element of F1() : S1[b1] } is set
x is set
y is Element of F1()
x is Element of F2()
F4(x) is Element of F1()
x is finite Element of Fin F1()
y is Element of F1()
x is Element of F2()
F4(x) is Element of F1()
Choice is Element of F1()
f is Element of F2()
F4(f) is Element of F1()
M is finite set
f is finite set
Funcs (M,f) is set

M is set
f is set
Funcs (M,f) is set
F3() is set
F4() is set
F1() is set
F2() is non empty set
Funcs (F1(),F2()) is non empty FUNCTION_DOMAIN of F1(),F2()
{ F5(b1) where b1 is Relation-like F1() -defined F2() -valued Function-like quasi_total Element of Funcs (F1(),F2()) : b1 .: F3() c= F4() } is set
the Element of { F5(b1) where b1 is Relation-like F1() -defined F2() -valued Function-like quasi_total Element of Funcs (F1(),F2()) : b1 .: F3() c= F4() } is Element of { F5(b1) where b1 is Relation-like F1() -defined F2() -valued Function-like quasi_total Element of Funcs (F1(),F2()) : b1 .: F3() c= F4() }
F2() /\ F4() is set
x is Relation-like F1() -defined F2() -valued Function-like quasi_total Element of Funcs (F1(),F2())
F5(x) is set
x .: F3() is Element of bool F2()
bool F2() is non empty cup-closed diff-closed preBoolean set
dom x is Element of bool F1()
bool F1() is non empty cup-closed diff-closed preBoolean set
F1() /\ F3() is set
Funcs ((F1() /\ F3()),(F2() /\ F4())) is set
y is non empty set
Choice is Element of y
f is Relation-like F1() -defined F2() -valued Function-like quasi_total Element of Funcs (F1(),F2())
f | (F1() /\ F3()) is Relation-like F1() -defined F1() /\ F3() -defined F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
[:F1(),F2():] is Relation-like set
bool [:F1(),F2():] is non empty cup-closed diff-closed preBoolean set
f | F3() is Relation-like F3() -defined F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
rng (f | F3()) is Element of bool F2()

proj1 t is set
proj2 t is set
f .: F3() is Element of bool F2()
F5(f) is set
x is non empty set
t is Element of x
x is Element of x
c10 is Relation-like F1() -defined F2() -valued Function-like quasi_total Element of Funcs (F1(),F2())
c10 | F3() is Relation-like F3() -defined F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
F5(c10) is set
[:y,x:] is Relation-like non empty set

Choice .: (Funcs ((F1() /\ F3()),(F2() /\ F4()))) is Element of bool x

f is set
t is Relation-like F1() -defined F2() -valued Function-like quasi_total Element of Funcs (F1(),F2())
F5(t) is set
t .: F3() is Element of bool F2()
t | F3() is Relation-like F3() -defined F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
rng (t | F3()) is Element of bool F2()
dom (t | F3()) is Element of bool F1()
dom t is Element of bool F1()
(dom t) /\ F3() is Element of bool F1()
x is Element of Funcs ((F1() /\ F3()),(F2() /\ F4()))
dom Choice is Element of bool y

Choice . x is set
F1() is non empty set
F2() is non empty set
Fin F1() is non empty cup-closed diff-closed preBoolean set
F3() is finite Element of Fin F1()
[:F1(),F2():] is Relation-like non empty set
bool [:F1(),F2():] is non empty cup-closed diff-closed preBoolean set
the Element of F2() is Element of F2()
{ { b2 where b2 is Element of F2() : P1[b1,b2] } where b1 is Element of F1() : b1 in F3() } is set
the Relation-like F1() -defined F2() -valued Function-like quasi_total Element of bool [:F1(),F2():] is Relation-like F1() -defined F2() -valued Function-like quasi_total Element of bool [:F1(),F2():]
y is Element of F1()
the Relation-like F1() -defined F2() -valued Function-like quasi_total Element of bool [:F1(),F2():] . y is Element of F2()
{ b1 where b1 is Element of F2() : P1[y,b1] } is set
Choice is set
x is non empty set
f is Element of F1()
{ b1 where b1 is Element of F2() : P1[f,b1] } is set
t is Element of F2()
Choice is Relation-like Function-like set
proj1 Choice is set
{ b1 where b1 is Element of F2() : P1[a1,b1] } is set
Choice . { b1 where b1 is Element of F2() : P1[a1,b1] } is set
f is Element of F1()
{ b1 where b1 is Element of F2() : P1[f,b1] } is set
Choice . { b1 where b1 is Element of F2() : P1[f,b1] } is set
x is Element of F2()
f is Relation-like F1() -defined F2() -valued Function-like quasi_total Element of bool [:F1(),F2():]
t is Element of F1()
{ b1 where b1 is Element of F2() : P1[t,b1] } is set
f . t is Element of F2()
Choice . { b1 where b1 is Element of F2() : P1[t,b1] } is set
x is Element of F2()
F1() is non empty set
F2() is non empty set
Fin F1() is non empty cup-closed diff-closed preBoolean set
F3() is finite Element of Fin F1()
Funcs (F1(),F2()) is non empty FUNCTION_DOMAIN of F1(),F2()
M is Element of F1()
[:F1(),F2():] is Relation-like non empty set
bool [:F1(),F2():] is non empty cup-closed diff-closed preBoolean set
M is Relation-like F1() -defined F2() -valued Function-like quasi_total Element of bool [:F1(),F2():]
f is Relation-like F1() -defined F2() -valued Function-like quasi_total Element of Funcs (F1(),F2())
x is Element of F1()
f . x is Element of F2()
F3() is set
F1() is non empty set
F2() is non empty set
{ b1 where b1 is Element of F2() : ex b2 being Element of F1() st
( P1[b2,b1] & b2 in F3() )
}
is set

f is set
x is set
f is set
x is set
y is set
[:F1(),F2():] is Relation-like non empty set
bool [:F1(),F2():] is non empty cup-closed diff-closed preBoolean set
f is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom f is Element of bool F1()
bool F1() is non empty cup-closed diff-closed preBoolean set
f .: F3() is Element of bool F2()
bool F2() is non empty cup-closed diff-closed preBoolean set
x is set
y is Element of F2()
x is Element of F1()
x is Element of F1()
f . x is set
x is set
y is set
f . y is set
x is Element of F2()