CARDINALITY - without Axiom ZF9

Definition S.CR.1
Let X,Y be sets.
We define that |X|=|Y|
if and only if 
there exist a function f:X->Y and f is 1-1 and "onto".

Notice that we don't define the operator |.|. 
We define the predicate P(X,Y)="|X|=|Y|".   

Definition S.CR.2
Let X,Y be sets.
We define that |X|<=|Y|
if and only if
there exist a function f:X->Y and f is 1-1.

Lemma S.CR.3
If X,Y are sets, X c Y and |Y|<=|X| then |X|=|Y|.

By assumption we have f:Y-1-1->X.

Let F[A] = X\f(Y\A) for all A c X.
Notice that 
By Theorem S.IS.4 
if A c B then F[A] c F[B].

Let W = {A:-P(X)|A c F(A)}.
Let E = u(W).

We will show that E:-W.
We have to show that E c X\f(Y\E).

Take any e:-E.
We have an A:-W such that e:-A.
Since A:-W, A c F[A].
And since A:-W, A c E.
Then F[A] c F[E].
Thus e:-F[E].
We have showed that E:-W.

We will show that F[E] = E.
Since E c F[E], F[E] c F[F[E]].
Hence F[E]:-W. So F[E] c E.
Thus E = F[E].

We have E = X\f(Y\E).
So X\E = f(Y\E).

Let g:Y->X such that

        / x    for x:-E, 
g(x) = {
        \ f(x) for x:-Y\E.

We will show that g:Y-1-1-onto->X.

Take any x1,x2:-Y such that x1 != x2.
If x1:-E and x2:-Y\E 
then g(x1) = x1 and g(x2):-f(Y\E)=X\E.
And then g(x1) != g(x2).
If x1,x2:-E then x1=g(x1)!=g(x2)=x2.
If x1,x2:-Y\E then f(x1)=g(x1)!=g(x2)=f(x2)
because f is 1-1.
Thus g:Y-1-1->X.
We have shown (1-1).

g(Y) = g((Y\E) u E) = g(Y\E) u g(E) =
f(Y\E) u E = X\E u E = X.
We have shown (onto).

We have shown that g:X-1-1-onto->Y.
Thus |X|=|Y|.

Theorem S.CR.4
If X,Y are sets then the statements below hold.

(1) |X|=|X|,
(2) |X|=|Y| <=> |Y|=|X|,
(3) |X|=|Y| and |Y|=|Z| => |X|=|Z|,

(4)  X c Y => |X|<=|Y|,
(5) |X|=|Y| and |Y|<=|Z| => |X|<=|Z|,
(6) |X|=|Y| and |Z|<=|Y| => |Z|<=|X|,

(7) |X|<=|X|,
(8) |X|<=|Y| and |Y|<=|Z| => |X|<=|Z|,
(9) |X|<=|Y| and |Y|<=|X| => |X|=|Y|.

Let f:X->X such that /\(x:-X) 
f(x)=x. Thus f:X-1-1-onto->Y.

If f:X-1-1-onto->Y then f^(-1):Y-1-1-onto->X.

If f:X-1-1-onto->Y and g:Y-1-1-onto->Z
then gof:X-1-1-onto->Z.

Let f:X->Y such that /\(x:-X) f(x)=x.
Thus f:X-1-1->Y.

If f:X-1-1-onto->Y and g:Y-1-1->Z
then gof:X-1-1->Z.

If f:X-1-1-onto->Y and g:Z-1-1->Y.
Then (f^(-1))o(g):Z-1-1->X.

Let f:X->X such that /\(x:-X) 
f(x)=x. Thus f:X-1-1->Y.

If f:X-1-1->Y and g:Y-1-1->Z
then gof:X-1-1->Z.

We have f:X-1-1->Y and g:Y-1-1-X.
Notice that f:X-1-1-onto->f(X).
So |f(X)|=|X|.
Since |Y|<=|X|, |Y|<=|f(X)| by (5).
Since f(X) c Y, |Y|=|f(X)| by Lemma S.CR.3.
By (3) |Y|=|X|.

AC.Theorem S.CR.5
If X,Y are sets then |X|<=|Y| or |Y|<=|X|.

Assume that the Axiom of Choice holds.
We will use Zorn's Lemma.

(*)Assume that !(|Y|<=|X|).
Let P = {f:-P(XxY)|f is 1-1}.
Notice that (P,c) is a partially ordered set.

Take any chain L c P.
By Theorem S.C.14 u(L) is a function.
We will show that u(L):-P.

Let g = u(L).
Take any x1,x2:-X such that g(x1) = g(x2).
So there exists y:-Y such that
(x1,y):-g and (x2,y):-g.
We have h1,h2:-L such that (x1,y):-h1 and (x2,y):-h2.
Since L is a chain, (h1 u h2) = h1 or (h1 u h2) = h2.
Hence (h1 u h2):-L and (h1 u h2)(x1) = (h1 u h2)(x2).
Since (h1 u h2):-P, x1 = x2.
Thus u(L) is 1-1.
We have shown that u(L):-P.

It is obvious that /\(g:-L) g c u(L).
Recall that L was arbitralily chosen.
Then for every chain in P 
there exists an upper bound in P.
Now by Zorn's Lemma we have an f:-P
such that /\(g:-P) f c g => f=g.
By assumption (*) f is not "onto".
If it was it would be f^(-1):Y-1-1->X and 
then |Y|<=|X|.

We will show that f:X-1-1->Y.
It is enough to show that /\(x:-X)\/(y:-Y) (x,y):-f.
Assume to the contrary that we have x0:-X such that
for every y:-Y !( (x,y):-f ).
Since f is not "onto", we have 
y0:-Y such that /\(x:-X) !( (x,y0):-f ).
Let g = f u {(x0,y0)}.
Notice that g is a function and g is 1-1.
Then g:-P and f c g. So g = f. Contradiction.
So /\(x:-X)\/(y:-Y) (x,y):-f.
Thus f:X-1-1->Y. 

We assumed that !( |Y|<=|X| ) and
and we have shown that |X|<=|Y|.
The proof is complete.  
Definition S.CR.6
Let X,Y be sets.
We define that
|X|<|Y| if and only if |X|<=|Y| and !(|X|=|Y|).

Theorem S.CR.7
If X is a set then |X|<|P(X)|.

Assume to the contrary that we have f:X-onto->P(X).
Let A = {x:-X | !(x:-f(x))}.
Since f is onto, we have a:-X
such that f(a)=A.

If a:-A then a:-f(a) and then !(a:-A).
If !(a:-A) then !(a:-f(a)) and then a:-A.
Thus !(|X|=|P(X)|).

Let g:X->P(X) such that /\(x:-X) g(x)={x}.
So g:X-1-1->P(X).
Thus |X|<=|P(X)|.

We have proved that |X|<|P(X)|.