NATURAL INFINITE SET

Definition S.N.1
Let Tr(z) means 
O:-z and (/\(x) x:-z => (x u {x}):-z).

Remark: We don't define a function Tr(z).
We just compress the above formula into Tr(z).

Theorem S.N.2
If K is a set such that K != O and /\(z:-K) Tr(z) 
then Tr(n(K)).

Remark: In particular if Tr(A) and Tr(B) then Tr(A n B).

Proof of Theorem S.N.2
It is obvious that O:-n(K).
Now take any x:-n(K). We have /\(z:-K) x:-z.
Take any z:-K. 
Since Tr(z) and x:-z, (x u {x}):-z.
Since z:-K was arbitrarily chosen, (x u {x}):-n(K).
We have proved that 
O:-n(K) and (/\(x) x:-n(K) => (x u {x}):-n(K)).

Theorem S.N.3
There is a unique set M such that 
Tr(M) and (/\(X) Tr(X) => M c X).

Proof
By Axiom ZF7 there exists a set m such that Tr(m).
Let K = {A:-P(m)|Tr(A)}
Let M = n(K). By Theorem S.N.2 Tr(M).
It is obvious that M c m.
Take any set X such that Tr(X).
By Theorem S.N.2 Tr(X n M).
Notice that X n M c m.
Hence (X n M):-K. Thus M c X n M c X.   
We have shown that /\(X) Tr(X) => M c X.

The proof of uniqueness.
Assume that we have a set M1 such that 
Tr(M1) and (/\(X) Tr(X) => M1 c X).
Then M1 c M.
By on the other hand, M c M1.
Thus M = M1.

Definition S.N.4 - Natural Infinite Set
We define that
M is a natural infinite set if and only if
Tr(M) and (/\(X) Tr(X) => M c X).

Remark: 
By Theorem S.N.3 there is only one natural infinite set.

Theorem S.N.5
If M is natural infinite set and x:-M then x is an ordinal.

Proof
Let K = {x:-M | x is an ordinal}.
It is easy to verify that O:-K.
We will show that /\(x:-K) x u {x} :- K.

Take any x:-K such that x is an ordinal.
We will show that x u {x} is an ordinal.
By Theorem S.CO.6 x is a set of ordinals.
Since x is an ordinal, 
x u {x} is aloso a set of ordinals.

By Theorem S.CO.11 and Theorem S.CO.13 
it is enough to show that 
/\(z :- x u {x}) z c x u {x}.

Take any z :- x u {x}.
If z:-x then z c x c x u {x}.
If z = x then x c x u {x}.
Hence z c x u {x}.

We have shown that x u {x} is an ordinal.
So x u {x}:-K.

We have shown that /\(x:-K) x u {x} :- K.
Since M is a natural infinite set, M = K.

Theorem S.N.6
If M is an natural infinite set then M is an ordinal.

Proof
Let K = {x:-M|x c M}.
It is obvious that O:-K.
We will show that /\(x:-K) x u {x}:-K.

Take any x:-K.
We have that x c K.
Hence x u {x} c K.
Thus x u {x}:-K.
We have shown that /\(x:-K) x u {x} :- K.
Since M is a natural infinite set, M = K.
Hence /\(x:-M) x c M.
Now by Theorem S.N.5 and Theorem S.CO.15
M is an ordinal.

Definition S.N.7 - Countability
Let x be a set. Let M be a natural infinite set.
We define that x is countable if and only if
\/(y) y c M and |y|=|x|.

Remark: For definition of |x|=|y| go to Cardinality.

Definition S.N.8 - Finiteness
Let x be a set. Let M be a natural infinite set.
We define that x is finite if and only if
\/(y) y :- M and |y|=|x|.

Remark: For definition of |x|=|y| go to Cardinality.