Metamath Proof Explorer

Theorem ominf

Description: The set of natural numbers is infinite. Corollary 6D(b) of Enderton p. 136. (Contributed by NM, 2-Jun-1998) Avoid ax-pow . (Revised by BTernaryTau, 2-Jan-2025)

		Ref	Expression
	Assertion	ominf	$⊢ \neg ω \in Fin$

Proof

Step	Hyp	Ref	Expression
1		isfi	$⊢ ω \in Fin \leftrightarrow \exists x \in ω ω \approx x$
2		nnord	$⊢ x \in ω \to Ord x$
3		ordom	$⊢ Ord ω$
4		ordelssne	$⊢ (Ord x \land Ord ω) \to (x \in ω \leftrightarrow (x \subseteq ω \land x \neq ω))$
5	2 3 4	sylancl	$⊢ x \in ω \to (x \in ω \leftrightarrow (x \subseteq ω \land x \neq ω))$
6	5	ibi	$⊢ x \in ω \to (x \subseteq ω \land x \neq ω)$
7		df-pss	$⊢ x \subset ω \leftrightarrow (x \subseteq ω \land x \neq ω)$
8	6 7	sylibr	$⊢ x \in ω \to x \subset ω$
9		nnfi	$⊢ x \in ω \to x \in Fin$
10		ensymfib	$⊢ x \in Fin \to (x \approx ω \leftrightarrow ω \approx x)$
11	9 10	syl	$⊢ x \in ω \to (x \approx ω \leftrightarrow ω \approx x)$
12	11	biimpar	$⊢ (x \in ω \land ω \approx x) \to x \approx ω$
13		pssinf	$⊢ (x \subset ω \land x \approx ω) \to \neg ω \in Fin$
14	8 12 13	syl2an2r	$⊢ (x \in ω \land ω \approx x) \to \neg ω \in Fin$
15	14	rexlimiva	$⊢ \exists x \in ω ω \approx x \to \neg ω \in Fin$
16	1 15	sylbi	$⊢ ω \in Fin \to \neg ω \in Fin$
17		pm2.01	$⊢ (ω \in Fin \to \neg ω \in Fin) \to \neg ω \in Fin$
18	16 17	ax-mp	$⊢ \neg ω \in Fin$