Ordinal type of the set of all countably infinite ordinals I can't understand a simple thing again, though found the similar questions here. Given the set $S$ of all countably infinite ordinals, how can we find its order type, or at least its cardinality? Do we need the axiom of choice or continuum hypothesis here? I've just managed to show $\omega_0\leq Ord(S)\leq\omega_1$.
P.S. I'm trying not to use the Neumann's approach (where ordinals are sets with the certain properties), considering the separate class of objects. It's also given that $\omega_1$ is the set of all countable (not necessarily infinite) ordinals.   
 A: We don't need the AC or CH. 
We can show that the collection of all well-orderings of $\mathbb N$ is a set (this makes essential use of power set). Each of these well-ordered sets corresponds to an ordinal - its order type (this makes essential use of replacement), and so (by replacement again) there is a set of all countable ordinals. This is a well-ordered set under the usual ordering $\in$, so it has an order type. We call this ordinal $\omega_1$ by definition.
$\omega_1$ is not countable since it is an ordinal, and by its definition any countable ordinal is strictly less.
So that's a complete answer to the question, and no choice was used. Where choice might get involved is when we want to say $\omega_1$ is the smallest uncountable cardinality. It's clearly the smallest uncountable ordinal, and so it can be embedded into any uncountable well-orderable set, so it is of size less than or equal to it. But we can't say every set is well-orderable without AC, and for instance, it is consistent with ZF that $\omega_1$ does not have an injection into the reals. (However it is provable in ZF that there is a surjection of the reals onto $\omega_1$.) It's also consistent that there are infinite sets that $\omega$ does not even inject into, so no AC also wrecks $\omega$'s status as the smallest infinite cardinality.
A: Here is an easy argument as to why the answer is $\omega_1$.
$\sf ZF$ (and in fact $\sf Z$) proves that given any two well-ordered sets, one is isomorphic to a unique initial segment of the other. That is, any two well-ordered sets are comparable.
By definition, $\omega_1$ is the smallest order type of an uncountable well-order. So if we prove that $\omega_1\setminus\omega$ is uncountable, then $\omega_1$ is isomorphic to an initial segment of it, but since it is also a subset of $\omega_1$, this initial segment cannot be a proper initial segment, as that would imply $\omega_1$ is isomorphic to a proper initial segment of itself which contradicts the uniqueness part of the above theorem.
But now it's easy. If $\omega_1\setminus\omega$ is countable, then $\omega_1$ is the union of two countable sets, which is indeed countable. That's not true, so the order type is $\omega_1$.

Finally, if you want an explicit argument, which you probably do, note that just like you can add an element to the bottom of $\omega$ and not change the order type, you can also add an $\omega$ sequence to the bottom of the ordinal $\omega\cdot\omega$ without changing the order type. Apply that sort of bijection on the initial segment that is $\omega\cdot\omega$ and the identity elsewhere, and you get your order isomorphism.
