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