Metamath Proof Explorer

Theorem onssnum

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

Ref Expression
Assertion onssnum 
|- ( ( A e. V /\ A C_ On ) -> A e. dom card )

Proof

Step Hyp Ref Expression
1 uniexg 
 |-  ( A e. V -> U. A e. _V )
2 ssorduni 
 |-  ( A C_ On -> Ord U. A )
3 elong 
 |-  ( U. A e. _V -> ( U. A e. On <-> Ord U. A ) )
4 3 biimpar 
 |-  ( ( U. A e. _V /\ Ord U. A ) -> U. A e. On )
5 1 2 4 syl2an 
 |-  ( ( A e. V /\ A C_ On ) -> U. A e. On )
6 onsuc 
 |-  ( U. A e. On -> suc U. A e. On )
7 onenon 
 |-  ( suc U. A e. On -> suc U. A e. dom card )
8 5 6 7 3syl 
 |-  ( ( A e. V /\ A C_ On ) -> suc U. A e. dom card )
9 onsucuni 
 |-  ( A C_ On -> A C_ suc U. A )
10 9 adantl 
 |-  ( ( A e. V /\ A C_ On ) -> A C_ suc U. A )
11 ssnum 
 |-  ( ( suc U. A e. dom card /\ A C_ suc U. A ) -> A e. dom card )
12 8 10 11 syl2anc 
 |-  ( ( A e. V /\ A C_ On ) -> A e. dom card )