Theorem onssnum

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

	Ref	Expression
Assertion	onssnum	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On ) → 𝐴 ∈ dom card )

Proof

Step	Hyp	Ref	Expression
1		uniexg	⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V )
2		ssorduni	⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )
3		elong	⊢ ( ∪ 𝐴 ∈ V → ( ∪ 𝐴 ∈ On ↔ Ord ∪ 𝐴 ) )
4	3	biimpar	⊢ ( ( ∪ 𝐴 ∈ V ∧ Ord ∪ 𝐴 ) → ∪ 𝐴 ∈ On )
5	1 2 4	syl2an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On ) → ∪ 𝐴 ∈ On )
6		suceloni	⊢ ( ∪ 𝐴 ∈ On → suc ∪ 𝐴 ∈ On )
7		onenon	⊢ ( suc ∪ 𝐴 ∈ On → suc ∪ 𝐴 ∈ dom card )
8	5 6 7	3syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On ) → suc ∪ 𝐴 ∈ dom card )
9		onsucuni	⊢ ( 𝐴 ⊆ On → 𝐴 ⊆ suc ∪ 𝐴 )
10	9	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On ) → 𝐴 ⊆ suc ∪ 𝐴 )
11		ssnum	⊢ ( ( suc ∪ 𝐴 ∈ dom card ∧ 𝐴 ⊆ suc ∪ 𝐴 ) → 𝐴 ∈ dom card )
12	8 10 11	syl2anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On ) → 𝐴 ∈ dom card )