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 |
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 |