{} is set
the Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty set is Relation-like non-empty empty-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty set
field {} is set
X is set
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
a is set
b is set
[a,b] is set
{a,b} is set
{a} is set
{{a,b},{a}} is set
b is set
[b,a] is set
{b,a} is set
{b} is set
{{b,a},{b}} is set
a is set
[a,a] is set
{a,a} is set
{a} is set
{{a,a},{a}} is set
a is set
b is set
[a,b] is set
{a,b} is set
{a} is set
{{a,b},{a}} is set
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
a is Relation-like set
field a is set
dom a is set
rng a is set
(dom a) \/ (rng a) is set
b is set
X is set
[b,X] is set
{b,X} is set
{b} is set
{{b,X},{b}} is set
X is set
(X) is Relation-like set
field (X) is set
dom (X) is set
rng (X) is set
(dom (X)) \/ (rng (X)) is set
R is set
[R,R] is set
{R,R} is set
{R} is set
{{R,R},{R}} is set
R is set
field (X) is set
dom (X) is set
rng (X) is set
(dom (X)) \/ (rng (X)) is set
a is set
[R,a] is set
{R,a} is set
{R} is set
{{R,a},{R}} is set
b is set
[a,b] is set
{a,b} is set
{a} is set
{{a,b},{a}} is set
[R,b] is set
{R,b} is set
{{R,b},{R}} is set
field (X) is set
dom (X) is set
rng (X) is set
(dom (X)) \/ (rng (X)) is set
R is set
a is set
[R,a] is set
{R,a} is set
{R} is set
{{R,a},{R}} is set
[a,R] is set
{a,R} is set
{a} is set
{{a,R},{a}} is set
X is epsilon-transitive epsilon-connected ordinal set
(X) is Relation-like reflexive antisymmetric transitive set
R is set
field (X) is set
dom (X) is set
rng (X) is set
(dom (X)) \/ (rng (X)) is set
a is set
[R,a] is set
{R,a} is set
{R} is set
{{R,a},{R}} is set
[a,R] is set
{a,R} is set
{a} is set
{{a,R},{a}} is set
b is epsilon-transitive epsilon-connected ordinal set
X is epsilon-transitive epsilon-connected ordinal set
R is set
field (X) is set
dom (X) is set
rng (X) is set
(dom (X)) \/ (rng (X)) is set
the Element of R is Element of R
b is epsilon-transitive epsilon-connected ordinal set
X is epsilon-transitive epsilon-connected ordinal set
x is set
(X) -Seg x is set
Coim ((X),x) is set
{x} is set
(X) " {x} is set
(Coim ((X),x)) \ {x} is Element of bool (Coim ((X),x))
bool (Coim ((X),x)) is set
((X) -Seg x) /\ R is set
the Element of ((X) -Seg x) /\ R is Element of ((X) -Seg x) /\ R
[ the Element of ((X) -Seg x) /\ R,x] is set
{ the Element of ((X) -Seg x) /\ R,x} is set
{ the Element of ((X) -Seg x) /\ R} is set
{{ the Element of ((X) -Seg x) /\ R,x},{ the Element of ((X) -Seg x) /\ R}} is set
z is epsilon-transitive epsilon-connected ordinal set
X is set
(X) is Relation-like reflexive antisymmetric transitive set
R is set
(R) is Relation-like reflexive antisymmetric transitive set
(R) |_2 X is Relation-like set
[:X,X:] is Relation-like set
(R) /\ [:X,X:] is Relation-like set
a is set
b is set
[a,b] is set
{a,b} is set
{a} is set
{{a,b},{a}} is set
field (X) is set
dom (X) is set
rng (X) is set
(dom (X)) \/ (rng (X)) is set
X is epsilon-transitive epsilon-connected ordinal set
R is set
(R) is Relation-like reflexive antisymmetric transitive set
(X) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
(X) |_2 R is Relation-like set
[:R,R:] is Relation-like set
(X) /\ [:R,R:] is Relation-like set
X is epsilon-transitive epsilon-connected ordinal set
R is epsilon-transitive epsilon-connected ordinal set
(R) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
(R) -Seg X is set
Coim ((R),X) is set
{X} is set
(R) " {X} is set
(Coim ((R),X)) \ {X} is Element of bool (Coim ((R),X))
bool (Coim ((R),X)) is set
a is set
b is epsilon-transitive epsilon-connected ordinal set
[b,X] is set
{b,X} is set
{b} is set
{{b,X},{b}} is set
a is set
[a,X] is set
{a,X} is set
{a} is set
{{a,X},{a}} is set
field (R) is set
dom (R) is set
rng (R) is set
(dom (R)) \/ (rng (R)) is set
b is epsilon-transitive epsilon-connected ordinal set
X is epsilon-transitive epsilon-connected ordinal set
(X) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
R is epsilon-transitive epsilon-connected ordinal set
(R) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
field (X) is set
dom (X) is set
rng (X) is set
(dom (X)) \/ (rng (X)) is set
field (R) is set
dom (R) is set
rng (R) is set
(dom (R)) \/ (rng (R)) is set
(R) -Seg X is set
Coim ((R),X) is set
{X} is set
(R) " {X} is set
(Coim ((R),X)) \ {X} is Element of bool (Coim ((R),X))
bool (Coim ((R),X)) is set
(R) |_2 ((R) -Seg X) is Relation-like set
[:((R) -Seg X),((R) -Seg X):] is Relation-like set
(R) /\ [:((R) -Seg X),((R) -Seg X):] is Relation-like set
(X) -Seg R is set
Coim ((X),R) is set
{R} is set
(X) " {R} is set
(Coim ((X),R)) \ {R} is Element of bool (Coim ((X),R))
bool (Coim ((X),R)) is set
(X) |_2 ((X) -Seg R) is Relation-like set
[:((X) -Seg R),((X) -Seg R):] is Relation-like set
(X) /\ [:((X) -Seg R),((X) -Seg R):] is Relation-like set
X is Relation-like set
R is epsilon-transitive epsilon-connected ordinal set
(R) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
a is epsilon-transitive epsilon-connected ordinal set
(a) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
X is Relation-like set
field X is set
dom X is set
rng X is set
(dom X) \/ (rng X) is set
R is set
X -Seg R is set
Coim (X,R) is set
{R} is set
X " {R} is set
(Coim (X,R)) \ {R} is Element of bool (Coim (X,R))
bool (Coim (X,R)) is set
X |_2 (X -Seg R) is Relation-like set
[:(X -Seg R),(X -Seg R):] is Relation-like set
X /\ [:(X -Seg R),(X -Seg R):] is Relation-like set
a is epsilon-transitive epsilon-connected ordinal set
(a) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
b is set
X is epsilon-transitive epsilon-connected ordinal set
(X) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
R is set
X -Seg R is set
Coim (X,R) is set
{R} is set
X " {R} is set
(Coim (X,R)) \ {R} is Element of bool (Coim (X,R))
bool (Coim (X,R)) is set
X |_2 (X -Seg R) is Relation-like set
[:(X -Seg R),(X -Seg R):] is Relation-like set
X /\ [:(X -Seg R),(X -Seg R):] is Relation-like set
a is set
b is set
X is epsilon-transitive epsilon-connected ordinal set
(X) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
R is Relation-like Function-like set
dom R is set
rng R is set
a is set
b is set
R . b is set
X -Seg b is set
Coim (X,b) is set
{b} is set
X " {b} is set
(Coim (X,b)) \ {b} is Element of bool (Coim (X,b))
bool (Coim (X,b)) is set
X |_2 (X -Seg b) is Relation-like set
[:(X -Seg b),(X -Seg b):] is Relation-like set
X /\ [:(X -Seg b),(X -Seg b):] is Relation-like set
X is epsilon-transitive epsilon-connected ordinal set
(X) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
a is epsilon-transitive epsilon-connected ordinal set
b is set
X is set
R . X is set
X -Seg X is set
Coim (X,X) is set
{X} is set
X " {X} is set
(Coim (X,X)) \ {X} is Element of bool (Coim (X,X))
bool (Coim (X,X)) is set
X |_2 (X -Seg X) is Relation-like set
[:(X -Seg X),(X -Seg X):] is Relation-like set
X /\ [:(X -Seg X),(X -Seg X):] is Relation-like set
z is epsilon-transitive epsilon-connected ordinal set
(z) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
z is set
[z,b] is set
{z,b} is set
{z} is set
{{z,b},{z}} is set
(a) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
field (a) is set
dom (a) is set
rng (a) is set
(dom (a)) \/ (rng (a)) is set
P is epsilon-transitive epsilon-connected ordinal set
(z) |_2 P is Relation-like set
[:P,P:] is Relation-like set
(z) /\ [:P,P:] is Relation-like set
(P) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
(z) -Seg P is set
Coim ((z),P) is set
{P} is set
(z) " {P} is set
(Coim ((z),P)) \ {P} is Element of bool (Coim ((z),P))
bool (Coim ((z),P)) is set
field (z) is set
dom (z) is set
rng (z) is set
(dom (z)) \/ (rng (z)) is set
canonical_isomorphism_of ((z),(X |_2 (X -Seg X))) is Relation-like Function-like set
field (X |_2 (X -Seg X)) is set
dom (X |_2 (X -Seg X)) is set
rng (X |_2 (X -Seg X)) is set
(dom (X |_2 (X -Seg X))) \/ (rng (X |_2 (X -Seg X))) is set
(z) |_2 ((z) -Seg P) is Relation-like set
[:((z) -Seg P),((z) -Seg P):] is Relation-like set
(z) /\ [:((z) -Seg P),((z) -Seg P):] is Relation-like set
d is set
(X |_2 (X -Seg X)) -Seg d is set
Coim ((X |_2 (X -Seg X)),d) is set
{d} is set
(X |_2 (X -Seg X)) " {d} is set
(Coim ((X |_2 (X -Seg X)),d)) \ {d} is Element of bool (Coim ((X |_2 (X -Seg X)),d))
bool (Coim ((X |_2 (X -Seg X)),d)) is set
(X |_2 (X -Seg X)) |_2 ((X |_2 (X -Seg X)) -Seg d) is Relation-like set
[:((X |_2 (X -Seg X)) -Seg d),((X |_2 (X -Seg X)) -Seg d):] is Relation-like set
(X |_2 (X -Seg X)) /\ [:((X |_2 (X -Seg X)) -Seg d),((X |_2 (X -Seg X)) -Seg d):] is Relation-like set
X -Seg d is set
Coim (X,d) is set
X " {d} is set
(Coim (X,d)) \ {d} is Element of bool (Coim (X,d))
bool (Coim (X,d)) is set
[d,X] is set
{d,X} is set
{{d,X},{d}} is set
X |_2 (X -Seg d) is Relation-like set
[:(X -Seg d),(X -Seg d):] is Relation-like set
X /\ [:(X -Seg d),(X -Seg d):] is Relation-like set
R . d is set
b is set
(a) -Seg b is set
Coim ((a),b) is set
{b} is set
(a) " {b} is set
(Coim ((a),b)) \ {b} is Element of bool (Coim ((a),b))
bool (Coim ((a),b)) is set
b is epsilon-transitive epsilon-connected ordinal set
(b) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
field (b) is set
dom (b) is set
rng (b) is set
(dom (b)) \/ (rng (b)) is set
X is set
R . X is set
X is set
R . X is set
x is set
R . x is set
X -Seg x is set
Coim (X,x) is set
{x} is set
X " {x} is set
(Coim (X,x)) \ {x} is Element of bool (Coim (X,x))
bool (Coim (X,x)) is set
X |_2 (X -Seg x) is Relation-like set
[:(X -Seg x),(X -Seg x):] is Relation-like set
X /\ [:(X -Seg x),(X -Seg x):] is Relation-like set
y is epsilon-transitive epsilon-connected ordinal set
(y) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
X -Seg X is set
Coim (X,X) is set
{X} is set
X " {X} is set
(Coim (X,X)) \ {X} is Element of bool (Coim (X,X))
bool (Coim (X,X)) is set
X |_2 (X -Seg X) is Relation-like set
[:(X -Seg X),(X -Seg X):] is Relation-like set
X /\ [:(X -Seg X),(X -Seg X):] is Relation-like set
X is set
R . X is set
x is set
[X,x] is set
{X,x} is set
{X} is set
{{X,x},{X}} is set
R . x is set
[(R . X),(R . x)] is set
{(R . X),(R . x)} is set
{(R . X)} is set
{{(R . X),(R . x)},{(R . X)}} is set
X -Seg x is set
Coim (X,x) is set
{x} is set
X " {x} is set
(Coim (X,x)) \ {x} is Element of bool (Coim (X,x))
bool (Coim (X,x)) is set
X |_2 (X -Seg x) is Relation-like set
[:(X -Seg x),(X -Seg x):] is Relation-like set
X /\ [:(X -Seg x),(X -Seg x):] is Relation-like set
P is epsilon-transitive epsilon-connected ordinal set
(P) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
z is epsilon-transitive epsilon-connected ordinal set
X -Seg X is set
Coim (X,X) is set
X " {X} is set
(Coim (X,X)) \ {X} is Element of bool (Coim (X,X))
bool (Coim (X,X)) is set
X |_2 (X -Seg X) is Relation-like set
[:(X -Seg X),(X -Seg X):] is Relation-like set
X /\ [:(X -Seg X),(X -Seg X):] is Relation-like set
(z) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
(X |_2 (X -Seg x)) -Seg X is set
Coim ((X |_2 (X -Seg x)),X) is set
(X |_2 (X -Seg x)) " {X} is set
(Coim ((X |_2 (X -Seg x)),X)) \ {X} is Element of bool (Coim ((X |_2 (X -Seg x)),X))
bool (Coim ((X |_2 (X -Seg x)),X)) is set
field (X |_2 (X -Seg x)) is set
dom (X |_2 (X -Seg x)) is set
rng (X |_2 (X -Seg x)) is set
(dom (X |_2 (X -Seg x))) \/ (rng (X |_2 (X -Seg x))) is set
(b) |_2 z is Relation-like set
[:z,z:] is Relation-like set
(b) /\ [:z,z:] is Relation-like set
(b) -Seg z is set
Coim ((b),z) is set
{z} is set
(b) " {z} is set
(Coim ((b),z)) \ {z} is Element of bool (Coim ((b),z))
bool (Coim ((b),z)) is set
(X |_2 (X -Seg x)) |_2 ((X |_2 (X -Seg x)) -Seg X) is Relation-like set
[:((X |_2 (X -Seg x)) -Seg X),((X |_2 (X -Seg x)) -Seg X):] is Relation-like set
(X |_2 (X -Seg x)) /\ [:((X |_2 (X -Seg x)) -Seg X),((X |_2 (X -Seg x)) -Seg X):] is Relation-like set
(b) |_2 ((b) -Seg z) is Relation-like set
[:((b) -Seg z),((b) -Seg z):] is Relation-like set
(b) /\ [:((b) -Seg z),((b) -Seg z):] is Relation-like set
(b) -Seg P is set
Coim ((b),P) is set
{P} is set
(b) " {P} is set
(Coim ((b),P)) \ {P} is Element of bool (Coim ((b),P))
bool (Coim ((b),P)) is set
(b) |_2 ((b) -Seg P) is Relation-like set
[:((b) -Seg P),((b) -Seg P):] is Relation-like set
(b) /\ [:((b) -Seg P),((b) -Seg P):] is Relation-like set
[z,P] is set
{z,P} is set
{{z,P},{z}} is set
[x,X] is set
{x,X} is set
{x} is set
{{x,X},{x}} is set
X -Seg x is set
Coim (X,x) is set
X " {x} is set
(Coim (X,x)) \ {x} is Element of bool (Coim (X,x))
bool (Coim (X,x)) is set
X -Seg X is set
Coim (X,X) is set
X " {X} is set
(Coim (X,X)) \ {X} is Element of bool (Coim (X,X))
bool (Coim (X,X)) is set
X |_2 (X -Seg X) is Relation-like set
[:(X -Seg X),(X -Seg X):] is Relation-like set
X /\ [:(X -Seg X),(X -Seg X):] is Relation-like set
y is epsilon-transitive epsilon-connected ordinal set
(y) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
X |_2 (X -Seg x) is Relation-like set
[:(X -Seg x),(X -Seg x):] is Relation-like set
X /\ [:(X -Seg x),(X -Seg x):] is Relation-like set
z is epsilon-transitive epsilon-connected ordinal set
(z) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
(b) |_2 z is Relation-like set
[:z,z:] is Relation-like set
(b) /\ [:z,z:] is Relation-like set
(b) -Seg y is set
Coim ((b),y) is set
{y} is set
(b) " {y} is set
(Coim ((b),y)) \ {y} is Element of bool (Coim ((b),y))
bool (Coim ((b),y)) is set
(b) |_2 ((b) -Seg y) is Relation-like set
[:((b) -Seg y),((b) -Seg y):] is Relation-like set
(b) /\ [:((b) -Seg y),((b) -Seg y):] is Relation-like set
(X |_2 (X -Seg X)) -Seg x is set
Coim ((X |_2 (X -Seg X)),x) is set
(X |_2 (X -Seg X)) " {x} is set
(Coim ((X |_2 (X -Seg X)),x)) \ {x} is Element of bool (Coim ((X |_2 (X -Seg X)),x))
bool (Coim ((X |_2 (X -Seg X)),x)) is set
(b) -Seg z is set
Coim ((b),z) is set
{z} is set
(b) " {z} is set
(Coim ((b),z)) \ {z} is Element of bool (Coim ((b),z))
bool (Coim ((b),z)) is set
(X |_2 (X -Seg X)) |_2 ((X |_2 (X -Seg X)) -Seg x) is Relation-like set
[:((X |_2 (X -Seg X)) -Seg x),((X |_2 (X -Seg X)) -Seg x):] is Relation-like set
(X |_2 (X -Seg X)) /\ [:((X |_2 (X -Seg X)) -Seg x),((X |_2 (X -Seg X)) -Seg x):] is Relation-like set
(b) |_2 ((b) -Seg z) is Relation-like set
[:((b) -Seg z),((b) -Seg z):] is Relation-like set
(b) /\ [:((b) -Seg z),((b) -Seg z):] is Relation-like set
field (X |_2 (X -Seg X)) is set
dom (X |_2 (X -Seg X)) is set
rng (X |_2 (X -Seg X)) is set
(dom (X |_2 (X -Seg X))) \/ (rng (X |_2 (X -Seg X))) is set
[z,y] is set
{z,y} is set
{{z,y},{z}} is set
X is Relation-like set
field X is set
dom X is set
rng X is set
(dom X) \/ (rng X) is set
R is set
a is set
X -Seg a is set
Coim (X,a) is set
{a} is set
X " {a} is set
(Coim (X,a)) \ {a} is Element of bool (Coim (X,a))
bool (Coim (X,a)) is set
X |_2 (X -Seg a) is Relation-like set
[:(X -Seg a),(X -Seg a):] is Relation-like set
X /\ [:(X -Seg a),(X -Seg a):] is Relation-like set
X is set
field (X |_2 (X -Seg a)) is set
dom (X |_2 (X -Seg a)) is set
rng (X |_2 (X -Seg a)) is set
(dom (X |_2 (X -Seg a))) \/ (rng (X |_2 (X -Seg a))) is set
[X,a] is set
{X,a} is set
{X} is set
{{X,a},{X}} is set
X -Seg X is set
Coim (X,X) is set
X " {X} is set
(Coim (X,X)) \ {X} is Element of bool (Coim (X,X))
bool (Coim (X,X)) is set
X |_2 (X -Seg X) is Relation-like set
[:(X -Seg X),(X -Seg X):] is Relation-like set
X /\ [:(X -Seg X),(X -Seg X):] is Relation-like set
x is epsilon-transitive epsilon-connected ordinal set
(x) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
(X |_2 (X -Seg a)) -Seg X is set
Coim ((X |_2 (X -Seg a)),X) is set
(X |_2 (X -Seg a)) " {X} is set
(Coim ((X |_2 (X -Seg a)),X)) \ {X} is Element of bool (Coim ((X |_2 (X -Seg a)),X))
bool (Coim ((X |_2 (X -Seg a)),X)) is set
(X |_2 (X -Seg a)) |_2 ((X |_2 (X -Seg a)) -Seg X) is Relation-like set
[:((X |_2 (X -Seg a)) -Seg X),((X |_2 (X -Seg a)) -Seg X):] is Relation-like set
(X |_2 (X -Seg a)) /\ [:((X |_2 (X -Seg a)) -Seg X),((X |_2 (X -Seg a)) -Seg X):] is Relation-like set
y is epsilon-transitive epsilon-connected ordinal set
(y) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
X is epsilon-transitive epsilon-connected ordinal set
(X) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
a is set
X -Seg a is set
Coim (X,a) is set
{a} is set
X " {a} is set
(Coim (X,a)) \ {a} is Element of bool (Coim (X,a))
bool (Coim (X,a)) is set
X |_2 (X -Seg a) is Relation-like set
[:(X -Seg a),(X -Seg a):] is Relation-like set
X /\ [:(X -Seg a),(X -Seg a):] is Relation-like set
X is Relation-like set
R is epsilon-transitive epsilon-connected ordinal set
(R) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
a is epsilon-transitive epsilon-connected ordinal set
(a) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
X is set
(X) is Relation-like reflexive antisymmetric transitive set
((X)) is epsilon-transitive epsilon-connected ordinal set
R is epsilon-transitive epsilon-connected ordinal set
(R) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
(R) |_2 X is Relation-like set
[:X,X:] is Relation-like set
(R) /\ [:X,X:] is Relation-like set
a is set
(R) -Seg a is set
Coim ((R),a) is set
{a} is set
(R) " {a} is set
(Coim ((R),a)) \ {a} is Element of bool (Coim ((R),a))
bool (Coim ((R),a)) is set
(R) |_2 ((R) -Seg a) is Relation-like set
[:((R) -Seg a),((R) -Seg a):] is Relation-like set
(R) /\ [:((R) -Seg a),((R) -Seg a):] is Relation-like set
b is epsilon-transitive epsilon-connected ordinal set
(R) -Seg b is set
Coim ((R),b) is set
{b} is set
(R) " {b} is set
(Coim ((R),b)) \ {b} is Element of bool (Coim ((R),b))
bool (Coim ((R),b)) is set
(R) |_2 b is Relation-like set
[:b,b:] is Relation-like set
(R) /\ [:b,b:] is Relation-like set
(b) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
field (R) is set
dom (R) is set
rng (R) is set
(dom (R)) \/ (rng (R)) is set
X is set
R is set
a is set
[:X,R:] is Relation-like set
a /\ [:X,R:] is Relation-like set
X is set
x is set
[X,x] is set
{X,x} is set
{X} is set
{{X,x},{X}} is set
y is set
[X,y] is set
{X,y} is set
{{X,y},{X}} is set
X is Relation-like Function-like set
x is Relation-like Function-like set
dom x is set
rng x is set
y is set
x . y is set
z is set
x . z is set
[z,(x . z)] is set
{z,(x . z)} is set
{z} is set
{{z,(x . z)},{z}} is set
[y,(x . y)] is set
{y,(x . y)} is set
{y} is set
{{y,(x . y)},{y}} is set
y is set
x . y is set
[y,(x . y)] is set
{y,(x . y)} is set
{y} is set
{{y,(x . y)},{y}} is set
y is set
z is set
[y,z] is set
{y,z} is set
{y} is set
{{y,z},{y}} is set
y is set
z is set
x . z is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
y is set
z is set
[z,y] is set
{z,y} is set
{z} is set
{{z,y},{z}} is set
x . z is set
a is Relation-like Function-like set
dom a is set
rng a is set
b is Relation-like Function-like set
X is set
a . X is set
[X,(a . X)] is set
{X,(a . X)} is set
{X} is set
{{X,(a . X)},{X}} is set
X is set
a " is Relation-like Function-like set
(a ") . X is set
[((a ") . X),X] is set
{((a ") . X),X} is set
{((a ") . X)} is set
{{((a ") . X),X},{((a ") . X)}} is set
dom (a ") is set
rng (a ") is set
a . ((a ") . X) is set
X is set
x is set
[X,x] is set
{X,x} is set
{X} is set
{{X,x},{X}} is set
y is set
z is set
[y,z] is set
{y,z} is set
{y} is set
{{y,z},{y}} is set
a . X is set
a . y is set
a is Relation-like Function-like set
dom a is set
rng a is set
b is set
a is set
id a is Relation-like a -defined a -valued Function-like one-to-one set
dom (id a) is set
rng (id a) is set
a is set
b is set
X is Relation-like Function-like set
dom X is set
rng X is set
X " is Relation-like Function-like set
dom (X ") is set
rng (X ") is set
X is set
R is set
a is set
b is Relation-like Function-like set
dom b is set
rng b is set
X is Relation-like Function-like set
dom X is set
rng X is set
b * X is Relation-like Function-like set
dom (b * X) is set
rng (b * X) is set
X is set
R is Relation-like set
R |_2 X is Relation-like set
[:X,X:] is Relation-like set
R /\ [:X,X:] is Relation-like set
field (R |_2 X) is set
dom (R |_2 X) is set
rng (R |_2 X) is set
(dom (R |_2 X)) \/ (rng (R |_2 X)) is set
a is set
b is set
[a,b] is set
{a,b} is set
{a} is set
{{a,b},{a}} is set
[b,a] is set
{b,a} is set
{b} is set
{{b,a},{b}} is set
a is set
b is set
R -Seg b is set
Coim (R,b) is set
{b} is set
R " {b} is set
(Coim (R,b)) \ {b} is Element of bool (Coim (R,b))
bool (Coim (R,b)) is set
(R |_2 X) -Seg b is set
Coim ((R |_2 X),b) is set
(R |_2 X) " {b} is set
(Coim ((R |_2 X),b)) \ {b} is Element of bool (Coim ((R |_2 X),b))
bool (Coim ((R |_2 X),b)) is set
X is set
[X,b] is set
{X,b} is set
{X} is set
{{X,b},{X}} is set
a is set
b is set
[a,b] is set
{a,b} is set
{a} is set
{{a,b},{a}} is set
X is set
[b,X] is set
{b,X} is set
{b} is set
{{b,X},{b}} is set
[a,X] is set
{a,X} is set
{{a,X},{a}} is set
a is set
b is set
[a,b] is set
{a,b} is set
{a} is set
{{a,b},{a}} is set
[b,a] is set
{b,a} is set
{b} is set
{{b,a},{b}} is set
a is set
[a,a] is set
{a,a} is set
{a} is set
{{a,a},{a}} is set
a is set
[a,a] is set
{a,a} is set
{a} is set
{{a,a},{a}} is set
X is set
R is Relation-like set
field R is set
dom R is set
rng R is set
(dom R) \/ (rng R) is set
a is Relation-like Function-like set
dom a is set
rng a is set
b is Relation-like set
field b is set
dom b is set
rng b is set
(dom b) \/ (rng b) is set
X is set
x is set
[x,X] is set
{x,X} is set
{x} is set
{{x,X},{x}} is set
x is set
[X,x] is set
{X,x} is set
{X} is set
{{X,x},{X}} is set
X is set
a . X is set
[(a . X),(a . X)] is set
{(a . X),(a . X)} is set
{(a . X)} is set
{{(a . X),(a . X)},{(a . X)}} is set
[X,X] is set
{X,X} is set
{X} is set
{{X,X},{X}} is set
X is set
a . X is set
x is set
[X,x] is set
{X,x} is set
{X} is set
{{X,x},{X}} is set
a . x is set
[(a . X),(a . x)] is set
{(a . X),(a . x)} is set
{(a . X)} is set
{{(a . X),(a . x)},{(a . X)}} is set
a " is Relation-like Function-like set
X is set
R is set
a is set
b is set
x is set
X is epsilon-transitive epsilon-connected ordinal set
y is epsilon-transitive epsilon-connected ordinal set
b is epsilon-transitive epsilon-connected ordinal set
X is set
(b) is Relation-like reflexive antisymmetric connected transitive well_founded well-ordering set
field (b) is set
dom (b) is set
rng (b) is set
(dom (b)) \/ (rng (b)) is set
X is Relation-like set
x is Relation-like Function-like set
dom x is set
rng x is set
y is set
z is set
x . z is set
{z} is set
z is set
y is set
x . y is set
z is set
x . z is set
{y} is set
{z} is set
X |_2 R is Relation-like set
[:R,R:] is Relation-like set
X /\ [:R,R:] is Relation-like set
field (X |_2 R) is set
dom (X |_2 R) is set
rng (X |_2 R) is set
(dom (X |_2 R)) \/ (rng (X |_2 R)) is set
(X |_2 R) |_2 (rng x) is Relation-like set
[:(rng x),(rng x):] is Relation-like set
(X |_2 R) /\ [:(rng x),(rng x):] is Relation-like set
field ((X |_2 R) |_2 (rng x)) is set
dom ((X |_2 R) |_2 (rng x)) is set
rng ((X |_2 R) |_2 (rng x)) is set
(dom ((X |_2 R) |_2 (rng x))) \/ (rng ((X |_2 R) |_2 (rng x))) is set
X is non empty set
union X is set
R is Relation-like set
a is set
b is set
X is set
[b,X] is set
{b,X} is set
{b} is set
{{b,X},{b}} is set
[X,b] is set
{X,b} is set
{X} is set
{{X,b},{X}} is set
a is set
b is set
R -Seg b is set
Coim (R,b) is set
{b} is set
R " {b} is set
(Coim (R,b)) \ {b} is Element of bool (Coim (R,b))
bool (Coim (R,b)) is set
X is set
[b,X] is set
{b,X} is set
{{b,X},{b}} is set
[X,b] is set
{X,b} is set
{X} is set
{{X,b},{X}} is set
a is Relation-like Function-like set
dom a is set
rng a is set
b is set
X is set
b /\ X is set
a . X is set
x is set
{x} is set
y is set
z is set
a . z is set
X /\ z is set
y is set
X is set
(X) is Relation-like reflexive antisymmetric transitive set
field (X) is set
dom (X) is set
rng (X) is set
(dom (X)) \/ (rng (X)) is set
X is set
(X) is Relation-like reflexive antisymmetric transitive set
field (X) is set
dom (X) is set
rng (X) is set
(dom (X)) \/ (rng (X)) is set
X is set
(X) is Relation-like reflexive antisymmetric transitive set
field (X) is set
dom (X) is set
rng (X) is set
(dom (X)) \/ (rng (X)) is set
({}) is Relation-like reflexive antisymmetric transitive set
X is set
R is set
[X,R] is set
{X,R} is set
{X} is set
{{X,R},{X}} is set
X is non empty set
(X) is Relation-like reflexive antisymmetric transitive set
the Element of X is Element of X
[ the Element of X, the Element of X] is set
{ the Element of X, the Element of X} is set
{ the Element of X} is set
{{ the Element of X, the Element of X},{ the Element of X}} is set
X is set
{X} is set
({X}) is Relation-like reflexive antisymmetric transitive set
[X,X] is set
{X,X} is set
{{X,X},{X}} is set
{[X,X]} is Relation-like Function-like set
R is set
a is set
[R,a] is set
{R,a} is set
{R} is set
{{R,a},{R}} is set
field {[X,X]} is set
dom {[X,X]} is set
rng {[X,X]} is set
(dom {[X,X]}) \/ (rng {[X,X]}) is set
X is set
(X) is Relation-like reflexive antisymmetric transitive set
[:X,X:] is Relation-like set
a is set
b is set
[a,b] is set
{a,b} is set
{a} is set
{{a,b},{a}} is set
field (X) is set
dom (X) is set
rng (X) is set
(dom (X)) \/ (rng (X)) is set