:: ORDINAL3 semantic presentation

a is set
succ a is non empty set
{a} is non empty set
a \/ {a} is non empty set
a is set
succ a is non empty set
{a} is non empty set
a \/ {a} is non empty set
b is set

{a} is non empty set
a \/ {a} is non empty set

{b} is non empty set
b \/ {b} is non empty set

b is set
union b is set
a is set
a is set
On a is set
union (On a) is set
b is set

b is set
On b is set
a is set
b is set
a is set
b is set

{a} is non empty set
On {a} is set

a \/ {a} is non empty set

On a is set
meet (On a) is set
meet a is set

{a} is non empty set

On {a} is set
meet (On {a}) is set
meet {a} is set

b is set
meet b is set

On b is set
meet (On b) is set

a \/ b is set
a /\ b is set

is non empty set
{} \/ is non empty set

{a} is non empty set
a \/ {a} is non empty set

{b} is non empty set
b \/ {b} is non empty set

rng b is set

x is set
b . x is set

{a} is non empty set
a \/ {a} is non empty set

succ (a +^ a) is non empty epsilon-transitive epsilon-connected ordinal set
{(a +^ a)} is non empty set
(a +^ a) \/ {(a +^ a)} is non empty set

rng a is set

{b} is non empty set
b \/ {b} is non empty set

{b} is non empty set
b \/ {b} is non empty set

succ (b +^ b) is non empty epsilon-transitive epsilon-connected ordinal set
{(b +^ b)} is non empty set
(b +^ b) \/ {(b +^ b)} is non empty set

{b} is non empty set
b \/ {b} is non empty set

succ ((a +^ b) +^ b) is non empty epsilon-transitive epsilon-connected ordinal set
{((a +^ b) +^ b)} is non empty set
((a +^ b) +^ b) \/ {((a +^ b) +^ b)} is non empty set
succ (b +^ b) is non empty epsilon-transitive epsilon-connected ordinal set
{(b +^ b)} is non empty set
(b +^ b) \/ {(b +^ b)} is non empty set

rng b is set
rng a is set
x is set
k is set
b . k is set

x is set

b is set
a . b is set

b . b is set

b is set
a . b is set

b . b is set

b is set
a . b is set

b . b is set

b is set
a . b is set

b . b is set

rng a is set

rng b is set

a is set

n is set
a . n is set

a is set

m is set
b . m is set

rng a is set

{b} is non empty set
b \/ {b} is non empty set
b is set

k is set
a . k is set

{x} is non empty set
x \/ {x} is non empty set

{m} is non empty set
m \/ {m} is non empty set

succ ((m *^ b) +^ {}) is non empty epsilon-transitive epsilon-connected ordinal set
{((m *^ b) +^ {})} is non empty set
((m *^ b) +^ {}) \/ {((m *^ b) +^ {})} is non empty set

rng b is set

b is set

k is set
b . k is set

{m} is non empty set
m \/ {m} is non empty set

rng a is set

rng b is set

b is set

k is set
a . k is set

b is set

x is set
b . x is set

rng a is set

rng (b,a) is set

rng a is set

rng (b,a) is set

{a} is non empty set
a \/ {a} is non empty set

succ (b +^ a) is non empty epsilon-transitive epsilon-connected ordinal set
{(b +^ a)} is non empty set
(b +^ a) \/ {(b +^ a)} is non empty set

{a} is non empty set
a \/ {a} is non empty set

(a *^ a) +^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

{b} is non empty set
b \/ {b} is non empty set

(a *^ a) +^ ((succ b) *^ a) is epsilon-transitive epsilon-connected ordinal set
succ (a +^ b) is non empty epsilon-transitive epsilon-connected ordinal set
{(a +^ b)} is non empty set
(a +^ b) \/ {(a +^ b)} is non empty set

((a *^ a) +^ (b *^ a)) +^ a is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ ((b *^ a) +^ a) is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

x is set

(a,b) . x is set

(a *^ a) +^ (k *^ a) is epsilon-transitive epsilon-connected ordinal set

((a *^ a),a) . x is set

rng a is set

dom ((a *^ a),a) is epsilon-transitive epsilon-connected ordinal set

rng b is set

rng (a,b) is set

union ((a *^ a) +^ (sup a)) is epsilon-transitive epsilon-connected ordinal set

(a *^ a) +^ (union (sup a)) is epsilon-transitive epsilon-connected ordinal set

{b} is non empty set
b \/ {b} is non empty set

{a} is non empty set
a \/ {a} is non empty set

{b} is non empty set
b \/ {b} is non empty set

{b} is non empty set
b \/ {b} is non empty set

(b *^ a) +^ (x *^ a) is epsilon-transitive epsilon-connected ordinal set
((b *^ a) +^ (x *^ a)) +^ a is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ ((x *^ a) +^ a) is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ (x *^ a) is epsilon-transitive epsilon-connected ordinal set
((b *^ a) +^ (x *^ a)) +^ b is epsilon-transitive epsilon-connected ordinal set

(b *^ a) +^ ((x *^ a) +^ b) is epsilon-transitive epsilon-connected ordinal set

rng a is set

{b} is non empty set
b \/ {b} is non empty set

{b} is non empty set
b \/ {b} is non empty set
a is set
a . a is set

{x} is non empty set
x \/ {x} is non empty set

{b} is non empty set
b \/ {b} is non empty set

((b *^ b) +^ b) *^ a is epsilon-transitive epsilon-connected ordinal set
(b *^ (b *^ a)) +^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

(b *^ (b *^ a)) +^ (1 *^ (b *^ a)) is epsilon-transitive epsilon-connected ordinal set

(b +^ 1) *^ (b *^ a) is epsilon-transitive epsilon-connected ordinal set

rng (a,b) is set

rng b is set

(a,((a,b) *^ b)) is epsilon-transitive epsilon-connected ordinal set

((a +^ b),a) is epsilon-transitive epsilon-connected ordinal set

(a,(b +^ a)) is epsilon-transitive epsilon-connected ordinal set
((a,b),a) is epsilon-transitive epsilon-connected ordinal set
(b +^ a) +^ (a,(b +^ a)) is epsilon-transitive epsilon-connected ordinal set
a +^ (a,(b +^ a)) is epsilon-transitive epsilon-connected ordinal set
b +^ (a +^ (a,(b +^ a))) is epsilon-transitive epsilon-connected ordinal set

(b,a) +^ (a,b) is epsilon-transitive epsilon-connected ordinal set
a +^ ((b,a) +^ (a,b)) is epsilon-transitive epsilon-connected ordinal set

((a +^ a),a) is epsilon-transitive epsilon-connected ordinal set

((a +^ b),a) is epsilon-transitive epsilon-connected ordinal set

((a *^ b),(a *^ b)) is epsilon-transitive epsilon-connected ordinal set

(a *^ b) +^ ((a,a) *^ b) is epsilon-transitive epsilon-connected ordinal set

((a,b) *^ b) +^ a is epsilon-transitive epsilon-connected ordinal set

(a,((a,b) *^ b)) is epsilon-transitive epsilon-connected ordinal set
((a,b) *^ b) +^ (a,b) is epsilon-transitive epsilon-connected ordinal set

(a,((a,a) *^ a)) is epsilon-transitive epsilon-connected ordinal set

(a,((a,a) *^ a)) is epsilon-transitive epsilon-connected ordinal set
((a,a) *^ a) +^ (a,a) is epsilon-transitive epsilon-connected ordinal set

((a,a) *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set

((a,a) *^ a) +^ b is epsilon-transitive epsilon-connected ordinal set

((b *^ a),a) is epsilon-transitive epsilon-connected ordinal set

((a *^ b),b) is epsilon-transitive epsilon-connected ordinal set
((a *^ b),b) is epsilon-transitive epsilon-connected ordinal set
((a *^ b),b) *^ b is epsilon-transitive epsilon-connected ordinal set
((a *^ b),(((a *^ b),b) *^ b)) is epsilon-transitive epsilon-connected ordinal set

((a *^ b),(a *^ b)) is epsilon-transitive epsilon-connected ordinal set
({},(((a *^ b),b) *^ b)) is epsilon-transitive epsilon-connected ordinal set

({},(({},a) *^ a)) is epsilon-transitive epsilon-connected ordinal set

(a,((a,{}) *^ {})) is epsilon-transitive epsilon-connected ordinal set

(a,((a,1) *^ 1)) is epsilon-transitive epsilon-connected ordinal set

a is set

On a is set
union (On a) is set
succ (union (On a)) is non empty set
{(union (On a))} is non empty set
(union (On a)) \/ {(union (On a))} is non empty set

{b} is non empty set
b \/ {b} is non empty set
a is set

{a} is non empty set
a \/ {a} is non empty set

rng b is set

a is set
b is set
b . b is set

{(b . {})} is non empty set

{a} is non empty set
a \/ {a} is non empty set

{b} is non empty set
b \/ {b} is non empty set

{(b +^ a)} is non empty set
(b +^ a) \/ {(b +^ a)} is non empty set

{a} is non empty set
a \/ {a} is non empty set

succ ((succ b) +^ a) is non empty epsilon-transitive epsilon-connected ordinal natural set
{((succ b) +^ a)} is non empty set
((succ b) +^ a) \/ {((succ b) +^ a)} is non empty set

succ (b +^ (succ a)) is non empty epsilon-transitive epsilon-connected ordinal natural set
{(b +^ (succ a))} is non empty set
(b +^ (succ a)) \/ {(b +^ (succ a))} is non empty set

{(b +^ {})} is non empty set
(b +^ {}) \/ {(b +^ {})} is non empty set

{(b +^ a)} is non empty set
(b +^ a) \/ {(b +^ a)} is non empty set

{b} is non empty set
b \/ {b} is non empty set

{a} is non empty set
a \/ {a} is non empty set

((a *^ (succ b)),(succ b)) is epsilon-transitive epsilon-connected ordinal natural set

((a *^ b),(a,(succ b))) is epsilon-transitive epsilon-connected ordinal natural set

{(a,b)} is non empty set
(a,b) \/ {(a,b)} is non empty set
((a *^ b),(succ (a,b))) is epsilon-transitive epsilon-connected ordinal natural set
((a *^ b),(a,b)) is epsilon-transitive epsilon-connected ordinal natural set
succ ((a *^ b),(a,b)) is non empty epsilon-transitive epsilon-connected ordinal natural set
{((a *^ b),(a,b))} is non empty set
((a *^ b),(a,b)) \/ {((a *^ b),(a,b))} is non empty set

(((a *^ b),b),a) is epsilon-transitive epsilon-connected ordinal natural set
succ (((a *^ b),b),a) is non empty epsilon-transitive epsilon-connected ordinal natural set
{(((a *^ b),b),a)} is non empty set
(((a *^ b),b),a) \/ {(((a *^ b),b),a)} is non empty set

(((succ a) *^ b),a) is epsilon-transitive epsilon-connected ordinal natural set
succ (((succ a) *^ b),a) is non empty epsilon-transitive epsilon-connected ordinal natural set
{(((succ a) *^ b),a)} is non empty set
(((succ a) *^ b),a) \/ {(((succ a) *^ b),a)} is non empty set
(((succ a) *^ b),(succ a)) is epsilon-transitive epsilon-connected ordinal natural set