Metamath Proof Explorer

Theorem winalim

Description: A weakly inaccessible cardinal is a limit ordinal. (Contributed by Mario Carneiro, 29-May-2014)

Ref Expression
Assertion winalim 
|- ( A e. InaccW -> Lim A )

Proof

Step Hyp Ref Expression
1 winainf 
 |-  ( A e. InaccW -> _om C_ A )
2 winacard 
 |-  ( A e. InaccW -> ( card ` A ) = A )
3 cardlim 
 |-  ( _om C_ ( card ` A ) <-> Lim ( card ` A ) )
4 sseq2 
 |-  ( ( card ` A ) = A -> ( _om C_ ( card ` A ) <-> _om C_ A ) )
5 limeq 
 |-  ( ( card ` A ) = A -> ( Lim ( card ` A ) <-> Lim A ) )
6 4 5 bibi12d 
 |-  ( ( card ` A ) = A -> ( ( _om C_ ( card ` A ) <-> Lim ( card ` A ) ) <-> ( _om C_ A <-> Lim A ) ) )
7 3 6 mpbii 
 |-  ( ( card ` A ) = A -> ( _om C_ A <-> Lim A ) )
8 2 7 syl 
 |-  ( A e. InaccW -> ( _om C_ A <-> Lim A ) )
9 1 8 mpbid 
 |-  ( A e. InaccW -> Lim A )