ORDINALS AND CARDINALS - with Axiom ZF9

Theorem S.CO.1
If x,y are sets and x:-y then !(y:-x).

Proof
Assume to the contrary that y:-x.
Then we have x:-y and y:-x.
Let z = {x,y}. By Axiom ZF9 we have
\/(a:-z) a n z = O.
But y :- x n {x,y} and x :- y n {x,y}. Contradiction.
Thus !(y:-x).

Theorem S.CO.2
If x is a set then !(x:-x).

Proof
Assume that x:-x. 
Then by Theorem S.CO.1 !(x:-x). Contradiction.
 
Definition S.CO.3 - Ordinal
Let X be a set.
We define that X is an ordinal if and only if
(1) /\(x,y:-X) x:-y or y:-x or x = y,
(2) /\(x,y,z:-X) (x:-y and y:-z) => x:-z,
(3) /\(x:-X) x c X.

Theorem S.CO.4
If x is an ordinal, y c x and y != O then
\/(e:-y)/\(z:-y) e:-z or e = z.

Proof
By Axiom ZF9 
we have e:-y such that e n y = O.
Take any z:-y.
Since e n y = O, !(z:-e).
Since x is an ordinal, e:-z or e = z.
We have proved that
\/(e:-y)/\(z:-y) e:-z or e = z.

Theorem S.CO.5
If x is an ordinal, a,b:-x and a:-b 
then a c b.

Proof
Take any a,b:-x such that a:-b.
Take any t:-a.
By Definition S.CO.3 t:-b.
Thus a c b.

Theorem S.CO.6
If x is an ordinal and y:-x then y is an ordinal.

Proof
By Definition S.CO.3 y c x.
Hence /\(p,q:-y) p:-q or q:-p or p = q,
/\(p,q,r:-y) (p:-q and q:-r) => p:-r.
We have to show that /\(z:-y) z c y.

Take any z:-y. Since y c x, z:-x.
Now we have z,y:-x and z:-y.
By Theorem S.CO.5 z c y.

We have proved that y is an ordinal.

Theorem S.CO.7
If x is an ordinal and a,b:-x
then a c b <=> a:-b or a = b.

Proof
By Theorem S.CO.5 it is enough to show that
a c b => a:-b or a = b.

Assume that a c b.
Assume to the contrary that !(a:-b) and a != b.
Since x is an ordinal b:-a.
Then by Theorem S.CO.5 b c a.
Hence a = b. Contradiction.

We have shown that a c b => a:-b or a = b.

Theorem S.CO.8
If X is an ordinal and E = {(a,b):-XxX | a c b}
then (X,E) is a well ordered set.

Proof
By Theorem S.CO.7, Theorem S.CO.4 and Definition S.CO.3.

Remark: If we write that (X,c) is a well ordered set
we mean that (X,E) with E = {(a,b):-XxX | a c b} is 
a well ordered set.   

Theorem S.CO.9
If x and y are ordinals 
then (x n y) is an initial segment of x in (x,c).

Proof
Take any a :- x n y.
Take any t:-x such that t c a.
We will show that t :- x n y.  
By Theorem S.CO.7 t = a or t:-a.
If a = t there is no problem.
Assume that t:-a.
Since x,y are ordinals, a c x n y.
Then t :- x n y.
Thus x n y is an initial segment of x in (x,c).

Theorem S.CO.10
If x and y are ordinals then x c y or y c x.

Proof
Assume to the contrary that !(x c y) and !(y c x).
Then x n y != x and x n y != y.

By Theorem S.CO.9 
x n y is an initial segment of x in (x,c).
Recall that x n y != x,
By Theorem S.O.8
we have r:-x such that 
x n y = {z:-x | z c r and z!=r} = {z:-x|z:-r}.
Since x is an ordinal, r c x.
Hence r = x n r = x n y.

By Theorem S.CO.9 
x n y is an initial segment of y in (y,c).
Recall that x n y != y,
By Theorem S.O.8
we have s:-y such that 
x n y = {z:-y | z c s and z!=s} = {z:-y|z:-s}.
Since y is an ordinal, s c y.
Hence s = s n y = x n y.

Thus s = r.
Since r:-x and s:-y, r:-x n y.
Then r:-r. Contradiction.

Theorem S.CO.11
If x and y are ordinals then x:-y or y:-x or y = x.

Proof
By Theorem S.CO.10 we can assume that x c y.
Then by Theorem S.CO.9 x is an initial segment of y.
If x = y there is no problem.
Assume that x != y.
Now by Theorem S.O.8 
we have r:-y such that x = {z:-y|z:-r}.
Since y is an ordinal r c y.
Hence x = y n r = r.
Thus x:-y.

Theorem S.CO.12
If x,y are ordinals then 
x:-y <=> x c y and x != y.

Proof
Assume that x c y and x != y.
By Theorem S.CO.11 x:-y or y:-x or x = y.
If y:-x then y:-y because x c y. Then contradiction.
Thus x:-y.

Assume that x:-y.
By Theorem S.CO.2 y != x.
By Theorem S.CO.10 we have x c y or y c x.
If y c x then x:-x because x:-y. Then contradiction.
Thus x c y.

Theorem S.CO.13
If x,y,z are ordinals and x:-y and y:-z then x:-z.

Proof
By S.CO.11 we have x c z and y c z.
Hence x c z.
If x = z then x:-y and y:-x. Then contradiction.
Hence x != z.
Thus By S.CO.11 x:-z.

Theorem S.CO.14
If y is a set such that /\(x:-y) x is an ordinal
then \/(e:-y)/\(z:-y) e:-z or e = z.

Proof
By Axiom ZF9 
we have e:-y such that e n y = O.
Take any z:-y.
Since e n y = O, !(z:-e).
Since z,e are ordinals, e:-z or e = z.
We have proved that
\/(e:-y)/\(z:-y) e:-z or e = z.

Theorem S.CO.15
If y is a set, 
/\(x:-y) ((x is an ordinal) and x c y)
then y is an ordinal.

Proof
By Theorem S.CO.11, Theorem S.CO.13 
and Definition S.CO.3.