This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 onsuc ⊢ ( ∪ 𝐴 ∈ 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 )