This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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