$\omega_1$ is uncountable, every ordinal below it is at most countable, it is a cardinal and a limit ordinal, and its existence is a theorem of ZF

Claim (a), forwards: if $f : \alpha \to \mathbb{N}$ is injective then $\alpha \approx f[\alpha] \subseteq \mathbb{N}$ by [L5], and $f[\alpha]$ is at most countable by [L3], so $\alpha$ is at most countable by [L2] and transitivity of $\approx$.

Claim (a), backwards: if $\alpha$ is at most countable then $\alpha \approx n$ for some $n \in \mathbb{N}$ or $\alpha \approx \mathbb{N}$; a bijection $\alpha \to n$ followed by the inclusion $n \subseteq \mathbb{N}$ is an injection $\alpha \to \mathbb{N}$ by [L8], and a bijection $\alpha \to \mathbb{N}$ is one outright.

$\omega \in \omega_1$: the identity is an injection $\omega \to \mathbb{N}$, so $\omega \ne \omega_1$ by [L1]; and $\omega_1 \in \omega$ or $\omega_1 = \omega$ would give $\omega_1 \subseteq \omega$ by [L7] and hence an injection $\omega_1 \to \mathbb{N}$ by inclusion, which [L1] forbids; so $\omega \in \omega_1$ by trichotomy.

Claim (b): $\omega_1$ does not inject into $\mathbb{N}$ by [L1], so it is not at most countable by step 1.2, that is, it is uncountable.

Claim (c): every $\alpha \in \omega_1$ injects into $\mathbb{N}$ by [L1], hence is at most countable by step 1.1; and by [L7] any uncountable ordinal $\gamma$ satisfies $\omega_1 \le \gamma$, since $\gamma \in \omega_1$ would make $\gamma$ at most countable.

Claim (d): suppose $\alpha \in \omega_1$ satisfies $\alpha \approx \omega_1$; then $\alpha$ is at most countable by step 2.2, so $\omega_1$ is at most countable by [L2] and symmetry of $\approx$, contradicting step 2.1; hence $\omega_1$ is a cardinal in the sense of [L6].

Claim (e): $\omega_1 \ne 0$ by step 1.3, since $\omega \in \omega_1$; and $\omega_1$ is not a successor, for if $\omega_1 = \delta^{+}$ then $\omega \in \delta^{+}$ gives $\omega \subseteq \delta$ by [L7], so $\delta$ is a nonempty ordinal in $\omega_1$ and is therefore at most countable by step 2.2, so [L4] supplies a surjection $s : \mathbb{N} \to \delta$, and the function $t : \mathbb{N} \to \delta^{+}$ with $t(0) = \delta$ and $t(\sigma(n)) = s(n)$ is a surjection onto $\delta^{+} = \delta \cup \{\delta\}$, making $\omega_1$ at most countable by [L4] and contradicting step 2.1; so $\omega_1$ is a limit ordinal by [L7].

Claims (a) to (e) are established, and every step used only Hartogs: an ordinal that does not inject into a given set, Every subset of an at most countable set is at most countable and A nonempty set is at most countable iff it is a surjective image of $\mathbb{N}$, all of which are choice free, so the whole statement is a theorem of ZF.