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}\leftrightarrow \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}$$