onssnum

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

		Ref	Expression
	Assertion	onssnum	$⊢ (A \in V \land A \subseteq On) \to A \in dom card$

Step	Hyp	Ref	Expression
1		uniexg	$⊢ A \in V \to ⋃ A \in V$
2		ssorduni	$⊢ A \subseteq On \to Ord ⋃ A$
3		elong	$⊢ ⋃ A \in V \to (⋃ A \in On \leftrightarrow Ord ⋃ A)$
4	3	biimpar	$⊢ (⋃ A \in V \land Ord ⋃ A) \to ⋃ A \in On$
5	1 2 4	syl2an	$⊢ (A \in V \land A \subseteq On) \to ⋃ A \in On$
6		onsuc	$⊢ ⋃ A \in On \to suc ⋃ A \in On$
7		onenon	$⊢ suc ⋃ A \in On \to suc ⋃ A \in dom card$
8	5 6 7	3syl	$⊢ (A \in V \land A \subseteq On) \to suc ⋃ A \in dom card$
9		onsucuni	$⊢ A \subseteq On \to A \subseteq suc ⋃ A$
10	9	adantl	$⊢ (A \in V \land A \subseteq On) \to A \subseteq suc ⋃ A$
11		ssnum	$⊢ (suc ⋃ A \in dom card \land A \subseteq suc ⋃ A) \to A \in dom card$
12	8 10 11	syl2anc	$⊢ (A \in V \land A \subseteq On) \to A \in dom card$

Metamath Proof Explorer