Metamath Proof Explorer

Theorem inawina

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

Ref Expression
Assertion inawina 
|- ( A e. Inacc -> A e. InaccW )

Proof

Step Hyp Ref Expression
1 cfon 
 |-  ( cf ` A ) e. On
2 eleq1 
 |-  ( ( cf ` A ) = A -> ( ( cf ` A ) e. On <-> A e. On ) )
3 1 2 mpbii 
 |-  ( ( cf ` A ) = A -> A e. On )
4 3 3ad2ant2 
 |-  ( ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A ~P x ~< A ) -> A e. On )
5 idd 
 |-  ( A e. On -> ( A =/= (/) -> A =/= (/) ) )
6 idd 
 |-  ( A e. On -> ( ( cf ` A ) = A -> ( cf ` A ) = A ) )
7 inawinalem 
 |-  ( A e. On -> ( A. x e. A ~P x ~< A -> A. x e. A E. y e. A x ~< y ) )
8 5 6 7 3anim123d 
 |-  ( A e. On -> ( ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A ~P x ~< A ) -> ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A E. y e. A x ~< y ) ) )
9 4 8 mpcom 
 |-  ( ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A ~P x ~< A ) -> ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A E. y e. A x ~< y ) )
10 elina 
 |-  ( A e. Inacc <-> ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A ~P x ~< A ) )
11 elwina 
 |-  ( A e. InaccW <-> ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A E. y e. A x ~< y ) )
12 9 10 11 3imtr4i 
 |-  ( A e. Inacc -> A e. InaccW )