K128() is Element of bool K124()
K124() is set
bool K124() is non empty set
K123() is set
bool K123() is non empty set
bool K128() is non empty set
BOOLEAN is non empty set
1 is non empty set
[:1,1:] is non empty Relation-like set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty Relation-like set
bool [:[:1,1:],1:] is non empty set
{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() set
the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() set
TRUE is boolean Element of BOOLEAN
FALSE is boolean Element of BOOLEAN
K129() is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() Element of K128()
field {} is set
K174() is set
K175() is set
{{}} is non empty functional set
X is non empty set
PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
bool (PARTITIONS X) is non empty set
f is non empty Element of bool (PARTITIONS X)
a is Element of f
X is non empty set
PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
{} (PARTITIONS X) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() Element of bool (PARTITIONS X)
bool (PARTITIONS X) is non empty set
'/\' ({} (PARTITIONS X)) is non empty with_non-empty_elements a_partition of X
%O X is non empty with_non-empty_elements a_partition of X
f is set
{X} is non empty set
a is Relation-like Function-like set
{} (bool X) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() Element of bool (bool X)
x is Relation-like Function-like set
dom x is set
rng x is set
y is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() Element of bool (bool X)
z is set
x . z is set
Intersect y is Element of bool X
a is Relation-like Function-like set
dom a is set
rng a is set
x is Element of bool (bool X)
Intersect x is Element of bool X
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
a is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
f \/ a is Relation-like X -defined X -valued Element of bool [:X,X:]
f * a is Relation-like X -defined X -valued Element of bool [:X,X:]
x is Element of X
y is Element of X
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
[y,y] is set
{y,y} is non empty set
{y} is non empty set
{{y,y},{y}} is non empty set
[x,x] is set
{x,x} is non empty set
{{x,x},{x}} is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is Relation-like X -defined X -valued Element of bool [:X,X:]
nabla X is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
nabla X is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
f is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
(nabla X) * f is Relation-like X -defined X -valued Element of bool [:X,X:]
f * (nabla X) is Relation-like X -defined X -valued Element of bool [:X,X:]
(nabla X) \/ f is Relation-like X -defined X -valued Element of bool [:X,X:]
X is non empty set
f is non empty with_non-empty_elements a_partition of X
ERl f is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
a is Element of X
x is Element of X
[a,x] is set
{a,x} is non empty set
{a} is non empty set
{{a,x},{a}} is non empty set
EqClass (x,f) is Element of f
bool X is non empty set
y is Element of bool X
X is non empty set
x is non empty with_non-empty_elements a_partition of X
ERl x is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is non empty with_non-empty_elements a_partition of X
ERl f is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
a is non empty with_non-empty_elements a_partition of X
ERl a is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
(ERl f) * (ERl a) is Relation-like X -defined X -valued Element of bool [:X,X:]
y is Element of X
z is Element of X
EqClass (z,x) is Element of x
EqClass (z,a) is Element of a
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
B is Element of X
[y,B] is set
{y,B} is non empty set
{{y,B},{y}} is non empty set
[B,z] is set
{B,z} is non empty set
{B} is non empty set
{{B,z},{B}} is non empty set
x is Element of X
EqClass (x,f) is Element of f
B is Element of X
EqClass (B,f) is Element of f
[y,B] is set
{y,B} is non empty set
{{y,B},{y}} is non empty set
[B,z] is set
{B,z} is non empty set
{B} is non empty set
{{B,z},{B}} is non empty set
X is Relation-like set
f is Relation-like set
X * f is Relation-like set
a 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 Relation-like set
field X is set
f is set
a is set
[a,a] is set
{a,a} is non empty set
{a} is non empty set
{{a,a},{a}} is non empty set
X is set
[:X,X:] is Relation-like set
bool [:X,X:] is non empty set
f is Relation-like X -defined X -valued Element of bool [:X,X:]
field f is set
X \/ X is set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
a is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
f * a is Relation-like X -defined X -valued Element of bool [:X,X:]
a * f is Relation-like X -defined X -valued Element of bool [:X,X:]
field a is set
field f is set
field (f * a) is set
dom (f * a) is Element of bool X
bool X is non empty set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
[y,x] is set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
z is set
[x,z] is set
{x,z} is non empty set
{{x,z},{x}} is non empty set
[z,y] is set
{z,y} is non empty set
{z} is non empty set
{{z,y},{z}} is non empty set
[y,z] is set
{y,z} is non empty set
{{y,z},{y}} is non empty set
[z,x] is set
{z,x} is non empty set
{{z,x},{z}} is non empty set
f * f is Relation-like X -defined X -valued Element of bool [:X,X:]
a * a is Relation-like X -defined X -valued Element of bool [:X,X:]
(f * a) * (f * a) is Relation-like X -defined X -valued Element of bool [:X,X:]
(f * a) * f is Relation-like X -defined X -valued Element of bool [:X,X:]
((f * a) * f) * a is Relation-like X -defined X -valued Element of bool [:X,X:]
f * (f * a) is Relation-like X -defined X -valued Element of bool [:X,X:]
(f * (f * a)) * a is Relation-like X -defined X -valued Element of bool [:X,X:]
(f * f) * a is Relation-like X -defined X -valued Element of bool [:X,X:]
((f * f) * a) * a is Relation-like X -defined X -valued Element of bool [:X,X:]
(f * f) * (a * a) is Relation-like X -defined X -valued Element of bool [:X,X:]
X is non empty set
[:X,BOOLEAN:] is non empty Relation-like set
bool [:X,BOOLEAN:] is non empty set
f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
a is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' a is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
x is Element of X
('not' a) . x is boolean Element of BOOLEAN
('not' f) . x is boolean Element of BOOLEAN
a . x is boolean Element of BOOLEAN
'not' ('not' a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
('not' ('not' a)) . x is boolean Element of BOOLEAN
'not' TRUE is boolean Element of BOOLEAN
K105(1,TRUE) is set
f . x is boolean Element of BOOLEAN
'not' FALSE is boolean Element of BOOLEAN
K105(1,FALSE) is set
X is non empty set
[:X,BOOLEAN:] is non empty Relation-like set
bool [:X,BOOLEAN:] is non empty set
PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
bool (PARTITIONS X) is non empty set
f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
a is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
x is Element of bool (PARTITIONS X)
y is non empty with_non-empty_elements a_partition of X
All (f,y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
All (a,y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
z is Element of X
(All (f,y,x)) . z is boolean Element of BOOLEAN
(All (a,y,x)) . z is boolean Element of BOOLEAN
CompF (y,x) is non empty with_non-empty_elements a_partition of X
B_INF (f,(CompF (y,x))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
EqClass (z,(CompF (y,x))) is Element of CompF (y,x)
B is Element of X
a . B is boolean Element of BOOLEAN
f . B is boolean Element of BOOLEAN
B_INF (a,(CompF (y,x))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
X is non empty set
[:X,BOOLEAN:] is non empty Relation-like set
bool [:X,BOOLEAN:] is non empty set
PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
bool (PARTITIONS X) is non empty set
f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
a is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
x is Element of bool (PARTITIONS X)
y is non empty with_non-empty_elements a_partition of X
Ex (f,y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
Ex (a,y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' a is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' ('not' a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
Ex (('not' ('not' a)),y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
All (('not' a),y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' (All (('not' a),y,x)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
All (('not' f),y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' ('not' f) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
Ex (('not' ('not' f)),y,x) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' (All (('not' f),y,x)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
X is non empty set
PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
bool (PARTITIONS X) is non empty set
f is Element of bool (PARTITIONS X)
a is Element of bool (PARTITIONS X)
x is Element of bool (PARTITIONS X)
'/\' a is non empty with_non-empty_elements a_partition of X
ERl ('/\' a) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
'/\' x is non empty with_non-empty_elements a_partition of X
ERl ('/\' x) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
(ERl ('/\' a)) * (ERl ('/\' x)) is Relation-like X -defined X -valued Element of bool [:X,X:]
(ERl ('/\' x)) * (ERl ('/\' a)) is Relation-like X -defined X -valued Element of bool [:X,X:]
{} (PARTITIONS X) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() Element of bool (PARTITIONS X)
%O X is non empty with_non-empty_elements a_partition of X
ERl (%O X) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
(ERl ('/\' x)) * (ERl (%O X)) is Relation-like X -defined X -valued Element of bool [:X,X:]
nabla X is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
(ERl ('/\' x)) * (nabla X) is Relation-like X -defined X -valued Element of bool [:X,X:]
{} (PARTITIONS X) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V56() Element of bool (PARTITIONS X)
%O X is non empty with_non-empty_elements a_partition of X
ERl (%O X) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
(ERl (%O X)) * (ERl ('/\' a)) is Relation-like X -defined X -valued Element of bool [:X,X:]
nabla X is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
(nabla X) * (ERl ('/\' a)) is Relation-like X -defined X -valued Element of bool [:X,X:]
z is Element of X
B is Element of X
[z,B] is set
{z,B} is non empty set
{z} is non empty set
{{z,B},{z}} is non empty set
x is Element of X
[z,x] is set
{z,x} is non empty set
{{z,x},{z}} is non empty set
[x,B] is set
{x,B} is non empty set
{x} is non empty set
{{x,B},{x}} is non empty set
z is Element of bool X
y is Element of bool X
u is Relation-like Function-like set
dom u is set
rng u is set
u is Element of bool (bool X)
Intersect u is Element of bool X
hP is Relation-like Function-like set
dom hP is set
rng hP is set
FP is Element of bool (bool X)
Intersect FP is Element of bool X
P is non empty Element of bool (PARTITIONS X)
[:P,(bool X):] is non empty Relation-like set
bool [:P,(bool X):] is non empty set
hP9 is non empty Relation-like P -defined bool X -valued Function-like V17(P) quasi_total Element of bool [:P,(bool X):]
Q is non empty Element of bool (PARTITIONS X)
[:Q,(bool X):] is non empty Relation-like set
bool [:Q,(bool X):] is non empty set
hQ9 is non empty Relation-like Q -defined bool X -valued Function-like V17(Q) quasi_total Element of bool [:Q,(bool X):]
y is non empty Element of bool (PARTITIONS X)
h9 is non empty with_non-empty_elements (X,y)
[:y,(bool X):] is non empty Relation-like set
bool [:y,(bool X):] is non empty set
h9 is non empty Relation-like y -defined bool X -valued Function-like V17(y) quasi_total Element of bool [:y,(bool X):]
h9 +* hP9 is Relation-like Function-like set
(h9 +* hP9) +* hQ9 is Relation-like Function-like set
dom hQ9 is non empty Element of bool Q
bool Q is non empty set
dom hP9 is non empty Element of bool P
bool P is non empty set
FP9 is set
((h9 +* hP9) +* hQ9) . FP9 is set
hP9 . FP9 is set
u . FP9 is set
hP . FP9 is set
hQ9 . FP9 is set
FQ9 is non empty with_non-empty_elements (X,P)
EqClass (z,FQ9) is Element of FQ9
EqClass (x,FQ9) is Element of FQ9
EqClass (B,FQ9) is Element of FQ9
(h9 +* hP9) . FP9 is set
rng hP9 is non empty Element of bool (bool X)
rng hQ9 is non empty Element of bool (bool X)
FP9 is Element of bool (bool X)
Intersect FP9 is Element of bool X
FQ9 is Element of bool (bool X)
Intersect FQ9 is Element of bool X
F is set
t is set
hP9 . t is set
a is non empty with_non-empty_elements (X,P)
EqClass (B,a) is Element of a
F is set
t is set
hQ9 . t is set
a is non empty with_non-empty_elements (X,Q)
EqClass (z,a) is Element of a
F is set
hQ9 . F is set
t is non empty with_non-empty_elements (X,Q)
hQ9 . t is Element of bool X
EqClass (z,t) is Element of t
rng (h9 +* hP9) is set
rng h9 is non empty Element of bool (bool X)
(rng h9) \/ (rng hP9) is non empty Element of bool (bool X)
rng ((h9 +* hP9) +* hQ9) is set
(rng (h9 +* hP9)) \/ (rng hQ9) is non empty set
dom ((h9 +* hP9) +* hQ9) is set
dom (h9 +* hP9) is set
(dom (h9 +* hP9)) \/ Q is non empty set
dom h9 is non empty Element of bool y
bool y is non empty set
(dom h9) \/ P is non empty set
((dom h9) \/ P) \/ Q is non empty set
f \/ P is non empty Element of bool (PARTITIONS X)
(f \/ P) \/ Q is non empty Element of bool (PARTITIONS X)
f \/ Q is non empty Element of bool (PARTITIONS X)
t is set
hP9 . t is set
a is non empty with_non-empty_elements (X,P)
hP9 . a is Element of bool X
EqClass (B,a) is Element of a
t is set
((h9 +* hP9) +* hQ9) . t is set
P \/ Q is non empty Element of bool (PARTITIONS X)
(P \/ Q) \/ f is non empty Element of bool (PARTITIONS X)
f \ (P \/ Q) is Element of bool (PARTITIONS X)
(f \ (P \/ Q)) \/ (P \/ Q) is non empty Element of bool (PARTITIONS X)
hQ9 . t is set
hP9 . t is set
hP9 +* hQ9 is Relation-like Function-like set
h9 +* (hP9 +* hQ9) is Relation-like Function-like set
dom (hP9 +* hQ9) is set
h9 . t is set
F is Element of bool (bool X)
Intersect F is Element of bool X
t is Element of X
a is set
b is set
hP9 . b is set
((h9 +* hP9) +* hQ9) . b is set
'/\' P is non empty with_non-empty_elements a_partition of X
[t,B] is set
{t,B} is non empty set
{t} is non empty set
{{t,B},{t}} is non empty set
ERl ('/\' P) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
a is set
b is set
hQ9 . b is set
b is non empty with_non-empty_elements (X,Q)
hQ9 . b is Element of bool X
((h9 +* hP9) +* hQ9) . b is set
'/\' Q is non empty with_non-empty_elements a_partition of X
[z,t] is set
{z,t} is non empty set
{{z,t},{z}} is non empty set
ERl ('/\' Q) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
X is non empty set
PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
bool (PARTITIONS X) is non empty set
f is Element of bool (PARTITIONS X)
a is Element of bool (PARTITIONS X)
x is Element of bool (PARTITIONS X)
'/\' a is non empty with_non-empty_elements a_partition of X
ERl ('/\' a) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
'/\' x is non empty with_non-empty_elements a_partition of X
ERl ('/\' x) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
(ERl ('/\' a)) * (ERl ('/\' x)) is Relation-like X -defined X -valued Element of bool [:X,X:]
(ERl ('/\' x)) * (ERl ('/\' a)) is Relation-like X -defined X -valued Element of bool [:X,X:]
X is non empty set
[:X,BOOLEAN:] is non empty Relation-like set
bool [:X,BOOLEAN:] is non empty set
PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
bool (PARTITIONS X) is non empty set
f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
a is Element of bool (PARTITIONS X)
x is non empty with_non-empty_elements a_partition of X
All (f,x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
y is non empty with_non-empty_elements a_partition of X
All ((All (f,x,a)),y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
All (f,y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
All ((All (f,y,a)),x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
{x} is non empty Element of bool (PARTITIONS X)
a \ {x} is Element of bool (PARTITIONS X)
{y} is non empty Element of bool (PARTITIONS X)
a \ {y} is Element of bool (PARTITIONS X)
CompF (x,a) is non empty with_non-empty_elements a_partition of X
'/\' (a \ {x}) is non empty with_non-empty_elements a_partition of X
CompF (y,a) is non empty with_non-empty_elements a_partition of X
'/\' (a \ {y}) is non empty with_non-empty_elements a_partition of X
ERl ('/\' (a \ {x})) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
ERl ('/\' (a \ {y})) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
(ERl ('/\' (a \ {x}))) * (ERl ('/\' (a \ {y}))) is Relation-like X -defined X -valued Element of bool [:X,X:]
(ERl ('/\' (a \ {y}))) * (ERl ('/\' (a \ {x}))) is Relation-like X -defined X -valued Element of bool [:X,X:]
B_INF (f,(CompF (x,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
B_INF (f,(CompF (y,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
B_INF ((B_INF (f,(CompF (y,a)))),(CompF (x,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
x is Element of X
EqClass (x,(CompF (y,a))) is Element of CompF (y,a)
(B_INF ((B_INF (f,(CompF (y,a)))),(CompF (x,a)))) . x is boolean Element of BOOLEAN
EqClass (x,(CompF (x,a))) is Element of CompF (x,a)
z is Element of X
(B_INF (f,(CompF (y,a)))) . z is boolean Element of BOOLEAN
[z,x] is set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
EqClass (z,(CompF (y,a))) is Element of CompF (y,a)
y is Element of X
f . y is boolean Element of BOOLEAN
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
[y,x] is set
{y,x} is non empty set
{{y,x},{y}} is non empty set
u is set
[y,u] is set
{y,u} is non empty set
{{y,u},{y}} is non empty set
[u,x] is set
{u,x} is non empty set
{u} is non empty set
{{u,x},{u}} is non empty set
field (ERl ('/\' (a \ {y}))) is set
u is Element of X
(B_INF (f,(CompF (x,a)))) . u is boolean Element of BOOLEAN
EqClass (u,(CompF (x,a))) is Element of CompF (x,a)
z is Element of X
(B_INF (f,(CompF (x,a)))) . z is boolean Element of BOOLEAN
EqClass (z,(CompF (x,a))) is Element of CompF (x,a)
y is Element of X
f . y is boolean Element of BOOLEAN
[z,x] is set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
[y,x] is set
{y,x} is non empty set
{{y,x},{y}} is non empty set
u is set
[y,u] is set
{y,u} is non empty set
{{y,u},{y}} is non empty set
[u,x] is set
{u,x} is non empty set
{u} is non empty set
{{u,x},{u}} is non empty set
field (ERl ('/\' (a \ {y}))) is set
u is Element of X
EqClass (u,(CompF (y,a))) is Element of CompF (y,a)
(B_INF (f,(CompF (y,a)))) . u is boolean Element of BOOLEAN
B_INF ((All (f,x,a)),(CompF (y,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
B_INF ((B_INF (f,(CompF (x,a)))),(CompF (y,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
B_INF ((All (f,y,a)),(CompF (x,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
X is non empty set
[:X,BOOLEAN:] is non empty Relation-like set
bool [:X,BOOLEAN:] is non empty set
PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
bool (PARTITIONS X) is non empty set
f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
a is Element of bool (PARTITIONS X)
x is non empty with_non-empty_elements a_partition of X
Ex (f,x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
y is non empty with_non-empty_elements a_partition of X
Ex ((Ex (f,x,a)),y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
Ex (f,y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
Ex ((Ex (f,y,a)),x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' (Ex ((Ex (f,x,a)),y,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' ('not' (Ex ((Ex (f,x,a)),y,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' (Ex (f,x,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
All (('not' (Ex (f,x,a))),y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' (All (('not' (Ex (f,x,a))),y,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
All (('not' f),x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
All ((All (('not' f),x,a)),y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' (All ((All (('not' f),x,a)),y,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
All (('not' f),y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
All ((All (('not' f),y,a)),x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' (All ((All (('not' f),y,a)),x,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' (Ex (f,y,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
All (('not' (Ex (f,y,a))),x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' (All (('not' (Ex (f,y,a))),x,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' (Ex ((Ex (f,y,a)),x,a)) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
'not' ('not' (Ex ((Ex (f,y,a)),x,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
X is non empty set
[:X,BOOLEAN:] is non empty Relation-like set
bool [:X,BOOLEAN:] is non empty set
PARTITIONS X is non empty partition-membered Element of bool (bool (bool X))
bool X is non empty Element of bool (bool X)
bool X is non empty set
bool (bool X) is non empty set
bool (bool X) is non empty set
bool (bool (bool X)) is non empty set
bool (PARTITIONS X) is non empty set
f is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
a is Element of bool (PARTITIONS X)
x is non empty with_non-empty_elements a_partition of X
All (f,x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
y is non empty with_non-empty_elements a_partition of X
Ex ((All (f,x,a)),y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
Ex (f,y,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
All ((Ex (f,y,a)),x,a) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
{x} is non empty Element of bool (PARTITIONS X)
a \ {x} is Element of bool (PARTITIONS X)
{y} is non empty Element of bool (PARTITIONS X)
a \ {y} is Element of bool (PARTITIONS X)
'/\' (a \ {x}) is non empty with_non-empty_elements a_partition of X
ERl ('/\' (a \ {x})) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
'/\' (a \ {y}) is non empty with_non-empty_elements a_partition of X
ERl ('/\' (a \ {y})) is Relation-like X -defined X -valued V17(X) quasi_total reflexive symmetric transitive Element of bool [:X,X:]
(ERl ('/\' (a \ {x}))) * (ERl ('/\' (a \ {y}))) is Relation-like X -defined X -valued Element of bool [:X,X:]
(ERl ('/\' (a \ {y}))) * (ERl ('/\' (a \ {x}))) is Relation-like X -defined X -valued Element of bool [:X,X:]
CompF (x,a) is non empty with_non-empty_elements a_partition of X
CompF (y,a) is non empty with_non-empty_elements a_partition of X
B_SUP ((All (f,x,a)),(CompF (y,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
x is Element of X
(Ex ((All (f,x,a)),y,a)) . x is boolean Element of BOOLEAN
(All ((Ex (f,y,a)),x,a)) . x is boolean Element of BOOLEAN
EqClass (x,(CompF (x,a))) is Element of CompF (x,a)
z is Element of X
(Ex (f,y,a)) . z is boolean Element of BOOLEAN
EqClass (x,(CompF (y,a))) is Element of CompF (y,a)
y is Element of X
(All (f,x,a)) . y is boolean Element of BOOLEAN
[z,x] is set
{z,x} is non empty set
{z} is non empty set
{{z,x},{z}} is non empty set
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
[y,x] is set
{y,x} is non empty set
{y} is non empty set
{{y,x},{y}} is non empty set
[y,z] is set
{y,z} is non empty set
{{y,z},{y}} is non empty set
u is set
[y,u] is set
{y,u} is non empty set
{{y,u},{y}} is non empty set
[u,z] is set
{u,z} is non empty set
{u} is non empty set
{{u,z},{u}} is non empty set
field (ERl ('/\' (a \ {y}))) is set
u is Element of X
[u,y] is set
{u,y} is non empty set
{u} is non empty set
{{u,y},{u}} is non empty set
B_INF (f,(CompF (x,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
EqClass (y,(CompF (x,a))) is Element of CompF (x,a)
f . u is boolean Element of BOOLEAN
B_SUP (f,(CompF (y,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
EqClass (z,(CompF (y,a))) is Element of CompF (y,a)
B_INF ((Ex (f,y,a)),(CompF (x,a))) is non empty Relation-like X -defined BOOLEAN -valued Function-like V17(X) quasi_total boolean-valued Element of bool [:X,BOOLEAN:]
X is set
f is set
[:X,f:] is Relation-like set
bool [:X,f:] is non empty set
X is set
f is set
(X,f) is Relation-like X -defined f -valued Element of bool [:X,f:]
[:X,f:] is Relation-like set
bool [:X,f:] is non empty set
X is non empty set
id X is non empty Relation-like X -defined X -valued Function-like one-to-one V17(X) reflexive symmetric antisymmetric transitive set
field (id X) is set
dom (id X) is non empty Element of bool X
bool X is non empty set
rng (id X) is non empty Element of bool X
X \/ X is non empty set
op1 is non empty Relation-like 1 -defined 1 -valued Function-like V17(1) quasi_total Element of bool [:1,1:]
[{},{}] is set
{{},{}} is non empty functional set
{{{},{}},{{}}} is non empty set
{[{},{}]} is non empty Relation-like Function-like set
dom op1 is non empty Element of bool 1
bool 1 is non empty set
op1 . {} is set
[{},(op1 . {})] is set
{{},(op1 . {})} is non empty set
{{{},(op1 . {})},{{}}} is non empty set
{[{},(op1 . {})]} is non empty Relation-like Function-like set
rng op1 is non empty Element of bool 1
{(op1 . {})} is non empty set
[:{{}},{{}}:] is non empty Relation-like set
X is set
f is set
(X,f) is empty Relation-like non-empty empty-yielding X -defined f -valued Function-like one-to-one constant functional V56() Element of bool [:X,f:]
[:X,f:] is Relation-like set
bool [:X,f:] is non empty set
field (X,f) is set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is Relation-like X -defined X -valued Element of bool [:X,X:]
field f is set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is Relation-like X -defined X -valued Element of bool [:X,X:]
a is set
field f is set
x is set
[a,x] is set
{a,x} is non empty set
{a} is non empty set
{{a,x},{a}} is non empty set
[x,a] is set
{x,a} is non empty set
{x} is non empty set
{{x,a},{x}} is non empty set
X \/ X is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is non empty set
a is Relation-like X -defined X -valued Element of bool [:X,X:]
field a is set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty 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 non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is non empty set
a is Relation-like X -defined X -valued Element of bool [:X,X:]
field a is set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty 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 non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is Relation-like X -defined X -valued Element of bool [:X,X:]
a is set
field f is set
x is set
[a,x] is set
{a,x} is non empty set
{a} is non empty set
{{a,x},{a}} is non empty set
[x,a] is set
{x,a} is non empty set
{x} is non empty set
{{x,a},{x}} is non empty set
X \/ X is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is non empty set
a is Relation-like X -defined X -valued Element of bool [:X,X:]
field a is set
x is set
y is set
z is set
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
[y,z] is set
{y,z} is non empty set
{y} is non empty set
{{y,z},{y}} is non empty set
[x,z] is set
{x,z} is non empty set
{{x,z},{x}} is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is Relation-like X -defined X -valued Element of bool [:X,X:]
a is set
field f is set
x is set
y is set
[a,x] is set
{a,x} is non empty set
{a} is non empty set
{{a,x},{a}} is non empty set
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
[a,y] is set
{a,y} is non empty set
{{a,y},{a}} is non empty set
X \/ X is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is non empty set
a is Relation-like X -defined X -valued Element of bool [:X,X:]
field a is set
x is set
y is set
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty 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 non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is Relation-like X -defined X -valued Element of bool [:X,X:]
a is set
field f is set
x is set
[a,x] is set
{a,x} is non empty set
{a} is non empty set
{{a,x},{a}} is non empty set
[x,a] is set
{x,a} is non empty set
{x} is non empty set
{{x,a},{x}} is non empty set
X \/ X is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is non empty set
a is Relation-like X -defined X -valued Element of bool [:X,X:]
field a 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 \ (field a) is Element of bool f
bool f is non empty set
(field a) \/ (f \ (field a)) is set
dom a is Element of bool X
bool X is non empty set
rng a is Element of bool X
(dom a) \/ (rng a) is Element of bool X
f \ ((dom a) \/ (rng a)) is Element of bool f
f \ (dom a) is Element of bool f
f \ (rng a) is Element of bool f
(f \ (dom a)) /\ (f \ (rng a)) is Element of bool f
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is Relation-like X -defined X -valued Element of bool [:X,X:]
field f is set
X \/ X is non empty set
a is set
[a,a] is set
{a,a} is non empty set
{a} is non empty set
{{a,a},{a}} is non empty set
X is Relation-like set
field X is set
f is set
[f,f] is set
{f,f} is non empty set
{f} is non empty set
{{f,f},{f}} is non empty set
f is set
a is set
[f,a] is set
{f,a} is non empty set
{f} is non empty set
{{f,a},{f}} is non empty set
[a,f] is set
{a,f} is non empty set
{a} is non empty set
{{a,f},{a}} is non empty set
f is set
a is set
x is set
[f,a] is set
{f,a} is non empty set
{f} is non empty set
{{f,a},{f}} is non empty set
[a,x] is set
{a,x} is non empty set
{a} is non empty set
{{a,x},{a}} is non empty set
[f,x] is set
{f,x} is non empty set
{{f,x},{f}} is non empty set
X is non empty set
[:X,X:] is non empty Relation-like set
bool [:X,X:] is non empty set
f is non empty Relation-like X -defined X -valued Function-like V17(X) quasi_total Element of bool [:X,X:]
dom f is non empty Element of bool X
bool X is non empty set
a is Element of X
f . a is Element of X
f . (f . a) is Element of X
a is set
dom f is non empty set
f . a is set
f . (f . a) is set
X is Element of 1
op1 . X is Element of 1
op1 . (op1 . X) is Element of 1
X is Relation-like Function-like set
X is set
id X is Relation-like X -defined X -valued Function-like one-to-one V17(X) reflexive symmetric antisymmetric transitive set
a is set
dom (id X) is set
(id X) . a is set
(id X) . ((id X) . a) is set
dom (id X) is Element of bool X
bool X is non empty set