Metamath Proof Explorer


Theorem alephsson

Description: The class of transfinite cardinals (the range of the aleph function) is a subclass of the class of ordinal numbers. (Contributed by NM, 11-Nov-2003)

Ref Expression
Assertion alephsson
|- ran aleph C_ On

Proof

Step Hyp Ref Expression
1 isinfcard
 |-  ( ( _om C_ x /\ ( card ` x ) = x ) <-> x e. ran aleph )
2 cardon
 |-  ( card ` x ) e. On
3 eleq1
 |-  ( ( card ` x ) = x -> ( ( card ` x ) e. On <-> x e. On ) )
4 2 3 mpbii
 |-  ( ( card ` x ) = x -> x e. On )
5 4 adantl
 |-  ( ( _om C_ x /\ ( card ` x ) = x ) -> x e. On )
6 1 5 sylbir
 |-  ( x e. ran aleph -> x e. On )
7 6 ssriv
 |-  ran aleph C_ On