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 )