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	$⊢ ω \in Inacc$

Proof

Step	Hyp	Ref	Expression
1		peano1	$⊢ \emptyset \in ω$
2	1	ne0ii	$⊢ ω \neq \emptyset$
3		cfom	$⊢ cf (ω) = ω$
4		nnfi	$⊢ x \in ω \to x \in Fin$
5		pwfi	$⊢ x \in Fin \leftrightarrow 𝒫 x \in Fin$
6	4 5	sylib	$⊢ x \in ω \to 𝒫 x \in Fin$
7		isfinite	$⊢ 𝒫 x \in Fin \leftrightarrow 𝒫 x ≺ ω$
8	6 7	sylib	$⊢ x \in ω \to 𝒫 x ≺ ω$
9	8	rgen	$⊢ \forall x \in ω 𝒫 x ≺ ω$
10		elina	$⊢ ω \in Inacc \leftrightarrow (ω \neq \emptyset \land cf (ω) = ω \land \forall x \in ω 𝒫 x ≺ ω)$
11	2 3 9 10	mpbir3an	$⊢ ω \in Inacc$

Metamath Proof Explorer

Theorem omina

Proof