:: CLASSES1 semantic presentation

omega is non empty epsilon-transitive epsilon-connected ordinal set

bool omega is non empty set

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural set

f is set

g is set

bool g is non empty Element of bool (bool g)

bool g is non empty set

bool (bool g) is non empty set

h is set

meet h is set

I is set

I is set

c

y is set

I is set

bool I is non empty Element of bool (bool I)

bool I is non empty set

bool (bool I) is non empty set

c

I is set

c

I is set

(meet h) /\ I is set

c

y is set

c

bool c

bool c

bool (bool c

c

c

g is set

h is set

f is set

(f) is set

f is set

card f is cardinal set

g is set

bool g is non empty Element of bool (bool g)

bool g is non empty set

bool (bool g) is non empty set

g is set

card g is cardinal set

g is set

card g is cardinal set

g is set

card g is cardinal set

f is set

(f) is non empty set

f is set

g is set

(g) is non empty set

h is set

f is set

bool f is non empty Element of bool (bool f)

bool f is non empty set

bool (bool f) is non empty set

g is set

(g) is non empty set

f is set

g is set

(g) is non empty set

f is set

card f is cardinal set

g is set

(g) is non empty set

card (g) is cardinal set

g is epsilon-transitive epsilon-connected ordinal set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

f is set

{f} is non empty set

(f) is non empty set

{ b

( b

{ (bool b

{ b

( b

f is set

(f) is non empty set

{ b

( b

{ (bool b

{ b

( b

{f} is non empty set

h is set

g is epsilon-transitive epsilon-connected ordinal set

(f,g) is set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

I is set

c

last c

dom c

p is epsilon-transitive epsilon-connected ordinal set

succ p is non empty epsilon-transitive epsilon-connected ordinal set

{p} is non empty set

p \/ {p} is non empty set

c

(f,p) is set

(f,{}) is set

g is epsilon-transitive epsilon-connected ordinal set

(f,g) is set

h is Relation-like Function-like T-Sequence-like set

dom h is epsilon-transitive epsilon-connected ordinal set

rng h is set

union (rng h) is set

(union (rng h)) /\ (f) is set

f is set

g is epsilon-transitive epsilon-connected ordinal set

(f,g) is set

(f) is non empty set

bool (f) is non empty set

{f} is non empty set

h is set

(f,{}) is set

h is epsilon-transitive epsilon-connected ordinal set

(f,h) is set

succ h is non empty epsilon-transitive epsilon-connected ordinal set

{h} is non empty set

h \/ {h} is non empty set

(f,(succ h)) is set

c

p is Element of bool (f)

{ b

( b

{ (bool b

{ b

( b

bool p is non empty set

bool p is non empty Element of bool (bool p)

bool (bool p) is non empty set

(bool p) /\ (f) is Element of bool (bool p)

( { b

( b

y is Element of (f)

f is Element of (f)

y is Element of (f)

bool y is non empty Element of bool (bool y)

bool y is non empty set

bool (bool y) is non empty set

h is epsilon-transitive epsilon-connected ordinal set

(f,h) is set

p is Relation-like Function-like T-Sequence-like set

dom p is epsilon-transitive epsilon-connected ordinal set

rng p is set

union (rng p) is set

(union (rng p)) /\ (f) is set

f is set

(f,{}) is Element of bool (f)

(f) is non empty set

bool (f) is non empty set

{f} is non empty set

f is set

g is epsilon-transitive epsilon-connected ordinal set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

(f,(succ g)) is Element of bool (f)

(f) is non empty set

bool (f) is non empty set

(f,g) is Element of bool (f)

{ b

( b

{ (bool b

{ b

( b

bool (f,g) is non empty set

bool (f,g) is non empty Element of bool (bool (f,g))

bool (bool (f,g)) is non empty set

(bool (f,g)) /\ (f) is Element of bool (bool (f,g))

( { b

( b

f is set

(f) is non empty set

g is epsilon-transitive epsilon-connected ordinal set

(f,g) is Element of bool (f)

bool (f) is non empty set

{ b

( b

h is Relation-like Function-like T-Sequence-like set

dom h is epsilon-transitive epsilon-connected ordinal set

rng h is set

union (rng h) is set

(union (rng h)) /\ (f) is set

p is set

I is set

c

h . c

y is epsilon-transitive epsilon-connected ordinal set

(f,y) is Element of bool (f)

p is set

I is Element of (f)

c

(f,c

c

(f,c

h . c

f is set

g is set

(g) is non empty set

h is epsilon-transitive epsilon-connected ordinal set

succ h is non empty epsilon-transitive epsilon-connected ordinal set

{h} is non empty set

h \/ {h} is non empty set

(g,(succ h)) is Element of bool (g)

bool (g) is non empty set

(g,h) is Element of bool (g)

{ b

( b

{ (bool b

bool (g,h) is non empty set

bool (g,h) is non empty Element of bool (bool (g,h))

bool (bool (g,h)) is non empty set

(bool (g,h)) /\ (g) is Element of bool (bool (g,h))

{ b

( b

( { b

( b

y is Element of (g)

f is Element of (g)

y is Element of (g)

bool y is non empty Element of bool (bool y)

bool y is non empty set

bool (bool y) is non empty set

y is set

bool y is non empty Element of bool (bool y)

bool y is non empty set

bool (bool y) is non empty set

f is set

bool f is non empty Element of bool (bool f)

bool f is non empty set

bool (bool f) is non empty set

f1 is set

bool f1 is non empty Element of bool (bool f1)

bool f1 is non empty set

bool (bool f1) is non empty set

y is set

bool y is non empty Element of bool (bool y)

bool y is non empty set

bool (bool y) is non empty set

f is Element of (g)

f1 is Element of (g)

bool f is non empty Element of bool (bool f)

bool f is non empty set

bool (bool f) is non empty set

y is set

bool y is non empty Element of bool (bool y)

bool y is non empty set

bool (bool y) is non empty set

f is set

g is set

h is set

p is epsilon-transitive epsilon-connected ordinal set

(h,p) is Element of bool (h)

(h) is non empty set

bool (h) is non empty set

succ p is non empty epsilon-transitive epsilon-connected ordinal set

{p} is non empty set

p \/ {p} is non empty set

(h,(succ p)) is Element of bool (h)

f is set

g is set

h is epsilon-transitive epsilon-connected ordinal set

(g,h) is Element of bool (g)

(g) is non empty set

bool (g) is non empty set

bool f is non empty Element of bool (bool f)

bool f is non empty set

bool (bool f) is non empty set

succ h is non empty epsilon-transitive epsilon-connected ordinal set

{h} is non empty set

h \/ {h} is non empty set

(g,(succ h)) is Element of bool (g)

f is set

g is set

h is epsilon-transitive epsilon-connected ordinal set

(f,h) is Element of bool (f)

(f) is non empty set

bool (f) is non empty set

{ b

( b

p is Element of (f)

I is epsilon-transitive epsilon-connected ordinal set

(f,I) is Element of bool (f)

p is epsilon-transitive epsilon-connected ordinal set

(f,p) is Element of bool (f)

I is Element of (f)

f is set

bool f is non empty Element of bool (bool f)

bool f is non empty set

bool (bool f) is non empty set

g is set

h is set

p is epsilon-transitive epsilon-connected ordinal set

(g,p) is Element of bool (g)

(g) is non empty set

bool (g) is non empty set

I is epsilon-transitive epsilon-connected ordinal set

(g,I) is Element of bool (g)

succ I is non empty epsilon-transitive epsilon-connected ordinal set

{I} is non empty set

I \/ {I} is non empty set

(g,(succ I)) is Element of bool (g)

f is set

g is epsilon-transitive epsilon-connected ordinal set

(f,g) is Element of bool (f)

(f) is non empty set

bool (f) is non empty set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

(f,(succ g)) is Element of bool (f)

h is set

{ b

( b

{ (bool b

{ b

( b

bool (f,g) is non empty set

bool (f,g) is non empty Element of bool (bool (f,g))

bool (bool (f,g)) is non empty set

(bool (f,g)) /\ (f) is Element of bool (bool (f,g))

( { b

( b

f is set

g is epsilon-transitive epsilon-connected ordinal set

(f,g) is Element of bool (f)

(f) is non empty set

bool (f) is non empty set

h is epsilon-transitive epsilon-connected ordinal set

(f,h) is Element of bool (f)

p is epsilon-transitive epsilon-connected ordinal set

(f,p) is Element of bool (f)

I is set

c

succ c

{c

c

(f,c

{ b

( b

c

succ c

{c

c

f is set

(f) is non empty set

g is set

h is set

p is set

I is set

c

succ c

{c

c

(f,(succ c

bool (f) is non empty set

(f,c

y is epsilon-transitive epsilon-connected ordinal set

succ y is non empty epsilon-transitive epsilon-connected ordinal set

{y} is non empty set

y \/ {y} is non empty set

(f,(succ y)) is Element of bool (f)

(f,y) is Element of bool (f)

h is set

p is epsilon-transitive epsilon-connected ordinal set

(f,p) is Element of bool (f)

bool (f) is non empty set

succ p is non empty epsilon-transitive epsilon-connected ordinal set

{p} is non empty set

p \/ {p} is non empty set

(f,(succ p)) is Element of bool (f)

I is set

f is set

(f) is non empty set

g is epsilon-transitive epsilon-connected ordinal set

(f,g) is Element of bool (f)

bool (f) is non empty set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

(f,(succ g)) is Element of bool (f)

(f,{}) is Element of bool (f)

{f} is non empty set

{ b

( b

{ (bool b

{ b

( b

bool (f,g) is non empty set

bool (f,g) is non empty Element of bool (bool (f,g))

bool (bool (f,g)) is non empty set

(bool (f,g)) /\ (f) is Element of bool (bool (f,g))

( { b

( b

h is set

p is set

I is Element of (f)

c

h is set

bool h is non empty Element of bool (bool h)

bool h is non empty set

bool (bool h) is non empty set

h is set

f is set

(f) is non empty set

g is epsilon-transitive epsilon-connected ordinal set

(f,g) is Element of bool (f)

bool (f) is non empty set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

(f,(succ g)) is Element of bool (f)

f is set

(f) is non empty set

g is epsilon-transitive epsilon-connected ordinal set

(f,g) is Element of bool (f)

bool (f) is non empty set

h is epsilon-transitive epsilon-connected ordinal set

(f,h) is Element of bool (f)

f is set

g is set

(g) is non empty set

h is epsilon-transitive epsilon-connected ordinal set

(g,h) is Element of bool (g)

bool (g) is non empty set

h is epsilon-transitive epsilon-connected ordinal set

(g,h) is Element of bool (g)

bool (g) is non empty set

{g} is non empty set

(g,{}) is Element of bool (g)

p is epsilon-transitive epsilon-connected ordinal set

(g,p) is Element of bool (g)

p is epsilon-transitive epsilon-connected ordinal set

succ p is non empty epsilon-transitive epsilon-connected ordinal set

{p} is non empty set

p \/ {p} is non empty set

(g,p) is Element of bool (g)

(g,(succ p)) is Element of bool (g)

f is set

g is epsilon-transitive epsilon-connected ordinal set

(f,g) is Element of bool (f)

(f) is non empty set

bool (f) is non empty set

h is set

p is epsilon-transitive epsilon-connected ordinal set

succ p is non empty epsilon-transitive epsilon-connected ordinal set

{p} is non empty set

p \/ {p} is non empty set

(f,p) is Element of bool (f)

I is set

bool I is non empty Element of bool (bool I)

bool I is non empty set

bool (bool I) is non empty set

c

c

{f} is non empty set

p is epsilon-transitive epsilon-connected ordinal set

(f,p) is Element of bool (f)

succ p is non empty epsilon-transitive epsilon-connected ordinal set

{p} is non empty set

p \/ {p} is non empty set

(f,(succ p)) is Element of bool (f)

p is epsilon-transitive epsilon-connected ordinal set

succ p is non empty epsilon-transitive epsilon-connected ordinal set

{p} is non empty set

p \/ {p} is non empty set

f is set

(f) is non empty set

g is epsilon-transitive epsilon-connected ordinal set

(f,g) is Element of bool (f)

bool (f) is non empty set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

(f,(succ g)) is Element of bool (f)

f is set

card f is cardinal set

g is set

(g) is non empty set

card (g) is cardinal set

bool f is non empty Element of bool (bool f)

bool f is non empty set

bool (bool f) is non empty set

h is set

card (bool f) is cardinal set

f is set

g is set

(g) is non empty set

card f is cardinal set

card (g) is cardinal set

f is set

(f) is non empty set

g is set

{g} is non empty set

h is set

{g,h} is non empty set

bool g is non empty Element of bool (bool g)

bool g is non empty set

bool (bool g) is non empty set

bool {g} is non empty Element of bool (bool {g})

bool {g} is non empty set

bool (bool {g}) is non empty set

{{},{g}} is non empty set

p is Relation-like Function-like set

dom p is set

rng p is set

I is set

c

p . I is set

p . c

I is set

c

p . c

I is set

p . {} is set

p . {g} is set

f is set

(f) is non empty set

g is set

h is set

[g,h] is set

{g,h} is non empty set

{g} is non empty set

{{g,h},{g}} is non empty set

f is set

g is set

(g) is non empty set

h is set

[:f,h:] is Relation-like set

p is set

I is set

[p,I] is set

{p,I} is non empty set

{p} is non empty set

{{p,I},{p}} is non empty set

f is epsilon-transitive epsilon-connected ordinal set

succ f is non empty epsilon-transitive epsilon-connected ordinal set

{f} is non empty set

f \/ {f} is non empty set

g is set

f is epsilon-transitive epsilon-connected ordinal set

(f) is set

succ f is non empty epsilon-transitive epsilon-connected ordinal set

{f} is non empty set

f \/ {f} is non empty set

p is set

I is Relation-like Function-like T-Sequence-like set

last I is set

dom I is epsilon-transitive epsilon-connected ordinal set

h is epsilon-transitive epsilon-connected ordinal set

succ h is non empty epsilon-transitive epsilon-connected ordinal set

{h} is non empty set

h \/ {h} is non empty set

I . {} is set

(h) is set

({}) is set

f is epsilon-transitive epsilon-connected ordinal set

(f) is set

g is Relation-like Function-like T-Sequence-like set

dom g is epsilon-transitive epsilon-connected ordinal set

rng g is set

union (rng g) is set

f is epsilon-transitive epsilon-connected ordinal set

succ f is non empty epsilon-transitive epsilon-connected ordinal set

{f} is non empty set

f \/ {f} is non empty set

((succ f)) is set

(f) is set

bool (f) is non empty Element of bool (bool (f))

bool (f) is non empty set

bool (bool (f)) is non empty set

f is epsilon-transitive epsilon-connected ordinal set

(f) is set

g is Relation-like Function-like T-Sequence-like set

dom g is epsilon-transitive epsilon-connected ordinal set

rng g is set

union (rng g) is set

h is set

p is set

I is set

g . I is set

c

(c

p is epsilon-transitive epsilon-connected ordinal set

(p) is set

g . p is set

f is set

g is epsilon-transitive epsilon-connected ordinal set

(g) is set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

((succ g)) is set

bool (g) is non empty Element of bool (bool (g))

bool (g) is non empty set

bool (bool (g)) is non empty set

bool (g) is non empty Element of bool (bool (g))

bool (g) is non empty set

bool (bool (g)) is non empty set

f is epsilon-transitive epsilon-connected ordinal set

(f) is set

g is epsilon-transitive epsilon-connected ordinal set

(g) is set

h is set

p is set

I is epsilon-transitive epsilon-connected ordinal set

(I) is set

I is epsilon-transitive epsilon-connected ordinal set

succ I is non empty epsilon-transitive epsilon-connected ordinal set

{I} is non empty set

I \/ {I} is non empty set

(I) is set

g is set

f is epsilon-transitive epsilon-connected ordinal set

(f) is epsilon-transitive set

succ f is non empty epsilon-transitive epsilon-connected ordinal set

{f} is non empty set

f \/ {f} is non empty set

((succ f)) is epsilon-transitive set

bool (f) is non empty Element of bool (bool (f))

bool (f) is non empty set

bool (bool (f)) is non empty set

f is epsilon-transitive epsilon-connected ordinal set

(f) is epsilon-transitive set

union (f) is set

g is set

h is set

f is set

union f is set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

h is epsilon-transitive epsilon-connected ordinal set

succ h is non empty epsilon-transitive epsilon-connected ordinal set

{h} is non empty set

h \/ {h} is non empty set

(h) is epsilon-transitive set

union (h) is set

h is epsilon-transitive epsilon-connected ordinal set

(h) is epsilon-transitive set

union (h) is set

succ h is non empty epsilon-transitive epsilon-connected ordinal set

{h} is non empty set

h \/ {h} is non empty set

((succ h)) is epsilon-transitive set

h is epsilon-transitive epsilon-connected ordinal set

succ h is non empty epsilon-transitive epsilon-connected ordinal set

{h} is non empty set

h \/ {h} is non empty set

f is epsilon-transitive epsilon-connected ordinal set

(f) is epsilon-transitive set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

h is epsilon-transitive epsilon-connected ordinal set

(h) is epsilon-transitive set

p is epsilon-transitive epsilon-connected ordinal set

(p) is epsilon-transitive set

I is epsilon-transitive epsilon-connected ordinal set

succ I is non empty epsilon-transitive epsilon-connected ordinal set

{I} is non empty set

I \/ {I} is non empty set

(I) is epsilon-transitive set

succ h is non empty epsilon-transitive epsilon-connected ordinal set

{h} is non empty set

h \/ {h} is non empty set

((succ h)) is epsilon-transitive set

I is epsilon-transitive epsilon-connected ordinal set

succ I is non empty epsilon-transitive epsilon-connected ordinal set

{I} is non empty set

I \/ {I} is non empty set

f is epsilon-transitive epsilon-connected ordinal set

(f) is epsilon-transitive set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

f is epsilon-transitive epsilon-connected ordinal set

(f) is epsilon-transitive set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

((succ g)) is epsilon-transitive set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

h is set

p is epsilon-transitive epsilon-connected ordinal set

succ p is non empty epsilon-transitive epsilon-connected ordinal set

{p} is non empty set

p \/ {p} is non empty set

(p) is epsilon-transitive set

((succ p)) is epsilon-transitive set

f is epsilon-transitive epsilon-connected ordinal set

(f) is epsilon-transitive set

g is set

h is epsilon-transitive epsilon-connected ordinal set

succ h is non empty epsilon-transitive epsilon-connected ordinal set

{h} is non empty set

h \/ {h} is non empty set

((succ h)) is epsilon-transitive set

(h) is epsilon-transitive set

bool (h) is non empty Element of bool (bool (h))

bool (h) is non empty set

bool (bool (h)) is non empty set

h is epsilon-transitive epsilon-connected ordinal set

(h) is epsilon-transitive set

h is epsilon-transitive epsilon-connected ordinal set

succ h is non empty epsilon-transitive epsilon-connected ordinal set

{h} is non empty set

h \/ {h} is non empty set

f is epsilon-transitive epsilon-connected ordinal set

(f) is epsilon-transitive set

card (f) is cardinal set

g is set

card g is cardinal set

f is set

bool f is non empty Element of bool (bool f)

bool f is non empty set

bool (bool f) is non empty set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

((succ g)) is epsilon-transitive set

h is set

bool (g) is non empty Element of bool (bool (g))

bool (g) is non empty set

bool (bool (g)) is non empty set

h is set

{h} is non empty set

bool (g) is non empty Element of bool (bool (g))

bool (g) is non empty set

bool (bool (g)) is non empty set

f is set

g is set

h is epsilon-transitive epsilon-connected ordinal set

(h) is epsilon-transitive set

p is epsilon-transitive epsilon-connected ordinal set

succ p is non empty epsilon-transitive epsilon-connected ordinal set

{p} is non empty set

p \/ {p} is non empty set

((succ p)) is epsilon-transitive set

(p) is epsilon-transitive set

bool (p) is non empty Element of bool (bool (p))

bool (p) is non empty set

bool (bool (p)) is non empty set

p is epsilon-transitive epsilon-connected ordinal set

(p) is epsilon-transitive set

bool (p) is non empty Element of bool (bool (p))

bool (p) is non empty set

bool (bool (p)) is non empty set

succ p is non empty epsilon-transitive epsilon-connected ordinal set

{p} is non empty set

p \/ {p} is non empty set

((succ p)) is epsilon-transitive set

p is epsilon-transitive epsilon-connected ordinal set

succ p is non empty epsilon-transitive epsilon-connected ordinal set

{p} is non empty set

p \/ {p} is non empty set

f is set

bool f is non empty Element of bool (bool f)

bool f is non empty set

bool (bool f) is non empty set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

((succ g)) is epsilon-transitive set

h is set

f is set

{f} is non empty set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

((succ g)) is epsilon-transitive set

f is set

g is set

{f,g} is non empty set

h is epsilon-transitive epsilon-connected ordinal set

(h) is epsilon-transitive set

succ h is non empty epsilon-transitive epsilon-connected ordinal set

{h} is non empty set

h \/ {h} is non empty set

((succ h)) is epsilon-transitive set

f is set

g is set

[f,g] is set

{f,g} is non empty set

{f} is non empty set

{{f,g},{f}} is non empty set

h is epsilon-transitive epsilon-connected ordinal set

(h) is epsilon-transitive set

succ h is non empty epsilon-transitive epsilon-connected ordinal set

{h} is non empty set

h \/ {h} is non empty set

succ (succ h) is non empty epsilon-transitive epsilon-connected ordinal set

{(succ h)} is non empty set

(succ h) \/ {(succ h)} is non empty set

((succ (succ h))) is epsilon-transitive set

((succ h)) is epsilon-transitive set

f is set

(f) is non empty set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

(g) /\ (f) is set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

((succ g)) is epsilon-transitive set

((succ g)) /\ (f) is set

h is set

(f) \ (g) is Element of bool (f)

bool (f) is non empty set

p is set

I is set

f is set

(f) is non empty set

g is set

h is set

p is set

I is set

c

(c

succ c

{c

c

((succ c

y is epsilon-transitive epsilon-connected ordinal set

(y) is epsilon-transitive set

succ y is non empty epsilon-transitive epsilon-connected ordinal set

{y} is non empty set

y \/ {y} is non empty set

((succ y)) is epsilon-transitive set

h is set

p is epsilon-transitive epsilon-connected ordinal set

(p) is epsilon-transitive set

(p) /\ (f) is set

succ p is non empty epsilon-transitive epsilon-connected ordinal set

{p} is non empty set

p \/ {p} is non empty set

((succ p)) is epsilon-transitive set

((succ p)) /\ (f) is set

I is set

f is set

union f is set

g is set

h is set

f is set

g is set

f \/ g is set

h is set

f is set

g is set

f /\ g is set

h is set

f is set

g is Relation-like Function-like set

dom g is set

g . {} is set

rng g is set

union (rng g) is set

h is set

p is set

I is set

c

g . c

y is epsilon-transitive epsilon-connected ordinal natural Element of omega

g . y is set

f is epsilon-transitive epsilon-connected ordinal natural set

succ f is non empty epsilon-transitive epsilon-connected ordinal natural set

{f} is non empty set

f \/ {f} is non empty set

g . (succ f) is set

g . f is set

union (g . f) is set

I is Relation-like Function-like set

c

I . c

dom I is set

I . {} is set

y is epsilon-transitive epsilon-connected ordinal natural set

succ y is non empty epsilon-transitive epsilon-connected ordinal natural set

{y} is non empty set

y \/ {y} is non empty set

g . (succ y) is set

g . y is set

union (g . y) is set

g is set

h is set

f is set

(f) is set

g is set

h is Relation-like Function-like set

p is epsilon-transitive epsilon-connected ordinal natural Element of omega

h . p is set

dom h is set

h . {} is set

succ p is non empty epsilon-transitive epsilon-connected ordinal natural set

{p} is non empty set

p \/ {p} is non empty set

h . (succ p) is set

union (h . p) is set

I is set

c

h . c

f is set

(f) is set

g is set

h is Relation-like Function-like set

dom h is set

h . {} is set

p is epsilon-transitive epsilon-connected ordinal natural Element of omega

h . p is set

f is set

(f) is set

g is set

h is set

p is Relation-like Function-like set

I is epsilon-transitive epsilon-connected ordinal natural Element of omega

p . I is set

dom p is set

p . {} is set

c

p . c

succ c

{c

c

p . (succ c

union (p . c

union g is set

f is set

(f) is set

g is set

f is set

(f) is set

g is set

({}) is set

f is epsilon-transitive epsilon-connected ordinal set

(f) is set

f is set

(f) is set

g is set

(g) is set

f is set

(f) is set

((f)) is set

f is set

(f) is set

g is set

f \/ g is set

((f \/ g)) is set

(g) is set

(f) \/ (g) is set

(((f) \/ (g))) is set

f is set

(f) is set

g is set

f /\ g is set

((f /\ g)) is set

(g) is set

(f) /\ (g) is set

f is set

(f) is set

((f)) is non empty set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

f is set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

h is epsilon-transitive epsilon-connected ordinal set

(h) is epsilon-transitive set

f is set

bool f is non empty Element of bool (bool f)

bool f is non empty set

bool (bool f) is non empty set

((bool f)) is epsilon-transitive epsilon-connected ordinal set

(f) is epsilon-transitive epsilon-connected ordinal set

succ (f) is non empty epsilon-transitive epsilon-connected ordinal set

{(f)} is non empty set

(f) \/ {(f)} is non empty set

((f)) is epsilon-transitive set

((succ (f))) is epsilon-transitive set

g is set

bool ((f)) is non empty Element of bool (bool ((f)))

bool ((f)) is non empty set

bool (bool ((f))) is non empty set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

h is epsilon-transitive epsilon-connected ordinal set

(h) is epsilon-transitive set

p is epsilon-transitive epsilon-connected ordinal set

(p) is epsilon-transitive set

p is epsilon-transitive epsilon-connected ordinal set

succ p is non empty epsilon-transitive epsilon-connected ordinal set

{p} is non empty set

p \/ {p} is non empty set

p is epsilon-transitive epsilon-connected ordinal set

succ p is non empty epsilon-transitive epsilon-connected ordinal set

{p} is non empty set

p \/ {p} is non empty set

(p) is epsilon-transitive set

f is epsilon-transitive epsilon-connected ordinal set

(f) is epsilon-transitive set

((f)) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

f is set

(f) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

((f)) is epsilon-transitive set

f is set

(f) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

bool f is non empty Element of bool (bool f)

bool f is non empty set

bool (bool f) is non empty set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

((succ g)) is epsilon-transitive set

((bool f)) is epsilon-transitive epsilon-connected ordinal set

succ (f) is non empty epsilon-transitive epsilon-connected ordinal set

{(f)} is non empty set

(f) \/ {(f)} is non empty set

succ (f) is non empty epsilon-transitive epsilon-connected ordinal set

{(f)} is non empty set

(f) \/ {(f)} is non empty set

((f)) is epsilon-transitive set

((succ (f))) is epsilon-transitive set

f is set

(f) is epsilon-transitive epsilon-connected ordinal set

g is set

(g) is epsilon-transitive epsilon-connected ordinal set

((g)) is epsilon-transitive set

f is set

(f) is epsilon-transitive epsilon-connected ordinal set

g is set

(g) is epsilon-transitive epsilon-connected ordinal set

((g)) is epsilon-transitive set

f is set

(f) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

((f)) is epsilon-transitive set

p is set

(p) is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

(g) is epsilon-transitive set

p is set

(p) is epsilon-transitive epsilon-connected ordinal set

f is set

(f) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

h is epsilon-transitive epsilon-connected ordinal set

(h) is epsilon-transitive set

f \ (h) is Element of bool f

bool f is non empty set

the Element of f \ (h) is Element of f \ (h)

( the Element of f \ (h)) is epsilon-transitive epsilon-connected ordinal set

h is set

p is epsilon-transitive epsilon-connected ordinal set

I is set

(I) is epsilon-transitive epsilon-connected ordinal set

f is set

(f) is epsilon-transitive epsilon-connected ordinal set

g is set

(g) is epsilon-transitive epsilon-connected ordinal set

f is set

(f) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

h is set

(h) 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 set

g is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive epsilon-connected ordinal set

h is epsilon-transitive epsilon-connected ordinal set

p is set

I is set

(I) is epsilon-transitive epsilon-connected ordinal set

f is set

(f) is non empty set

((f)) is epsilon-transitive epsilon-connected ordinal set

(((f))) is epsilon-transitive set

g is epsilon-transitive epsilon-connected ordinal set

succ g is non empty epsilon-transitive epsilon-connected ordinal set

{g} is non empty set

g \/ {g} is non empty set

h is set

(h) is epsilon-transitive epsilon-connected ordinal set

bool h is non empty Element of bool (bool h)

bool h is non empty set

bool (bool h) is non empty set

((bool h)) is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive set

F

f is set

f is Relation-like Function-like set

dom f is set

rng f is set

f is non empty set

g is Element of f

h is set

(h) is epsilon-transitive epsilon-connected ordinal set

((h)) is epsilon-transitive set

succ (h) is non empty epsilon-transitive epsilon-connected ordinal set

{(h)} is non empty set

(h) \/ {(h)} is non empty set

((succ (h))) is epsilon-transitive set

g is Relation-like Function-like set

dom g is set

rng g is set

sup (rng g) is epsilon-transitive epsilon-connected ordinal set

((sup (rng g))) is epsilon-transitive set

h is set

g . h is set

p is epsilon-transitive epsilon-connected ordinal set

(p) is epsilon-transitive set

I is set

I is set

h is Relation-like Function-like set

dom h is set

rng h is set

h is Relation-like set

p is set

Coim (h,p) is set

{p} is non empty set

h " {p} is set

card (Coim (h,p)) is cardinal set

h is Relation-like set

p is Relation-like set

I is set

Coim (p,I) is set

{I} is non empty set

p " {I} is set

card (Coim (p,I)) is cardinal set

Coim (h,I) is set

h " {I} is set

card (Coim (h,I)) is cardinal set

f is Relation-like Function-like set

rng f is set

g is set

Coim (f,g) is set

{g} is non empty set

f " {g} is set

h is set

f is Relation-like Function-like set

g is Relation-like Function-like set

rng f is set

rng g is set

h is set

Coim (f,h) is set

{h} is non empty set

f " {h} is set

card (Coim (f,h)) is cardinal set

Coim (g,h) is set

g " {h} is set

card (Coim (g,h)) is cardinal set

dom f is set

p is set

f . p is set

h is set

Coim (g,h) is set

{h} is non empty set

g " {h} is set

card (Coim (g,h)) is cardinal set

Coim (f,h) is set

f " {h} is set

card (Coim (f,h)) is cardinal set

dom g is set

p is set

g . p is set

f is Relation-like Function-like set

g is Relation-like Function-like set

h is Relation-like Function-like set

p is set

Coim (g,p) is set

{p} is non empty set

g " {p} is set

card (Coim (g,p)) is cardinal set

Coim (h,p) is set

h " {p} is set

card (Coim (h,p)) is cardinal set

Coim (f,p) is set

f " {p} is set

card (Coim (f,p)) is cardinal set

f is Relation-like Function-like set

g is Relation-like Function-like set

dom f is set

dom g is set

rng f is set

h is set

{h} is non empty set

f " {h} is set

g " {h} is set

Coim (f,h) is set

card (Coim (f,h)) is cardinal set

Coim (g,h) is set

card (Coim (g,h)) is cardinal set

p is Relation-like Function-like set

dom p is set

rng p is set

I is Relation-like Function-like set

dom I is set

rng I is set

h is Relation-like Function-like set

dom h is set

c

f . c

h . (f . c

y is Relation-like Function-like set

dom y is set

{(f . c

f " {(f . c

rng y is set

g " {(f . c

y . c

f is set

f1 is Relation-like Function-like set

f1 . c

c

dom c

rng c

c

y is set

g . y is set

rng g is set

h . (g . y) is set

f is Relation-like Function-like set

dom f is set

{(g . y)} is non empty set

f " {(g . y)} is set

rng f is set

g " {(g . y)} is set

f1 is set

f . f1 is set

f . f1 is set

c

y is set

f is set

c

c

f . y is set

f . f is set

h . (f . y) is set

h . (f . f) is set

f1 is Relation-like Function-like set

f1 . y is set

f2 is Relation-like Function-like set

f2 . f is set

dom f1 is set

{(f . y)} is non empty set

f " {(f . y)} is set

rng f1 is set

g " {(f . y)} is set

dom f2 is set

{(f . f)} is non empty set

f " {(f . f)} is set

rng f2 is set

g " {(f . f)} is set

(g " {(f . y)}) /\ (g " {(f . f)}) is set

{(f . y)} /\ {(f . f)} is set

g " ({(f . y)} /\ {(f . f)}) is set

g . (f1 . y) is set

dom (c

y is set

f . y is set

h . (f . y) is set

f is Relation-like Function-like set

dom f is set

{(f . y)} is non empty set

f " {(f . y)} is set

rng f is set

g " {(f . y)} is set

f . y is set

g . (f . y) is set

c

(c

h is Relation-like Function-like set

dom h is set

rng h is set

h * g is Relation-like Function-like set

p is set

Coim (f,p) is set

{p} is non empty set

f " {p} is set

card (Coim (f,p)) is cardinal set

Coim (g,p) is set

g " {p} is set

card (Coim (g,p)) is cardinal set

h | (f " {p}) is Relation-like Function-like set

dom (h | (f " {p})) is set

rng (h | (f " {p})) is set

c

y is set

(h | (f " {p})) . y is set

f . y is set

h . y is set

(dom h) /\ (f " {p}) is set

g . c

c

g . c

y is set

h . y is set

f . y is set

(h | (f " {p})) . y is set

f is Relation-like Function-like set

g is Relation-like Function-like set

dom f is set

dom g is set

h is Relation-like Function-like set

dom h is set

rng h is set

h * g is Relation-like Function-like set

p is set

f " p is set

card (f " p) is cardinal set

g " p is set

card (g " p) is cardinal set

h | (f " p) is Relation-like Function-like set

dom (h | (f " p)) is set

rng (h | (f " p)) is set

c

y is set

(h | (f " p)) . y is set

f . y is set

h . y is set

(dom h) /\ (f " p) is set

g . c

c

g . c

y is set

h . y is set

f . y is set

(h | (f " p)) . y is set

h is set

Coim (f,h) is set

{h} is non empty set

f " {h} is set

card (Coim (f,h)) is cardinal set

Coim (g,h) is set

g " {h} is set

card (Coim (g,h)) is cardinal set

f is non empty set

g is Relation-like Function-like set

rng g is set

h is Relation-like Function-like set

rng h is set

p is set

Coim (g,p) is set

{p} is non empty set

g " {p} is set

card (Coim (g,p)) is cardinal set

Coim (h,p) is set

h " {p} is set

card (Coim (h,p)) is cardinal set

I is Element of f

Coim (h,I) is set

{I} is non empty set

h " {I} is set

card (Coim (h,I)) is cardinal set

Coim (g,I) is set

g " {I} is set

card (Coim (g,I)) is cardinal set

dom h is set

c

h . c

I is Element of f

Coim (g,I) is set

{I} is non empty set

g " {I} is set

card (Coim (g,I)) is cardinal set

Coim (h,I) is set

h " {I} is set

card (Coim (h,I)) is cardinal set

f is Relation-like Function-like set

dom f is set

g is Relation-like Function-like set

dom g is set

[:(dom f),(dom f):] is Relation-like set

bool [:(dom f),(dom f):] is non empty set

h is Relation-like Function-like set

dom h is set

rng h is set

h * g is Relation-like Function-like set

p is Relation-like dom f -defined dom f -valued Function-like V38( dom f) quasi_total Element of bool [:(dom f),(dom f):]

I is Relation-like dom f -defined dom f -valued Function-like one-to-one V38( dom f) quasi_total onto bijective Element of bool [:(dom f),(dom f):]

I * g is Relation-like dom f -defined Function-like set

h is Relation-like dom f -defined dom f -valued Function-like one-to-one V38( dom f) quasi_total onto bijective Element of bool [:(dom f),(dom f):]

h * g is Relation-like dom f -defined Function-like set

rng h is set

dom h is set

f is Relation-like Function-like set

g is Relation-like Function-like set

dom f is set

card (dom f) is cardinal set

dom g is set

card (dom g) is cardinal set

rng f is set

f " (rng f) is set

card (f " (rng f)) is cardinal set

g " (rng f) is set

card (g " (rng f)) is cardinal set

rng g is set

g " (rng g) is set

card (g " (rng g)) is cardinal set

f is set

g is Relation-like set

rng g is set

[g,f] is set

{g,f} is non empty set

{g} is non empty set

{{g,f},{g}} is non empty set

([g,f]) is epsilon-transitive epsilon-connected ordinal set

h is set

(h) is epsilon-transitive epsilon-connected ordinal set

p is set

[p,h] is set

{p,h} is non empty set

{p} is non empty set

{{p,h},{p}} is non empty set

({p,h}) is epsilon-transitive epsilon-connected ordinal set

([p,h]) is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive epsilon-connected ordinal set

({g,f}) is epsilon-transitive epsilon-connected ordinal set

f is Relation-like Function-like set

dom f is set

g is Relation-like Function-like set

dom g is set

rng f is set

h is Relation-like Function-like set

dom h is set

rng g is set

f * h is Relation-like Function-like set

g * h is Relation-like Function-like set

[:(dom f),(dom f):] is Relation-like set

bool [:(dom f),(dom f):] is non empty set

p is Relation-like dom f -defined dom f -valued Function-like one-to-one V38( dom f) quasi_total onto bijective Element of bool [:(dom f),(dom f):]

p * g is Relation-like dom f -defined Function-like set

dom (f * h) is set

dom (g * h) is set

p * (g * h) is Relation-like dom f -defined Function-like set