ominf

Description: The set of natural numbers is infinite. Corollary 6D(b) of Enderton p. 136. (Contributed by NM, 2-Jun-1998)

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

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		ensym	$⊢ ω \approx x \to x \approx ω$
10		pssinf	$⊢ (x \subset ω \land x \approx ω) \to \neg ω \in Fin$
11	8 9 10	syl2an	$⊢ (x \in ω \land ω \approx x) \to \neg ω \in Fin$
12	11	rexlimiva	$⊢ \exists x \in ω ω \approx x \to \neg ω \in Fin$
13	1 12	sylbi	$⊢ ω \in Fin \to \neg ω \in Fin$
14		pm2.01	$⊢ (ω \in Fin \to \neg ω \in Fin) \to \neg ω \in Fin$
15	13 14	ax-mp	$⊢ \neg ω \in Fin$

Metamath Proof Explorer