:: CARD_1 semantic presentation

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