Theorem winacard

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

	Ref	Expression
Assertion	winacard	|- ( A e. InaccW -> ( card ` A ) = 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		cardcf	|- ( card ` ( cf ` A ) ) = ( cf ` A )
3		fveq2	|- ( ( cf ` A ) = A -> ( card ` ( cf ` A ) ) = ( card ` A ) )
4		id	|- ( ( cf ` A ) = A -> ( cf ` A ) = A )
5	2 3 4	3eqtr3a	|- ( ( cf ` A ) = A -> ( card ` A ) = A )
6	5	3ad2ant2	|- ( ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A E. y e. A x ~< y ) -> ( card ` A ) = A )
7	1 6	sylbi	|- ( A e. InaccW -> ( card ` A ) = A )