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