:: 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₆ is set
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₆ is set
I is set
c₆ is set
I is set
(meet h) /\ I is set
c₆ is set
y is set
c₆ is set
bool c₆ is non empty Element of bool (bool c₆)
bool c₆ is non empty set
bool (bool c₆) is non empty set
c₆ is set
c₆ is set
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₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in a₂ & b₁ c= b₂ ) } is set
{ (bool b₁) where b₁ is Element of (f) : b₁ in a₂ } is set
{ b₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in a₂ & b₁ c= b₂ ) } \/ { (bool b₁) where b₁ is Element of (f) : b₁ in a₂ } is set
f is set
(f) is non empty set
{ b₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in a₂ & b₁ c= b₂ ) } is set
{ (bool b₁) where b₁ is Element of (f) : b₁ in a₂ } is set
{ b₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in a₂ & b₁ c= b₂ ) } \/ { (bool b₁) where b₁ is Element of (f) : b₁ in a₂ } is set
{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₆ is Relation-like Function-like T-Sequence-like set
last c₆ is set
dom c₆ is epsilon-transitive epsilon-connected ordinal 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
c₆ . {} is set
(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₆ is set
p is Element of bool (f)
{ b₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in p & b₁ c= b₂ ) } is set
{ (bool b₁) where b₁ is Element of (f) : b₁ in p } is set
{ b₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in p & b₁ c= b₂ ) } \/ { (bool b₁) where b₁ is Element of (f) : b₁ in p } is set
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₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in p & b₁ c= b₂ ) } \/ { (bool b₁) where b₁ is Element of (f) : b₁ in p } ) \/ ((bool p) /\ (f)) is set
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₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in (f,g) & b₁ c= b₂ ) } is set
{ (bool b₁) where b₁ is Element of (f) : b₁ in (f,g) } is set
{ b₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in (f,g) & b₁ c= b₂ ) } \/ { (bool b₁) where b₁ is Element of (f) : b₁ in (f,g) } is set
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₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in (f,g) & b₁ c= b₂ ) } \/ { (bool b₁) where b₁ is Element of (f) : b₁ in (f,g) } ) \/ ((bool (f,g)) /\ (f)) 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
{ b₁ where b₁ is Element of (f) : ex b₂ being epsilon-transitive epsilon-connected ordinal set st
( b₂ in g & b₁ in (f,b₂) ) } 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
p is set
I is set
c₆ is set
h . c₆ is set
y is epsilon-transitive epsilon-connected ordinal set
(f,y) is Element of bool (f)
p is set
I is Element of (f)
c₆ is epsilon-transitive epsilon-connected ordinal set
(f,c₆) is Element of bool (f)
c₆ is epsilon-transitive epsilon-connected ordinal set
(f,c₆) is Element of bool (f)
h . c₆ is set
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₁ where b₁ is Element of (g) : ex b₂ being Element of (g) st
( b₂ in (g,h) & b₁ c= b₂ ) } is set
{ (bool b₁) where b₁ is Element of (g) : b₁ in (g,h) } is set
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₁ where b₁ is Element of (g) : ex b₂ being Element of (g) st
( b₂ in (g,h) & b₁ c= b₂ ) } \/ { (bool b₁) where b₁ is Element of (g) : b₁ in (g,h) } is set
( { b₁ where b₁ is Element of (g) : ex b₂ being Element of (g) st
( b₂ in (g,h) & b₁ c= b₂ ) } \/ { (bool b₁) where b₁ is Element of (g) : b₁ in (g,h) } ) \/ ((bool (g,h)) /\ (g)) is set
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₁ where b₁ is Element of (f) : ex b₂ being epsilon-transitive epsilon-connected ordinal set st
( b₂ in h & b₁ in (f,b₂) ) } is set
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₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in (f,g) & b₁ c= b₂ ) } is set
{ (bool b₁) where b₁ is Element of (f) : b₁ in (f,g) } is set
{ b₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in (f,g) & b₁ c= b₂ ) } \/ { (bool b₁) where b₁ is Element of (f) : b₁ in (f,g) } is set
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₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in (f,g) & b₁ c= b₂ ) } \/ { (bool b₁) where b₁ is Element of (f) : b₁ in (f,g) } ) \/ ((bool (f,g)) /\ (f)) is set
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₆ is epsilon-transitive epsilon-connected ordinal set
succ c₆ is non empty epsilon-transitive epsilon-connected ordinal set
{c₆} is non empty set
c₆ \/ {c₆} is non empty set
(f,c₆) is Element of bool (f)
{ b₁ where b₁ is Element of (f) : ex b₂ being epsilon-transitive epsilon-connected ordinal set st
( b₂ in p & b₁ in (f,b₂) ) } is set
c₆ is epsilon-transitive epsilon-connected ordinal set
succ c₆ is non empty epsilon-transitive epsilon-connected ordinal set
{c₆} is non empty set
c₆ \/ {c₆} is non empty set
f is set
(f) is non empty set
g is set
h is set
p is set
I is set
c₆ is epsilon-transitive epsilon-connected ordinal set
succ c₆ is non empty epsilon-transitive epsilon-connected ordinal set
{c₆} is non empty set
c₆ \/ {c₆} is non empty set
(f,(succ c₆)) is Element of bool (f)
bool (f) is non empty set
(f,c₆) is Element of bool (f)
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₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in (f,g) & b₁ c= b₂ ) } is set
{ (bool b₁) where b₁ is Element of (f) : b₁ in (f,g) } is set
{ b₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in (f,g) & b₁ c= b₂ ) } \/ { (bool b₁) where b₁ is Element of (f) : b₁ in (f,g) } is set
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₁ where b₁ is Element of (f) : ex b₂ being Element of (f) st
( b₂ in (f,g) & b₁ c= b₂ ) } \/ { (bool b₁) where b₁ is Element of (f) : b₁ in (f,g) } ) \/ ((bool (f,g)) /\ (f)) is set
h is set
p is set
I is Element of (f)
c₆ is Element of (f)
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₆ is set
c₆ is set
{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₆ is set
p . I is set
p . c₆ is set
I is set
c₆ is set
p . c₆ is set
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₆ is epsilon-transitive epsilon-connected ordinal set
(c₆) is set
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₆ is epsilon-transitive epsilon-connected ordinal set
(c₆) is epsilon-transitive set
succ c₆ is non empty epsilon-transitive epsilon-connected ordinal set
{c₆} is non empty set
c₆ \/ {c₆} is non empty set
((succ c₆)) is epsilon-transitive set
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₆ is set
g . c₆ is set
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₆ is epsilon-transitive epsilon-connected ordinal natural Element of omega
I . c₆ is set
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₆ is epsilon-transitive epsilon-connected ordinal natural Element of omega
h . c₆ is set
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₆ is epsilon-transitive epsilon-connected ordinal natural set
p . c₆ is set
succ c₆ is non empty epsilon-transitive epsilon-connected ordinal natural set
{c₆} is non empty set
c₆ \/ {c₆} is non empty set
p . (succ c₆) is set
union (p . c₆) is set
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₁() is set
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₆ is set
f . c₆ is set
h . (f . c₆) is set
y is Relation-like Function-like set
dom y is set
{(f . c₆)} is non empty set
f " {(f . c₆)} is set
rng y is set
g " {(f . c₆)} is set
y . c₆ is set
f is set
f1 is Relation-like Function-like set
f1 . c₆ is set
c₆ is Relation-like Function-like set
dom c₆ is set
rng c₆ is set
c₆ * g is Relation-like Function-like set
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₆ . f1 is set
y is set
f is set
c₆ . y is set
c₆ . f is set
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₆ * g) is set
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₆ . y is set
(c₆ * g) . y 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
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₆ is set
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₆ is set
c₆ is set
g . c₆ is set
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₆ is set
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₆ is set
c₆ is set
g . c₆ is set
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₆ is set
h . c₆ is set
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