{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
Y is Relation-like Function-like set
dom Y is set
x is Relation-like Function-like set
dom x is set
(dom Y) /\ (dom x) is set
Y \/ x is Relation-like set
X is set
f is set
[X,f] is set
{X,f} is non empty set
{X} is non empty set
{{X,f},{X}} is non empty set
p is set
[X,p] is set
{X,p} is non empty set
{{X,p},{X}} is non empty set
Y . X is set
x . X is set
(dom Y) \/ (dom x) is set
X is Relation-like Function-like set
f is set
p is set
[f,p] is set
{f,p} is non empty set
{f} is non empty set
{{f,p},{f}} is non empty set
Y is Relation-like Function-like set
x is Relation-like Function-like set
Y \/ x is Relation-like set
X is Relation-like Function-like set
dom Y is set
dom x is set
(dom Y) /\ (dom x) is set
f is set
Y . f is set
x . f is set
X . f is set
F1() is set
Y is set
F2(Y) is set
F3(Y) is set
Y is set
x is set
F2(Y) is set
F3(Y) is set
X is set
X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
dom X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
Y is set
rng X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial set
x is set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Function-like set
dom X is set
rng X is set
f is Relation-like Y -defined x -valued Element of bool [:Y,x:]
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is set
f is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
rng f is set
dom f is Element of bool Y
bool Y is non empty set
p is set
f . p is set
Y is set
x is set
X is Relation-like Y -valued Function-like set
dom X is set
X . x is set
rng X is set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
dom X is Element of bool Y
bool Y is non empty set
f is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
dom f is Element of bool Y
p is set
X . p is set
f . p is set
F1() is set
F2() is set
[:F1(),F2():] is Relation-like set
bool [:F1(),F2():] is non empty set
the set is set
x is set
X is set
X is set
f is set
x is set
X is set
p is set
f is set
q is set
x is Relation-like Function-like set
dom x is set
X is set
x | X is Relation-like Function-like set
dom (x | X) is set
rng (x | X) is set
p is set
q is set
(x | X) . q is set
x . q is set
p is set
p is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
q is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom q is Element of bool F1()
bool F1() is non empty set
p is set
q is set
(dom x) /\ X is set
p is set
x . p is set
q is set
q . p is set
Y is Relation-like Function-like set
dom Y is set
rng Y is set
x is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
X is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom X is Element of bool F1()
f is set
p is set
q is set
f is set
X . f is set
Y is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom Y is Element of bool F1()
x is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom x is Element of bool F1()
F2() is set
F1() is set
[:F1(),F2():] is Relation-like set
bool [:F1(),F2():] is non empty set
Y is set
x is set
F3(Y) is set
X is set
Y is set
x is set
F3(Y) is set
Y is Relation-like F1() -defined F2() -valued Function-like Element of bool [:F1(),F2():]
dom Y is Element of bool F1()
bool F1() is non empty set
x is set
F3(x) is set
X is set
F3(x) is set
X is set
x is set
Y . x is set
F3(x) is set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is set
f is set
[:X,f:] is Relation-like set
bool [:X,f:] is non empty set
p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
q is Relation-like X -defined f -valued Function-like Element of bool [:X,f:]
p * q is Relation-like Y -defined f -valued Function-like set
[:Y,f:] is Relation-like set
bool [:Y,f:] is non empty set
dom (p * q) is Element of bool Y
bool Y is non empty set
rng (p * q) is set
Y is set
id Y is Relation-like Y -defined Y -valued Function-like one-to-one set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Element of bool [:Y,x:]
(id Y) * X is Relation-like Y -defined x -valued set
dom X is Element of bool Y
bool Y is non empty set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
id x is Relation-like x -defined x -valued Function-like one-to-one set
X is Relation-like Y -defined x -valued Element of bool [:Y,x:]
X * (id x) is Relation-like Y -defined x -valued set
rng X is Element of bool x
bool x is non empty set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
dom X is Element of bool Y
bool Y is non empty set
f is set
p is set
X . f is set
X . p is set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
[:x,Y:] is Relation-like set
bool [:x,Y:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
X " is Relation-like Function-like set
rng X is set
dom (X ") is set
dom X is Element of bool Y
bool Y is non empty set
rng (X ") is set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is set
[:X,x:] is Relation-like set
bool [:X,x:] is non empty set
f is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
f | X is Relation-like Y -defined X -defined Y -defined x -valued Function-like Element of bool [:Y,x:]
dom (f | X) is Element of bool Y
bool Y is non empty set
rng (f | X) is set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
f is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
X is set
f | X is Relation-like Y -defined X -defined Y -defined x -valued Function-like Element of bool [:Y,x:]
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
f is set
X | f is Relation-like f -defined Y -defined x -valued Function-like set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is set
[:Y,X:] is Relation-like set
bool [:Y,X:] is non empty set
f is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
X |` f is Relation-like Y -defined x -valued X -valued x -valued Function-like Element of bool [:Y,x:]
dom (X |` f) is Element of bool Y
bool Y is non empty set
rng (X |` f) is set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is set
f is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
X |` f is Relation-like Y -defined x -valued X -valued x -valued Function-like Element of bool [:Y,x:]
Y is set
x is set
[:x,Y:] is Relation-like set
bool [:x,Y:] is non empty set
X is Relation-like Function-like set
Y |` X is Relation-like Function-like set
(Y |` X) | x is Relation-like Function-like set
X | x is Relation-like Function-like set
Y |` (X | x) is Relation-like Function-like set
dom ((Y |` X) | x) is set
rng ((Y |` X) | x) is set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is set
f is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
f .: Y is set
dom f is Element of bool Y
bool Y is non empty set
p is set
f . p is set
Y is set
{Y} is non empty set
x is set
[:{Y},x:] is Relation-like set
bool [:{Y},x:] is non empty set
X is Relation-like {Y} -defined x -valued Function-like Element of bool [:{Y},x:]
rng X is set
X . Y is set
{(X . Y)} is non empty set
dom X is Element of bool {Y}
bool {Y} is non empty set
Y is set
{Y} is non empty set
x is set
[:{Y},x:] is Relation-like set
bool [:{Y},x:] is non empty set
X is Relation-like {Y} -defined x -valued Function-like Element of bool [:{Y},x:]
f is set
dom X is set
X . f is set
p is set
X . p is set
dom X is Element of bool {Y}
bool {Y} is non empty set
Y is set
{Y} is non empty set
x is set
[:{Y},x:] is Relation-like set
bool [:{Y},x:] is non empty set
X is set
f is Relation-like {Y} -defined x -valued Function-like Element of bool [:{Y},x:]
f .: X is set
f . Y is set
{(f . Y)} is non empty set
rng f is set
Y is set
{Y} is non empty set
x is set
X is set
[:x,X:] is Relation-like set
bool [:x,X:] is non empty set
f is Relation-like Function-like set
dom f is set
f . Y is set
rng f is set
{(f . Y)} is non empty set
Y is set
x is set
{x} is non empty set
[:Y,{x}:] is Relation-like set
bool [:Y,{x}:] is non empty set
X is set
f is Relation-like Y -defined {x} -valued Function-like Element of bool [:Y,{x}:]
dom f is Element of bool Y
bool Y is non empty set
f . X is set
Y is set
x is set
{x} is non empty set
[:Y,{x}:] is Relation-like set
bool [:Y,{x}:] is non empty set
X is Relation-like Y -defined {x} -valued Function-like Element of bool [:Y,{x}:]
dom X is Element of bool Y
bool Y is non empty set
f is Relation-like Y -defined {x} -valued Function-like Element of bool [:Y,{x}:]
dom f is Element of bool Y
p is set
X . p is set
f . p is set
X is set
Y is Relation-like Function-like set
X |` Y is Relation-like Function-like set
x is set
(X |` Y) | x is Relation-like Function-like set
[:x,X:] is Relation-like set
bool [:x,X:] is non empty set
Y is set
x is set
X is Relation-like Function-like set
(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` X is Relation-like Function-like set
(x |` X) | Y is Relation-like Function-like set
Y is set
x is set
X is Relation-like Function-like set
(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` X is Relation-like Function-like set
(x |` X) | Y is Relation-like Function-like set
dom (X,Y,x) is Element of bool Y
bool Y is non empty set
dom X is set
rng (X,Y,x) is set
rng X is set
Y is set
x is set
X is set
f is Relation-like Function-like set
(f,x,X) is Relation-like x -defined X -valued Function-like Element of bool [:x,X:]
[:x,X:] is Relation-like set
bool [:x,X:] is non empty set
X |` f is Relation-like Function-like set
(X |` f) | x is Relation-like Function-like set
dom (f,x,X) is Element of bool x
bool x is non empty set
dom f is set
f . Y is set
dom (X |` f) is set
(dom (X |` f)) /\ x is set
dom (X |` f) is set
(dom (X |` f)) /\ x is set
Y is set
x is set
X is set
f is Relation-like Function-like set
dom f is set
f . Y is set
(f,x,X) is Relation-like x -defined X -valued Function-like Element of bool [:x,X:]
[:x,X:] is Relation-like set
bool [:x,X:] is non empty set
X |` f is Relation-like Function-like set
(X |` f) | x is Relation-like Function-like set
(f,x,X) . Y is set
dom (X |` f) is set
(X |` f) . Y is set
((X |` f) | x) . Y is set
Y is set
x is set
X is set
f is Relation-like Function-like set
(f,x,X) is Relation-like x -defined X -valued Function-like Element of bool [:x,X:]
[:x,X:] is Relation-like set
bool [:x,X:] is non empty set
X |` f is Relation-like Function-like set
(X |` f) | x is Relation-like Function-like set
dom (f,x,X) is Element of bool x
bool x is non empty set
(f,x,X) . Y is set
f . Y is set
dom f is set
Y is set
x is set
X is Relation-like Function-like set
f is Relation-like Function-like set
(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` X is Relation-like Function-like set
(x |` X) | Y is Relation-like Function-like set
(f,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
x |` f is Relation-like Function-like set
(x |` f) | Y is Relation-like Function-like set
dom (X,Y,x) is Element of bool Y
bool Y is non empty set
dom X is set
dom (f,Y,x) is Element of bool Y
p is set
dom f is set
X . p is set
f . p is set
p is set
(X,Y,x) . p is set
X . p is set
(f,Y,x) . p is set
f . p is set
Y is set
x is set
X is set
f is Relation-like Function-like set
(f,Y,X) is Relation-like Y -defined X -valued Function-like Element of bool [:Y,X:]
[:Y,X:] is Relation-like set
bool [:Y,X:] is non empty set
X |` f is Relation-like Function-like set
(X |` f) | Y is Relation-like Function-like set
(f,x,X) is Relation-like x -defined X -valued Function-like Element of bool [:x,X:]
[:x,X:] is Relation-like set
bool [:x,X:] is non empty set
(X |` f) | x is Relation-like Function-like set
dom (f,Y,X) is Element of bool Y
bool Y is non empty set
dom (f,x,X) is Element of bool x
bool x is non empty set
p is set
f . p is set
dom f is set
p is set
(f,Y,X) . p is set
f . p is set
(f,x,X) . p is set
Y is set
x is set
X is set
f is Relation-like Function-like set
(f,X,Y) is Relation-like X -defined Y -valued Function-like Element of bool [:X,Y:]
[:X,Y:] is Relation-like set
bool [:X,Y:] is non empty set
Y |` f is Relation-like Function-like set
(Y |` f) | X is Relation-like Function-like set
(f,X,x) is Relation-like X -defined x -valued Function-like Element of bool [:X,x:]
[:X,x:] is Relation-like set
bool [:X,x:] is non empty set
x |` f is Relation-like Function-like set
(x |` f) | X is Relation-like Function-like set
dom (f,X,Y) is Element of bool X
bool X is non empty set
dom (f,X,x) is Element of bool X
p is set
f . p is set
dom f is set
p is set
(f,X,Y) . p is set
f . p is set
(f,X,x) . p is set
Y is set
x is set
X is set
f is set
p is Relation-like Function-like set
(p,Y,X) is Relation-like Y -defined X -valued Function-like Element of bool [:Y,X:]
[:Y,X:] is Relation-like set
bool [:Y,X:] is non empty set
X |` p is Relation-like Function-like set
(X |` p) | Y is Relation-like Function-like set
(p,x,f) is Relation-like x -defined f -valued Function-like Element of bool [:x,f:]
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
f |` p is Relation-like Function-like set
(f |` p) | x is Relation-like Function-like set
(p,x,X) is Relation-like x -defined X -valued Function-like Element of bool [:x,X:]
[:x,X:] is Relation-like set
bool [:x,X:] is non empty set
(X |` p) | x is Relation-like Function-like set
Y is set
x is set
X is Relation-like Function-like set
dom X is set
rng X is set
(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` X is Relation-like Function-like set
(x |` X) | Y is Relation-like Function-like set
dom (X,Y,x) is Element of bool Y
bool Y is non empty set
f is set
X . f is set
f is set
X . f is set
(X,Y,x) . f is set
Y is Relation-like Function-like set
dom Y is set
rng Y is set
(Y,(dom Y),(rng Y)) is Relation-like dom Y -defined rng Y -valued Function-like Element of bool [:(dom Y),(rng Y):]
[:(dom Y),(rng Y):] is Relation-like set
bool [:(dom Y),(rng Y):] is non empty set
(rng Y) |` Y is Relation-like Function-like set
((rng Y) |` Y) | (dom Y) is Relation-like Function-like set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
x |` X is Relation-like Y -defined x -valued x -valued Function-like set
(x |` X) | Y is Relation-like Y -defined Y -defined x -valued Function-like set
Y is set
x is set
({},Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` {} is Relation-like Function-like set
(x |` {}) | Y is Relation-like Function-like set
dom {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
rng {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial set
Y is set
x is set
X is set
f is Relation-like Function-like set
(f,X,Y) is Relation-like X -defined Y -valued Function-like Element of bool [:X,Y:]
[:X,Y:] is Relation-like set
bool [:X,Y:] is non empty set
Y |` f is Relation-like Function-like set
(Y |` f) | X is Relation-like Function-like set
p is Relation-like Function-like set
(p,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` p is Relation-like Function-like set
(x |` p) | Y is Relation-like Function-like set
(X,Y,Y,x,(f,X,Y),(p,Y,x)) is Relation-like X -defined x -valued Function-like Element of bool [:X,x:]
[:X,x:] is Relation-like set
bool [:X,x:] is non empty set
f * p is Relation-like Function-like set
((f * p),X,x) is Relation-like X -defined x -valued Function-like Element of bool [:X,x:]
x |` (f * p) is Relation-like Function-like set
(x |` (f * p)) | X is Relation-like Function-like set
dom (X,Y,Y,x,(f,X,Y),(p,Y,x)) is Element of bool X
bool X is non empty set
q is set
(X,Y,Y,x,(f,X,Y),(p,Y,x)) . q is set
((f * p),X,x) . q is set
dom (f,X,Y) is Element of bool X
dom f is set
(f,X,Y) . q is set
dom (p,Y,x) is Element of bool Y
bool Y is non empty set
f . q is set
p . (f . q) is set
(f * p) . q is set
dom p is set
dom (f * p) is set
dom ((f * p),X,x) is Element of bool X
(p,Y,x) . ((f,X,Y) . q) is set
(p,Y,x) . (f . q) is set
dom ((f * p),X,x) is Element of bool X
q is set
dom (f,X,Y) is Element of bool X
dom f is set
(f,X,Y) . q is set
dom (p,Y,x) is Element of bool Y
bool Y is non empty set
f . q is set
p . (f . q) is set
(f * p) . q is set
dom p is set
dom (f * p) is set
Y is set
x is set
X is set
f is Relation-like Function-like set
rng f is set
p is Relation-like Function-like set
dom p is set
(rng f) /\ (dom p) is set
(f,X,Y) is Relation-like X -defined Y -valued Function-like Element of bool [:X,Y:]
[:X,Y:] is Relation-like set
bool [:X,Y:] is non empty set
Y |` f is Relation-like Function-like set
(Y |` f) | X is Relation-like Function-like set
(p,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` p is Relation-like Function-like set
(x |` p) | Y is Relation-like Function-like set
(X,Y,Y,x,(f,X,Y),(p,Y,x)) is Relation-like X -defined x -valued Function-like Element of bool [:X,x:]
[:X,x:] is Relation-like set
bool [:X,x:] is non empty set
f * p is Relation-like Function-like set
((f * p),X,x) is Relation-like X -defined x -valued Function-like Element of bool [:X,x:]
x |` (f * p) is Relation-like Function-like set
(x |` (f * p)) | X is Relation-like Function-like set
dom ((f * p),X,x) is Element of bool X
bool X is non empty set
dom (X,Y,Y,x,(f,X,Y),(p,Y,x)) is Element of bool X
q is set
dom (f * p) is set
f . q is set
dom f is set
(f * p) . q is set
p . (f . q) is set
dom (p,Y,x) is Element of bool Y
bool Y is non empty set
dom (f,X,Y) is Element of bool X
(f,X,Y) . q is set
q is set
((f * p),X,x) . q is set
(X,Y,Y,x,(f,X,Y),(p,Y,x)) . q is set
dom (f * p) is set
f . q is set
dom f is set
(f * p) . q is set
p . (f . q) is set
dom (p,Y,x) is Element of bool Y
bool Y is non empty set
dom (f,X,Y) is Element of bool X
(p,Y,x) . (f . q) is set
(f,X,Y) . q is set
(p,Y,x) . ((f,X,Y) . q) is set
Y is set
x is set
X is Relation-like Function-like set
(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` X is Relation-like Function-like set
(x |` X) | Y is Relation-like Function-like set
Y is set
x is set
X is Relation-like Function-like set
(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` X is Relation-like Function-like set
(x |` X) | Y is Relation-like Function-like set
(X,Y,x) " is Relation-like Function-like set
X " is Relation-like Function-like set
((X "),x,Y) is Relation-like x -defined Y -valued Function-like Element of bool [:x,Y:]
[:x,Y:] is Relation-like set
bool [:x,Y:] is non empty set
Y |` (X ") is Relation-like Function-like set
(Y |` (X ")) | x is Relation-like Function-like set
dom ((X,Y,x) ") is set
dom ((X "),x,Y) is Element of bool x
bool x is non empty set
f is set
rng (X,Y,x) is set
dom (X,Y,x) is Element of bool Y
bool Y is non empty set
p is set
(X,Y,x) . p is set
X . p is set
rng X is set
dom (X ") is set
dom X is set
(X ") . f is set
dom (X ") is set
rng X is set
dom X is set
p is set
X . p is set
(X ") . (X . p) is set
dom (X,Y,x) is Element of bool Y
bool Y is non empty set
(X,Y,x) . p is set
rng (X,Y,x) is set
f is set
((X "),x,Y) . f is set
((X,Y,x) ") . f is set
rng (X,Y,x) is set
rng X is set
dom X is set
p is set
X . p is set
(X ") . (X . p) is set
dom (X,Y,x) is Element of bool Y
bool Y is non empty set
(X,Y,x) . p is set
((X,Y,x) ") . ((X,Y,x) . p) is set
Y is set
x is set
X is set
Y /\ X is set
f is Relation-like Function-like set
(f,x,X) is Relation-like x -defined X -valued Function-like Element of bool [:x,X:]
[:x,X:] is Relation-like set
bool [:x,X:] is non empty set
X |` f is Relation-like Function-like set
(X |` f) | x is Relation-like Function-like set
Y |` (f,x,X) is Relation-like x -defined Y -valued X -valued Function-like Element of bool [:x,X:]
(f,x,(Y /\ X)) is Relation-like x -defined Y /\ X -valued Function-like Element of bool [:x,(Y /\ X):]
[:x,(Y /\ X):] is Relation-like set
bool [:x,(Y /\ X):] is non empty set
(Y /\ X) |` f is Relation-like Function-like set
((Y /\ X) |` f) | x is Relation-like Function-like set
f | x is Relation-like Function-like set
X |` (f | x) is Relation-like Function-like set
Y |` (X |` (f | x)) is Relation-like Function-like set
(Y /\ X) |` (f | x) is Relation-like Function-like set
Y is set
Y is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like non-empty empty-yielding Y -defined x -valued Function-like one-to-one constant functional empty Element of bool [:Y,x:]
dom X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty non proper Element of bool Y
bool Y is non empty set
Y is non empty set
x is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like non-empty empty-yielding Y -defined x -valued Function-like one-to-one constant functional empty Element of bool [:Y,x:]
dom X is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty proper Element of bool Y
bool Y is non empty set
Y is set
x is set
X is Relation-like Function-like set
(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` X is Relation-like Function-like set
(x |` X) | Y is Relation-like Function-like set
dom X is set
dom (X,Y,x) is Element of bool Y
bool Y is non empty set
f is set
Y is set
x is set
({},Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` {} is Relation-like Function-like set
(x |` {}) | Y is Relation-like Function-like set
dom {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
Y is set
x is set
X is Relation-like Function-like set
dom X is set
rng X is set
(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` X is Relation-like Function-like set
(x |` X) | Y is Relation-like Function-like set
dom (X,Y,x) is Element of bool Y
bool Y is non empty set
f is set
X . f is set
Y is set
x is set
X is Relation-like Function-like set
(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` X is Relation-like Function-like set
(x |` X) | Y is Relation-like Function-like set
X .: Y is set
dom (X,Y,x) is Element of bool Y
bool Y is non empty set
f is set
rng (X,Y,x) is set
dom X is set
p is set
X . p is set
(X,Y,x) . p is set
Y is set
x is set
X is Relation-like Function-like set
dom X is set
X .: Y is set
(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` X is Relation-like Function-like set
(x |` X) | Y is Relation-like Function-like set
dom (X,Y,x) is Element of bool Y
bool Y is non empty set
f is set
X . f is set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is set
f is set
p is Relation-like Function-like set
dom p is set
rng p is set
q is set
p is set
[q,p] is set
{q,p} is non empty set
{q} is non empty set
{{q,p},{q}} is non empty set
p . q is set
X is set
f is set
p is set
q is Relation-like Function-like set
dom q is set
rng q is set
q is Relation-like Function-like set
dom q is set
rng q is set
Y is set
x is set
(Y,x) is set
X is Relation-like Function-like set
dom X is set
rng X is set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
(Y,x) is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
dom X is Element of bool Y
bool Y is non empty set
rng X is set
Y is set
x is set
(Y,x) is non empty set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is set
f is Relation-like Function-like set
dom f is set
rng f is set
Y is set
x is set
(Y,x) is non empty set
X is Element of (Y,x)
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
{{}} is functional non empty set
Y is set
({},Y) is non empty set
x is set
[:{},Y:] is Relation-like set
bool [:{},Y:] is non empty set
[:{},Y:] is Relation-like set
bool [:{},Y:] is non empty set
Y is set
(Y,{}) is non empty set
x is set
[:Y,{}:] is Relation-like set
bool [:Y,{}:] is non empty set
[:Y,{}:] is Relation-like set
bool [:Y,{}:] is non empty set
Y is set
x is set
X is set
(Y,X) is non empty set
f is set
(x,f) is non empty set
p is set
[:Y,X:] is Relation-like set
bool [:Y,X:] is non empty set
[:x,f:] is Relation-like set
bool [:x,f:] is non empty set
f is set
X is Relation-like Function-like set
dom X is set
(dom X) /\ (dom X) is set
X . f is set
X is Relation-like Function-like set
dom X is set
f is Relation-like Function-like set
dom f is set
(dom X) /\ (dom f) is set
p is set
(dom f) /\ (dom X) is set
f . p is set
X . p is set
Y is Relation-like Function-like set
x is Relation-like Function-like set
Y \/ x is Relation-like set
dom Y is set
dom x is set
(dom Y) /\ (dom x) is set
X is Relation-like Function-like set
f is set
Y . f is set
x . f is set
X is Relation-like Function-like set
f is set
Y . f is set
x . f is set
p is Relation-like Function-like set
Y is Relation-like Function-like set
x is Relation-like Function-like set
Y \/ x is Relation-like set
X is Relation-like Function-like set
X is Relation-like Function-like set
X is Relation-like Function-like set
f is Relation-like Function-like set
p is Relation-like Function-like set
Y is Relation-like Function-like set
dom Y is set
x is Relation-like Function-like set
dom x is set
(dom Y) /\ (dom x) is set
X is set
Y . X is set
x . X is set
Y is Relation-like Function-like set
x is Relation-like Function-like set
Y is Relation-like Function-like set
dom Y is set
x is Relation-like Function-like set
dom x is set
X is set
Y . X is set
x . X is set
Y is Relation-like Function-like set
dom Y is set
x is Relation-like Function-like set
dom x is set
Y \/ x is Relation-like set
Y is Relation-like Function-like set
X is Relation-like Function-like set
x is Relation-like Function-like set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
f is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
p is Relation-like Function-like set
dom f is Element of bool Y
bool Y is non empty set
dom X is Element of bool Y
q is set
dom f is set
dom p is set
(dom f) /\ (dom p) is set
f . q is set
p . q is set
(dom f) /\ (dom p) is Element of bool Y
X . q is set
(dom X) /\ (dom p) is Element of bool Y
Y is Relation-like Function-like set
{} \/ Y is Relation-like set
Y is set
x is set
({},Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` {} is Relation-like Function-like set
(x |` {}) | Y is Relation-like Function-like set
X is Relation-like Function-like set
Y is set
x is set
{x} is non empty set
[:Y,{x}:] is Relation-like set
bool [:Y,{x}:] is non empty set
X is Relation-like Y -defined {x} -valued Function-like Element of bool [:Y,{x}:]
f is Relation-like Y -defined {x} -valued Function-like Element of bool [:Y,{x}:]
p is set
dom X is set
dom f is set
(dom X) /\ (dom f) is set
X . p is set
f . p is set
dom X is Element of bool Y
bool Y is non empty set
dom f is Element of bool Y
(dom X) /\ (dom f) is Element of bool Y
Y is set
x is Relation-like Function-like set
x | Y is Relation-like Function-like set
Y is set
x is Relation-like Function-like set
Y |` x is Relation-like Function-like set
Y is set
x is set
X is Relation-like Function-like set
Y |` X is Relation-like Function-like set
(Y |` X) | x is Relation-like Function-like set
X is Relation-like Function-like set
Y is set
x is set
(X,Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
x |` X is Relation-like Function-like set
(x |` X) | Y is Relation-like Function-like set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
f is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
dom X is Element of bool Y
bool Y is non empty set
dom f is Element of bool Y
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
f is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
dom p is Element of bool Y
bool Y is non empty set
q is set
dom X is set
dom f is set
(dom X) /\ (dom f) is set
X . q is set
f . q is set
dom X is Element of bool Y
dom f is Element of bool Y
(dom X) /\ (dom f) is Element of bool Y
(dom X) /\ (dom p) is Element of bool Y
p . q is set
(dom f) /\ (dom p) is Element of bool Y
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
f is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
({},Y,x) is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
x |` {} is Relation-like Function-like set
(x |` {}) | Y is Relation-like Function-like set
the Element of x is Element of x
dom X is Element of bool Y
bool Y is non empty set
dom f is Element of bool Y
q is set
X . q is set
f . q is set
p is set
(dom X) /\ (dom f) is Element of bool Y
p is set
p is set
p is set
q is set
p is set
X . q is set
f . q is set
q is set
q is Relation-like Function-like set
dom q is set
rng q is set
p is set
q is set
q . q is set
X . q is set
X . q is set
f . q is set
q is set
dom X is set
(dom X) /\ (dom q) is set
X . q is set
q . q is set
(dom X) /\ (dom q) is Element of bool Y
q is set
dom f is set
(dom f) /\ (dom q) is set
f . q is set
q . q is set
(dom f) /\ (dom q) is Element of bool Y
p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
(Y,x) is non empty set
f is set
q is set
p is set
p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
f is set
f is set
p is set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
(Y,x,X) is set
f is set
p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
f is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
(Y,x,X) is set
p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
(Y,x,X) is set
f is Relation-like Function-like set
p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
Y is non empty set
x is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like non-empty empty-yielding Y -defined x -valued Function-like one-to-one constant functional empty (Y) Element of bool [:Y,x:]
(Y,x,X) is set
the Element of (Y,x,X) is Element of (Y,x,X)
[:Y,{}:] is Relation-like set
bool [:Y,{}:] is non empty set
p is Relation-like non-empty empty-yielding Y -defined {} -valued Function-like one-to-one constant functional empty (Y) Element of bool [:Y,{}:]
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
(Y,x,X) is set
{X} is functional non empty set
f is set
p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
Y is set
[:{},Y:] is Relation-like set
bool [:{},Y:] is non empty set
x is Relation-like non-empty empty-yielding {} -defined Y -valued Function-like one-to-one constant functional empty ( {} ) Element of bool [:{},Y:]
({},Y,x) is set
{x} is functional non empty set
Y is set
[:{},Y:] is Relation-like set
bool [:{},Y:] is non empty set
x is Relation-like non-empty empty-yielding {} -defined Y -valued Function-like one-to-one constant functional empty ( {} ) Element of bool [:{},Y:]
({},Y,x) is set
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
(Y,x,X) is set
f is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
(Y,x,f) is set
(Y,x,X) /\ (Y,x,f) is set
the Element of (Y,x,X) /\ (Y,x,f) is Element of (Y,x,X) /\ (Y,x,f)
q is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
Y is set
x is set
[:Y,x:] is Relation-like set
bool [:Y,x:] is non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
f is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
(Y,x,X) is set
(Y,x,f) is set
p is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
(Y,x,X) /\ (Y,x,f) is set
Y is set
[:Y,Y:] is Relation-like set
bool [:Y,Y:] is non empty set
id Y is Relation-like Y -defined Y -valued Function-like one-to-one set
x is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]
dom x is Element of bool Y
bool Y is non empty set
Y is set
id Y is Relation-like Y -defined Y -valued Function-like one-to-one set
x is Relation-like set
dom x is set
rng x is set
field x is set
(dom x) \/ (rng x) is set
X is set
[X,X] is set
{X,X} is non empty set
{X} is non empty set
{{X,X},{X}} is non empty set
X is set
f is set
[X,f] is set
{X,f} is non empty set
{X} is non empty set
{{X,f},{X}} is non empty set
[f,X] is set
{f,X} is non empty set
{f} is non empty set
{{f,X},{f}} is non empty set
X is set
f is set
[X,f] is set
{X,f} is non empty set
{X} is non empty set
{{X,f},{X}} is non empty set
[f,X] is set
{f,X} is non empty set
{f} is non empty set
{{f,X},{f}} is non empty set
X is set
f is set
p is set
[X,f] is set
{X,f} is non empty set
{X} is non empty set
{{X,f},{X}} is non empty set
[f,p] is set
{f,p} is non empty set
{f} is non empty set
{{f,p},{f}} is non empty set
[X,p] is set
{X,p} is non empty set
{{X,p},{X}} is non empty set
Y is set
id Y is Relation-like Y -defined Y -valued Function-like one-to-one set
[:Y,Y:] is Relation-like set
bool [:Y,Y:] is non empty set
dom (id Y) is Element of bool Y
bool Y is non empty set
rng (id Y) is set
Y is set
[:Y,Y:] is Relation-like set
bool [:Y,Y:] is non empty set
id Y is Relation-like Y -defined Y -valued Function-like one-to-one set
x is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]
Y is Relation-like set
field Y is set
dom Y is set
rng Y is set
(dom Y) \/ (rng Y) is set
x is set
[x,x] is set
{x,x} is non empty set
{x} is non empty set
{{x,x},{x}} is non empty set
X is set
[x,X] is set
{x,X} is non empty set
{{x,X},{x}} is non empty set
[X,x] is set
{X,x} is non empty set
{X} is non empty set
{{X,x},{X}} is non empty set
Y is set
id Y is Relation-like Y -defined Y -valued Function-like one-to-one set
Y is set
id Y is Relation-like Y -defined Y -valued Function-like one-to-one reflexive symmetric antisymmetric transitive set
[:Y,Y:] is Relation-like set
bool [:Y,Y:] is non empty set
F1() is non empty set
Y is Relation-like Function-like set
dom Y is set
x is Element of F1()
Y . x is set
F2(x) is set
X is Element of F1()
Y . X is set
F3(X) is set
Y is set
x is set
[Y,x] is set
{Y,x} is non empty set
{Y} is non empty set
{{Y,x},{Y}} is non empty set
X is set
[Y,X] is set
{Y,X} is non empty set
{{Y,X},{Y}} is non empty set
f is Relation-like Function-like set
p is Relation-like Function-like set
f \/ p is Relation-like set
q is Relation-like Function-like set
Y is set
union Y is set
x is set
X is set
[x,X] is set
{x,X} is non empty set
{x} is non empty set
{{x,X},{x}} is non empty set
f is set
[x,f] is set
{x,f} is non empty set
{{x,f},{x}} is non empty set
p is set
q is set
p is Relation-like Function-like set
q is Relation-like Function-like set
x is set
X is set
f is Relation-like Function-like set
Y is set
X is set
x is Relation-like Y -valued Function-like set
dom x is set
x . X is set
Y is non empty set
x is non empty set
[:Y,x:] is Relation-like non empty set
bool [:Y,x:] is non empty set
choose Y is Element of Y
choose x is Element of x
[(choose Y),(choose x)] is set
{(choose Y),(choose x)} is non empty set
{(choose Y)} is non empty set
{{(choose Y),(choose x)},{(choose Y)}} is non empty set
{[(choose Y),(choose x)]} is Relation-like Function-like non empty set
X is Relation-like Y -defined x -valued Function-like Element of bool [:Y,x:]
Y is set
x is set
(Y,x) is non empty set
X is set
f is Relation-like Function-like set
dom f is set
rng f is set
X is Relation-like Function-like set
rng X is set
Y is Relation-like Function-like set
dom Y is set
x is Relation-like Function-like set
dom x is set
X * Y is Relation-like Function-like set
X * x is Relation-like Function-like set
dom (X * x) is set
dom X is set
dom (X * Y) is set
f is set
(X * x) . f is set
X . f is set
x . (X . f) is set
(dom Y) /\ (dom x) is set
(X * Y) . f is set
Y . (X . f) is set
Y is set
x is set
X is set
f is Relation-like Y -valued Function-like set
f | X is Relation-like Y -valued Function-like set
dom (f | X) is set
(Y,(f | X),x) is Element of Y
(Y,f,x) is Element of Y
dom f is set
(f | X) . x is set
f . x is set