# Metamath Proof Explorer

## Theorem onssnum

Description: All subsets of the ordinals are numerable. (Contributed by Mario Carneiro, 12-Feb-2013)

Ref Expression
Assertion onssnum ${⊢}\left({A}\in {V}\wedge {A}\subseteq \mathrm{On}\right)\to {A}\in \mathrm{dom}\mathrm{card}$

### Proof

Step Hyp Ref Expression
1 uniexg ${⊢}{A}\in {V}\to \bigcup {A}\in \mathrm{V}$
2 ssorduni ${⊢}{A}\subseteq \mathrm{On}\to \mathrm{Ord}\bigcup {A}$
3 elong ${⊢}\bigcup {A}\in \mathrm{V}\to \left(\bigcup {A}\in \mathrm{On}↔\mathrm{Ord}\bigcup {A}\right)$
4 3 biimpar ${⊢}\left(\bigcup {A}\in \mathrm{V}\wedge \mathrm{Ord}\bigcup {A}\right)\to \bigcup {A}\in \mathrm{On}$
5 1 2 4 syl2an ${⊢}\left({A}\in {V}\wedge {A}\subseteq \mathrm{On}\right)\to \bigcup {A}\in \mathrm{On}$
6 suceloni ${⊢}\bigcup {A}\in \mathrm{On}\to \mathrm{suc}\bigcup {A}\in \mathrm{On}$
7 onenon ${⊢}\mathrm{suc}\bigcup {A}\in \mathrm{On}\to \mathrm{suc}\bigcup {A}\in \mathrm{dom}\mathrm{card}$
8 5 6 7 3syl ${⊢}\left({A}\in {V}\wedge {A}\subseteq \mathrm{On}\right)\to \mathrm{suc}\bigcup {A}\in \mathrm{dom}\mathrm{card}$
9 onsucuni ${⊢}{A}\subseteq \mathrm{On}\to {A}\subseteq \mathrm{suc}\bigcup {A}$
10 9 adantl ${⊢}\left({A}\in {V}\wedge {A}\subseteq \mathrm{On}\right)\to {A}\subseteq \mathrm{suc}\bigcup {A}$
11 ssnum ${⊢}\left(\mathrm{suc}\bigcup {A}\in \mathrm{dom}\mathrm{card}\wedge {A}\subseteq \mathrm{suc}\bigcup {A}\right)\to {A}\in \mathrm{dom}\mathrm{card}$
12 8 10 11 syl2anc ${⊢}\left({A}\in {V}\wedge {A}\subseteq \mathrm{On}\right)\to {A}\in \mathrm{dom}\mathrm{card}$