Description: A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | winainf | |- ( A e. InaccW -> _om C_ A ) |
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 ) |