Metamath Proof Explorer


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 )