Metamath Proof Explorer


Theorem omina

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 ω ∈ Inacc

Proof

Step Hyp Ref Expression
1 peano1 ∅ ∈ ω
2 1 ne0ii ω ≠ ∅
3 cfom ( cf ‘ ω ) = ω
4 nnfi ( 𝑥 ∈ ω → 𝑥 ∈ Fin )
5 pwfi ( 𝑥 ∈ Fin ↔ 𝒫 𝑥 ∈ Fin )
6 4 5 sylib ( 𝑥 ∈ ω → 𝒫 𝑥 ∈ Fin )
7 isfinite ( 𝒫 𝑥 ∈ Fin ↔ 𝒫 𝑥 ≺ ω )
8 6 7 sylib ( 𝑥 ∈ ω → 𝒫 𝑥 ≺ ω )
9 8 rgen 𝑥 ∈ ω 𝒫 𝑥 ≺ ω
10 elina ( ω ∈ Inacc ↔ ( ω ≠ ∅ ∧ ( cf ‘ ω ) = ω ∧ ∀ 𝑥 ∈ ω 𝒫 𝑥 ≺ ω ) )
11 2 3 9 10 mpbir3an ω ∈ Inacc