Metamath Proof Explorer

Theorem alephislim

Description: Every aleph is a limit ordinal. (Contributed by NM, 11-Nov-2003)

Ref Expression
Assertion alephislim 
|- ( A e. On <-> Lim ( aleph ` A ) )

Proof

Step Hyp Ref Expression
1 alephgeom 
 |-  ( A e. On <-> _om C_ ( aleph ` A ) )
2 cardlim 
 |-  ( _om C_ ( card ` ( aleph ` A ) ) <-> Lim ( card ` ( aleph ` A ) ) )
3 alephcard 
 |-  ( card ` ( aleph ` A ) ) = ( aleph ` A )
4 3 sseq2i 
 |-  ( _om C_ ( card ` ( aleph ` A ) ) <-> _om C_ ( aleph ` A ) )
5 limeq 
 |-  ( ( card ` ( aleph ` A ) ) = ( aleph ` A ) -> ( Lim ( card ` ( aleph ` A ) ) <-> Lim ( aleph ` A ) ) )
6 3 5 ax-mp 
 |-  ( Lim ( card ` ( aleph ` A ) ) <-> Lim ( aleph ` A ) )
7 2 4 6 3bitr3i 
 |-  ( _om C_ ( aleph ` A ) <-> Lim ( aleph ` A ) )
8 1 7 bitri 
 |-  ( A e. On <-> Lim ( aleph ` A ) )