Metamath Proof Explorer


Theorem winainf

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

Ref Expression
Assertion winainf
|- ( A e. InaccW -> _om C_ A )

Proof

Step Hyp Ref Expression
1 elwina
 |-  ( A e. InaccW <-> ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A E. y e. A x ~< y ) )
2 cfon
 |-  ( cf ` A ) e. On
3 eleq1
 |-  ( ( cf ` A ) = A -> ( ( cf ` A ) e. On <-> A e. On ) )
4 2 3 mpbii
 |-  ( ( cf ` A ) = A -> A e. On )
5 winainflem
 |-  ( ( A =/= (/) /\ A e. On /\ A. x e. A E. y e. A x ~< y ) -> _om C_ A )
6 4 5 syl3an2
 |-  ( ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A E. y e. A x ~< y ) -> _om C_ A )
7 1 6 sylbi
 |-  ( A e. InaccW -> _om C_ A )