omega is epsilon-transitive epsilon-connected ordinal non empty set
{} is Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty trivial finite V39() set
the Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty trivial finite V39() set is Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty trivial finite V39() set
the epsilon-transitive epsilon-connected ordinal set is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
f is set
y is epsilon-transitive epsilon-connected ordinal set
f is set
x is epsilon-transitive epsilon-connected ordinal set
f is set
x is Relation-like set
x |_2 f is Relation-like set
order_type_of (x |_2 f) is epsilon-transitive epsilon-connected ordinal set
y is epsilon-transitive epsilon-connected ordinal set
RelIncl y is Relation-like set
y1 is Relation-like Function-like set
dom y1 is set
rng y1 is set
field (x |_2 f) is set
dom (x |_2 f) is set
rng (x |_2 f) is set
(dom (x |_2 f)) \/ (rng (x |_2 f)) is set
field (RelIncl y) is set
dom (RelIncl y) is set
rng (RelIncl y) is set
(dom (RelIncl y)) \/ (rng (RelIncl y)) is set
f is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal set
y is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal () set
y is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal () set
f is set
x is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal () set
f is set
x is epsilon-transitive epsilon-connected ordinal () set
f is set
x is epsilon-transitive epsilon-connected ordinal set
f is Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty trivial finite V39() () set
(f) is epsilon-transitive epsilon-connected ordinal () set
f is non empty set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is Relation-like Function-like set
dom x is set
rng x is set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is Relation-like set
field f is set
dom f is set
rng f is set
(dom f) \/ (rng f) is set
order_type_of f is epsilon-transitive epsilon-connected ordinal set
RelIncl (order_type_of f) is Relation-like set
x is Relation-like Function-like set
dom x is set
rng x is set
field (RelIncl (order_type_of f)) is set
dom (RelIncl (order_type_of f)) is set
rng (RelIncl (order_type_of f)) is set
(dom (RelIncl (order_type_of f))) \/ (rng (RelIncl (order_type_of f))) is set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal () set
RelIncl f is Relation-like set
order_type_of (RelIncl f) is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
field (RelIncl f) is set
dom (RelIncl f) is set
rng (RelIncl f) is set
(dom (RelIncl f)) \/ (rng (RelIncl f)) is set
y is epsilon-transitive epsilon-connected ordinal set
y1 is epsilon-transitive epsilon-connected ordinal set
y1 is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal set
f is set
x is epsilon-transitive epsilon-connected ordinal () set
(f) is epsilon-transitive epsilon-connected ordinal () set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is Relation-like Function-like set
dom f is set
rng f is set
y is Relation-like Function-like set
dom y is set
rng y is set
y " is Relation-like Function-like set
f * (y ") is Relation-like Function-like set
y1 is Relation-like Function-like set
dom y1 is set
rng y1 is set
dom (y ") is set
rng (y ") is set
f is Relation-like Function-like set
dom f is set
rng f is set
y is Relation-like Function-like set
dom y is set
rng y is set
f * y is Relation-like Function-like set
rng (f * y) is set
dom (f * y) is set
((rng (f * y))) is epsilon-transitive epsilon-connected ordinal () set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is set
(x) is epsilon-transitive epsilon-connected ordinal () set
id f is Relation-like Function-like one-to-one set
dom (id f) is set
rng (id f) is set
f is Relation-like Function-like set
dom f is set
rng f is set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is Relation-like Function-like set
dom f is set
rng f is set
f " is Relation-like Function-like set
y is set
(f ") . y is set
y1 is set
y2 is set
y is set
y1 is set
(f ") . y is set
y2 is set
y is Relation-like Function-like set
dom y is set
rng y is set
y1 is set
f . y1 is set
(f ") . (f . y1) is set
y . (f . y1) is set
f is Relation-like Function-like set
dom f is set
rng f is set
y is Relation-like Function-like set
dom y is set
rng y is set
y1 is non empty set
y2 is set
h is set
y . h is set
{h} is non empty trivial finite set
f " {h} is set
x is set
f . x is set
y2 is Relation-like Function-like set
dom y2 is set
y * y2 is Relation-like Function-like set
dom (y * y2) is set
h is set
(y * y2) . h is set
x is set
(y * y2) . x is set
y . x is set
{x} is non empty trivial finite set
f " {x} is set
y2 . (f " {x}) is set
f . (y2 . (f " {x})) is set
y . h is set
{h} is non empty trivial finite set
f " {h} is set
y2 . (f " {h}) is set
f . (y2 . (f " {h})) is set
y2 . (y . h) is set
y2 . (y . x) is set
rng (y * y2) is set
h is set
x is set
(y * y2) . x is set
y . x is set
y2 . (y . x) is set
{x} is non empty trivial finite set
f " {x} is set
f is set
bool f is non empty set
x is Relation-like Function-like set
dom x is set
rng x is set
f is set
y is set
y is set
x . y is set
y1 is set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
bool f is non empty set
((bool f)) is epsilon-transitive epsilon-connected ordinal non empty () set
x is Relation-like Function-like set
dom x is set
rng x is set
f is set
y is set
x . y is set
{y} is non empty trivial finite set
y1 is set
f is set
x . f is set
y is set
x . y is set
{f} is non empty trivial finite set
{y} is non empty trivial finite set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
bool f is non empty set
((bool f)) is epsilon-transitive epsilon-connected ordinal non empty () set
x is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal () set
y is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal () set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
({}) is Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty trivial finite V39() () set
(f) is epsilon-transitive epsilon-connected ordinal () set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is set
(x) is epsilon-transitive epsilon-connected ordinal () set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal () set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is set
(x) is epsilon-transitive epsilon-connected ordinal () set
(f) is epsilon-transitive epsilon-connected ordinal () set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal set
(f) is epsilon-transitive epsilon-connected ordinal () set
((f)) is epsilon-transitive epsilon-connected ordinal () set
(f) is epsilon-transitive epsilon-connected ordinal () set
((f)) is epsilon-transitive epsilon-connected ordinal () set
((f)) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal set
succ f is epsilon-transitive epsilon-connected ordinal non empty set
{f} is non empty trivial finite set
f \/ {f} is non empty set
(omega) is epsilon-transitive epsilon-connected ordinal non empty () set
x is set
f is epsilon-transitive epsilon-connected ordinal set
(f) is set
succ f is epsilon-transitive epsilon-connected ordinal non empty set
{f} is non empty trivial finite set
f \/ {f} is non empty set
y is set
y1 is Relation-like Function-like T-Sequence-like set
last y1 is set
dom y1 is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
succ f is epsilon-transitive epsilon-connected ordinal non empty set
{f} is non empty trivial finite set
f \/ {f} is non empty set
y1 . {} is set
(f) is set
({}) is set
f is epsilon-transitive epsilon-connected ordinal set
(f) is set
x is Relation-like Function-like T-Sequence-like set
dom x is epsilon-transitive epsilon-connected ordinal set
sup x is epsilon-transitive epsilon-connected ordinal set
((sup x)) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal set
(f) is set
x is Relation-like Function-like T-Sequence-like set
dom x is epsilon-transitive epsilon-connected ordinal set
sup x is epsilon-transitive epsilon-connected ordinal set
((sup x)) is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal set
succ x is epsilon-transitive epsilon-connected ordinal non empty set
{x} is non empty trivial finite set
x \/ {x} is non empty set
(x) is set
{(x)} is non empty trivial finite set
union {(x)} is set
((union {(x)})) is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal set
succ x is epsilon-transitive epsilon-connected ordinal non empty set
{x} is non empty trivial finite set
x \/ {x} is non empty set
f is epsilon-transitive epsilon-connected ordinal set
succ f is epsilon-transitive epsilon-connected ordinal non empty set
{f} is non empty trivial finite set
f \/ {f} is non empty set
((succ f)) is epsilon-transitive epsilon-connected ordinal () set
(f) is epsilon-transitive epsilon-connected ordinal () set
((f)) is epsilon-transitive epsilon-connected ordinal () set
{(f)} is non empty trivial finite set
union {(f)} is set
((union {(f)})) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal set
x is Relation-like Function-like T-Sequence-like set
dom x is epsilon-transitive epsilon-connected ordinal set
(f) is epsilon-transitive epsilon-connected ordinal () set
sup x is epsilon-transitive epsilon-connected ordinal set
((sup x)) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal set
(f) is epsilon-transitive epsilon-connected ordinal () set
succ f is epsilon-transitive epsilon-connected ordinal non empty set
{f} is non empty trivial finite set
f \/ {f} is non empty set
((succ f)) is epsilon-transitive epsilon-connected ordinal () set
y is epsilon-transitive epsilon-connected ordinal set
(y) is epsilon-transitive epsilon-connected ordinal () set
((f)) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal set
(f) is epsilon-transitive epsilon-connected ordinal () set
y is epsilon-transitive epsilon-connected ordinal set
(y) is epsilon-transitive epsilon-connected ordinal () set
y1 is Relation-like Function-like T-Sequence-like set
dom y1 is epsilon-transitive epsilon-connected ordinal set
succ y is epsilon-transitive epsilon-connected ordinal non empty set
{y} is non empty trivial finite set
y \/ {y} is non empty set
y1 . (succ y) is set
rng y1 is set
((succ y)) is epsilon-transitive epsilon-connected ordinal () set
sup (rng y1) is epsilon-transitive epsilon-connected ordinal set
sup y1 is epsilon-transitive epsilon-connected ordinal set
(((succ y))) is epsilon-transitive epsilon-connected ordinal () set
((y)) is epsilon-transitive epsilon-connected ordinal () set
((sup y1)) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal set
(f) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is set
x is set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
(f) is epsilon-transitive epsilon-connected ordinal () set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is set
bool f is non empty set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is set
(x) is epsilon-transitive epsilon-connected ordinal () set
((bool f)) is epsilon-transitive epsilon-connected ordinal non empty () set
f is set
x is Relation-like Function-like set
dom x is set
rng x is set
({}) is Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty trivial finite V39() () set
f is set
x is set
{x} is non empty trivial finite set
f is Relation-like Function-like set
dom f is set
rng f is set
f . x is set
{(f . x)} is non empty trivial finite set
f is set
{f} is non empty trivial finite set
[:f,{x}:] is set
bool [:f,{x}:] is non empty set
f --> x is Relation-like f -defined Function-like constant V23(f) V27(f,{x}) Element of bool [:f,{x}:]
y is Relation-like f -defined Function-like constant V23(f) V27(f,{x}) Element of bool [:f,{x}:]
dom y is set
rng y is trivial finite set
y1 is set
y . y1 is set
y2 is set
y . y2 is set
y1 is set
y . f is set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is set
{x} is non empty trivial finite set
({x}) is epsilon-transitive epsilon-connected ordinal non empty () set
f is set
{f} is non empty trivial finite set
1 is epsilon-transitive epsilon-connected ordinal natural non empty Element of omega
f is set
{f} is non empty trivial finite set
({f}) is epsilon-transitive epsilon-connected ordinal non empty () set
succ {} is epsilon-transitive epsilon-connected ordinal natural non empty set
{{}} is non empty trivial finite V39() set
{} \/ {{}} is non empty finite V39() set
x is epsilon-transitive epsilon-connected ordinal natural non empty Element of omega
f is epsilon-transitive epsilon-connected ordinal set
y is set
{y} is non empty trivial finite set
x is epsilon-transitive epsilon-connected ordinal () set
f is set
x is set
f \/ x is set
f is set
y is set
f \/ y is set
f /\ x is set
f /\ y is set
y1 is Relation-like Function-like set
dom y1 is set
rng y1 is set
y2 is Relation-like Function-like set
dom y2 is set
rng y2 is set
h is set
y1 . h is set
y2 . h is set
h is set
x is set
y1 . h is set
y2 . h is set
y is set
h is Relation-like Function-like set
dom h is set
rng h is set
x is set
h . x is set
y is set
h . y is set
y1 . y is set
y2 . y is set
y1 . x is set
y2 . x is set
x is set
y is set
h . y is set
y1 . y is set
y2 . y is set
x is set
y is set
y2 . y is set
h . y is set
y1 . y is set
y is set
y1 . y is set
h . y is set
y2 . y is set
f is set
{f} is non empty trivial finite set
x is set
x \ {f} is Element of bool x
bool x is non empty set
f is set
{f} is non empty trivial finite set
x \ {f} is Element of bool x
y is set
y1 is set
y2 is set
y is set
y1 is set
y2 is set
y is Relation-like Function-like set
dom y is set
rng y is set
y1 is set
y . y1 is set
y2 is set
y . y2 is set
y1 is set
y2 is set
y . y2 is set
y1 is set
y . y1 is set
y . f is set
f is set
x is Relation-like Function-like set
dom x is set
x .: f is set
x | f is Relation-like Function-like set
f is Relation-like Function-like set
dom f is set
rng f is set
f is set
x is set
f is set
{f} is non empty trivial finite set
f \ {f} is Element of bool f
bool f is non empty set
y is set
{y} is non empty trivial finite set
x \ {y} is Element of bool x
bool x is non empty set
y1 is Relation-like Function-like set
dom y1 is set
rng y1 is set
y1 .: (f \ {f}) is set
y1 . f is set
{(y1 . f)} is non empty trivial finite set
x \ {(y1 . f)} is Element of bool x
y1 .: f is set
Im (y1,f) is set
y1 .: {f} is finite set
(y1 .: f) \ (Im (y1,f)) is Element of bool (y1 .: f)
bool (y1 .: f) is non empty set
x \ (Im (y1,f)) is Element of bool x
f is set
succ f is non empty set
{f} is non empty trivial finite set
f \/ {f} is non empty set
x is set
succ x is non empty set
{x} is non empty trivial finite set
x \/ {x} is non empty set
(succ f) \ {f} is Element of bool (succ f)
bool (succ f) is non empty set
(succ x) \ {x} is Element of bool (succ x)
bool (succ x) is non empty set
f is epsilon-transitive epsilon-connected ordinal natural set
x is epsilon-transitive epsilon-connected ordinal natural set
f is epsilon-transitive epsilon-connected ordinal natural set
succ f is epsilon-transitive epsilon-connected ordinal natural non empty set
{f} is non empty trivial finite set
f \/ {f} is non empty set
succ x is epsilon-transitive epsilon-connected ordinal natural non empty set
{x} is non empty trivial finite set
x \/ {x} is non empty set
f is epsilon-transitive epsilon-connected ordinal natural set
x is epsilon-transitive epsilon-connected ordinal natural set
f is epsilon-transitive epsilon-connected ordinal natural set
succ f is epsilon-transitive epsilon-connected ordinal natural non empty set
{f} is non empty trivial finite set
f \/ {f} is non empty set
y is epsilon-transitive epsilon-connected ordinal natural set
y1 is epsilon-transitive epsilon-connected ordinal natural set
succ y1 is epsilon-transitive epsilon-connected ordinal natural non empty set
{y1} is non empty trivial finite set
y1 \/ {y1} is non empty set
f is epsilon-transitive epsilon-connected ordinal natural set
f is set
x is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
y is epsilon-transitive epsilon-connected ordinal natural set
y1 is epsilon-transitive epsilon-connected ordinal natural set
f is set
f is set
x is set
f is Relation-like Function-like set
dom f is set
rng f is set
y is Relation-like Function-like set
rng y is set
dom y is set
y * f is Relation-like Function-like set
rng (y * f) is set
dom (y * f) is set
f is epsilon-transitive epsilon-connected ordinal natural () set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal natural () Element of omega
id x is Relation-like Function-like one-to-one set
rng (id x) is set
dom (id x) is set
f is epsilon-transitive epsilon-connected ordinal natural () set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal natural () set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal natural () Element of omega
(f) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal natural () set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal natural () set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal natural () set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal natural () set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is set
x is set
{x} is non empty trivial finite set
f is set
f \/ {x} is non empty set
y is epsilon-transitive epsilon-connected ordinal natural () set
f /\ {x} is finite set
the Element of f /\ {x} is Element of f /\ {x}
{y} is non empty trivial finite set
y1 is set
succ y is epsilon-transitive epsilon-connected ordinal natural non empty () set
y \/ {y} is non empty set
y1 is epsilon-transitive epsilon-connected ordinal natural () set
y2 is epsilon-transitive epsilon-connected ordinal natural () set
f is epsilon-transitive epsilon-connected ordinal natural () set
(f) is epsilon-transitive epsilon-connected ordinal () set
((f)) is epsilon-transitive epsilon-connected ordinal () set
succ f is epsilon-transitive epsilon-connected ordinal natural non empty () set
{f} is non empty trivial finite set
f \/ {f} is non empty set
((succ f)) is epsilon-transitive epsilon-connected ordinal non empty () set
((f)) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal natural () set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal natural () set
succ f is epsilon-transitive epsilon-connected ordinal natural non empty () set
{f} is non empty trivial finite set
f \/ {f} is non empty set
f is finite set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal natural () set
f is epsilon-transitive epsilon-connected ordinal natural () Element of omega
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is finite set
(x) is epsilon-transitive epsilon-connected ordinal natural () Element of omega
((x)) is epsilon-transitive epsilon-connected ordinal () set
((x)) is epsilon-transitive epsilon-connected ordinal natural non empty () Element of omega
{(x)} is non empty trivial finite set
(x) \/ {(x)} is non empty set
(((x))) is epsilon-transitive epsilon-connected ordinal non empty () set
((x)) is epsilon-transitive epsilon-connected ordinal () set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal () set
y is epsilon-transitive epsilon-connected ordinal () set
(y) is epsilon-transitive epsilon-connected ordinal () set
y is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal () set
x is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal () set
y is epsilon-transitive epsilon-connected ordinal () set
f is set
x is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal natural () Element of omega
(f) is epsilon-transitive epsilon-connected ordinal natural non empty () Element of omega
{f} is non empty trivial finite set
f \/ {f} is non empty set
((f)) is epsilon-transitive epsilon-connected ordinal non empty () set
f is set
f is epsilon-transitive epsilon-connected ordinal () set
(f) is epsilon-transitive epsilon-connected ordinal () set
succ f is epsilon-transitive epsilon-connected ordinal non empty set
{f} is non empty trivial finite set
f \/ {f} is non empty set
x is epsilon-transitive epsilon-connected ordinal natural () Element of omega
(x) is epsilon-transitive epsilon-connected ordinal natural non empty () Element of omega
{x} is non empty trivial finite set
x \/ {x} is non empty set
((x)) is epsilon-transitive epsilon-connected ordinal non empty () set
(x) is epsilon-transitive epsilon-connected ordinal () set
((x)) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal natural () Element of omega
the epsilon-transitive epsilon-connected ordinal natural finite () Element of omega is epsilon-transitive epsilon-connected ordinal natural finite () Element of omega
f is epsilon-transitive epsilon-connected ordinal finite () set
(f) is epsilon-transitive epsilon-connected ordinal natural finite () Element of omega
f is finite set
(f) is epsilon-transitive epsilon-connected ordinal natural finite () Element of omega
f is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal natural () set
f is epsilon-transitive epsilon-connected ordinal natural () set
(f) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{f} is non empty trivial finite set
f \/ {f} is non empty set
y is epsilon-transitive epsilon-connected ordinal set
(f) \ {f} is finite Element of bool (f)
bool (f) is non empty finite V39() set
(y) is epsilon-transitive epsilon-connected ordinal () set
((f)) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
y1 is epsilon-transitive epsilon-connected ordinal set
succ y1 is epsilon-transitive epsilon-connected ordinal non empty set
{y1} is non empty trivial finite set
y1 \/ {y1} is non empty set
y \ {y1} is Element of bool y
bool y is non empty set
f is epsilon-transitive epsilon-connected ordinal set
f is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal natural () set
f is non empty non trivial non finite set
(f) is epsilon-transitive epsilon-connected ordinal non empty () set
{{}} is non empty trivial finite V39() set
({}) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{} \/ {{}} is non empty finite V39() set
2 is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{{},1} is non empty finite V39() set
(1) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{1} is non empty trivial finite V39() set
1 \/ {1} is non empty finite set
3 is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{{},1,2} is non empty finite set
(2) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{2} is non empty trivial finite V39() set
2 \/ {2} is non empty finite set
4 is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{{},1,2,3} is non empty finite set
(3) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{3} is non empty trivial finite V39() set
3 \/ {3} is non empty finite set
5 is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{{},1,2,3,4} is non empty finite set
(4) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{4} is non empty trivial finite V39() set
4 \/ {4} is non empty finite set
6 is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{{},1,2,3,4,5} is non empty finite set
(5) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{5} is non empty trivial finite V39() set
5 \/ {5} is non empty finite set
7 is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{{},1,2,3,4,5,6} is non empty finite set
(6) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{6} is non empty trivial finite V39() set
6 \/ {6} is non empty finite set
8 is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{{},1,2,3,4,5,6,7} is non empty finite set
(7) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{7} is non empty trivial finite V39() set
7 \/ {7} is non empty finite set
9 is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{{},1,2,3,4,5,6,7,8} is non empty set
(8) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{8} is non empty trivial finite V39() set
8 \/ {8} is non empty finite set
10 is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{{},1,2,3,4,5,6,7,8,9} is non empty set
(9) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{9} is non empty trivial finite V39() set
9 \/ {9} is non empty finite set
f is Relation-like Function-like set
dom f is set
rng f is set
f is epsilon-transitive epsilon-connected ordinal natural () set
f is epsilon-transitive epsilon-connected ordinal natural () set
(f) is set
bool omega is non empty set
f is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal natural () set
f is epsilon-transitive epsilon-connected ordinal set
x is epsilon-transitive epsilon-connected ordinal set
f is set
f is non empty non trivial non finite set
bool f is non empty set
x is set
union x is set
f is set
y is set
{f} is non empty trivial finite set
f is set
y is set
{y} is non empty trivial finite set
f is set
x is non empty set
[:f,x:] is non empty set
f is Relation-like Function-like set
dom f is set
rng f is set
y is set
y1 is set
f . y1 is set
y1 `1 is set
the Element of x is Element of x
[y, the Element of x] is non empty V24() set
{y, the Element of x} is non empty finite set
{y} is non empty trivial finite set
{{y, the Element of x},{y}} is non empty finite V39() set
f . [y, the Element of x] is set
[y, the Element of x] `1 is set
f .: [:f,x:] is set
[:x,f:] is non empty set
f is Relation-like Function-like set
dom f is set
rng f is set
y is set
y1 is set
f . y1 is set
y1 `2 is set
the Element of x is Element of x
[ the Element of x,y] is non empty V24() set
{ the Element of x,y} is non empty finite set
{ the Element of x} is non empty trivial finite set
{{ the Element of x,y},{ the Element of x}} is non empty finite V39() set
[ the Element of x,y] `2 is set
f . [ the Element of x,y] is set
f .: [:x,f:] is set
f is non empty non trivial non finite set
bool f is non empty non trivial non finite set
f is set
f is Relation-like Function-like set
(f) is epsilon-transitive epsilon-connected ordinal () set
dom f is set
((dom f)) is epsilon-transitive epsilon-connected ordinal () set
x is Relation-like Function-like set
dom x is set
rng x is set
f is set
x . f is set
y is set
x . y is set
f . f is set
[f,(f . f)] is non empty V24() set
{f,(f . f)} is non empty finite set
{f} is non empty trivial finite set
{{f,(f . f)},{f}} is non empty finite V39() set
f . y is set
[y,(f . y)] is non empty V24() set
{y,(f . y)} is non empty finite set
{y} is non empty trivial finite set
{{y,(f . y)},{y}} is non empty finite V39() set
f is set
y is set
x . y is set
f . y is set
[y,(f . y)] is non empty V24() set
{y,(f . y)} is non empty finite set
{y} is non empty trivial finite set
{{y,(f . y)},{y}} is non empty finite V39() set
f is set
y is set
[f,y] is non empty V24() set
{f,y} is non empty finite set
{f} is non empty trivial finite set
{{f,y},{f}} is non empty finite V39() set
f . f is set
x . f is set
f is finite set
RelIncl f is Relation-like set
[:f,f:] is finite set
f is set
RelIncl f is Relation-like set
f is Relation-like finite set
field f is finite set
dom f is finite set
rng f is finite set
(dom f) \/ (rng f) is finite set
f is set
x is epsilon-transitive epsilon-connected ordinal natural finite () set
x --> f is Relation-like x -defined Function-like constant V23(x) V27(x,{f}) finite Element of bool [:x,{f}:]
{f} is non empty trivial finite set
[:x,{f}:] is finite set
bool [:x,{f}:] is non empty finite V39() set
((x --> f)) is epsilon-transitive epsilon-connected ordinal natural finite () set
dom (x --> f) is finite set
(x) is epsilon-transitive epsilon-connected ordinal natural finite () Element of omega
f is epsilon-transitive epsilon-connected ordinal () set
(f) is epsilon-transitive epsilon-connected ordinal () set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
f is set
{f} is non empty trivial finite set
({}) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
{} \/ {{}} is non empty finite V39() set
({f}) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
f is epsilon-transitive epsilon-connected ordinal () set
{{{}}} is non empty trivial finite V39() (1) set
[:f,{{{}}}:] is set
bool [:f,{{{}}}:] is non empty set
f --> {{}} is Relation-like non-empty f -defined Function-like constant V23(f) V27(f,{{{}}}) Element of bool [:f,{{{}}}:]
x is Relation-like non-empty f -defined Function-like constant V23(f) V27(f,{{{}}}) Element of bool [:f,{{{}}}:]
dom x is set
((dom x)) is epsilon-transitive epsilon-connected ordinal () set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is epsilon-transitive epsilon-connected ordinal () set
x is Relation-like Function-like (f) set
dom x is set
(x) is epsilon-transitive epsilon-connected ordinal () set
((dom x)) is epsilon-transitive epsilon-connected ordinal () set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
({{}}) is epsilon-transitive epsilon-connected ordinal natural non empty finite () Element of omega
x is set
{x} is non empty trivial finite (1) set
f is set
x is set
{x} is non empty trivial finite (1) set
f is non empty set
bool f is non empty set
the non empty trivial finite (1) Element of bool f is non empty trivial finite (1) Element of bool f
f is non empty set
bool f is non empty set
x is non empty trivial finite (1) Element of bool f
f is set
{f} is non empty trivial finite (1) set
y is Element of f
{y} is non empty trivial finite (1) set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is set
(x) is epsilon-transitive epsilon-connected ordinal () set
f is Relation-like Function-like set
dom f is set
rng f is set
f .: x is set
f is Relation-like Function-like set
f .: x is set
dom f is set
y is Relation-like Function-like set
dom y is set
rng y is set
y1 is set
y2 is set
f . y2 is set
y . y2 is set
x is Relation-like Function-like set
f is set
x .: f is set
((x .: f)) is epsilon-transitive epsilon-connected ordinal () set
(f) is epsilon-transitive epsilon-connected ordinal () set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is set
(x) is epsilon-transitive epsilon-connected ordinal () set
x \ f is Element of bool x
bool x is non empty set
f is set
(f) is epsilon-transitive epsilon-connected ordinal () set
x is set
{x} is non empty trivial finite (1) set
[:f,{x}:] is set
([:f,{x}:]) is epsilon-transitive epsilon-connected ordinal () set
f is Relation-like Function-like set
dom f is set
rng f is set
y is set
f . y is set
y1 is set
f . y1 is set
[y,x] is non empty V24() set
{y,x} is non empty finite set
{y} is non empty trivial finite (1) set
{{y,x},{y}} is non empty finite V39() set
[y,x] `1 is set
[y1,x] is non empty V24() set
{y1,x} is non empty finite set
{y1} is non empty trivial finite (1) set
{{y1,x},{y1}} is non empty finite V39() set
y is set
y1 is set
f . y1 is set
[y1,x] is non empty V24() set
{y1,x} is non empty finite set
{y1} is non empty trivial finite (1) set
{{y1,x},{y1}} is non empty finite V39() set
y is set
y1 is set
y2 is set
[y1,y2] is non empty V24() set
{y1,y2} is non empty finite set
{y1} is non empty trivial finite (1) set
{{y1,y2},{y1}} is non empty finite V39() set
f . y1 is set
f is Relation-like Function-like set
dom f is set
((dom f)) is epsilon-transitive epsilon-connected ordinal () set
rng f is set
((rng f)) is epsilon-transitive epsilon-connected ordinal () set
f .: (dom f) is set