Description: _om is a strongly inaccessible cardinal. (Many definitions of "inaccessible" explicitly disallow _om as an inaccessible cardinal, but this choice allows us to reuse our results for inaccessibles for _om .) (Contributed by Mario Carneiro, 29-May-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | omina | |- _om e. Inacc |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | peano1 | |- (/) e. _om |
|
| 2 | 1 | ne0ii | |- _om =/= (/) |
| 3 | cfom | |- ( cf ` _om ) = _om |
|
| 4 | nnfi | |- ( x e. _om -> x e. Fin ) |
|
| 5 | pwfi | |- ( x e. Fin <-> ~P x e. Fin ) |
|
| 6 | 4 5 | sylib | |- ( x e. _om -> ~P x e. Fin ) |
| 7 | isfinite | |- ( ~P x e. Fin <-> ~P x ~< _om ) |
|
| 8 | 6 7 | sylib | |- ( x e. _om -> ~P x ~< _om ) |
| 9 | 8 | rgen | |- A. x e. _om ~P x ~< _om |
| 10 | elina | |- ( _om e. Inacc <-> ( _om =/= (/) /\ ( cf ` _om ) = _om /\ A. x e. _om ~P x ~< _om ) ) |
|
| 11 | 2 3 9 10 | mpbir3an | |- _om e. Inacc |