Theorem 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	⊢ ¬ ω ∈ Fin

Proof

Step	Hyp	Ref	Expression
1		isfi	⊢ ( ω ∈ Fin ↔ ∃ 𝑥 ∈ ω ω ≈ 𝑥 )
2		nnord	⊢ ( 𝑥 ∈ ω → Ord 𝑥 )
3		ordom	⊢ Ord ω
4		ordelssne	⊢ ( ( Ord 𝑥 ∧ Ord ω ) → ( 𝑥 ∈ ω ↔ ( 𝑥 ⊆ ω ∧ 𝑥 ≠ ω ) ) )
5	2 3 4	sylancl	⊢ ( 𝑥 ∈ ω → ( 𝑥 ∈ ω ↔ ( 𝑥 ⊆ ω ∧ 𝑥 ≠ ω ) ) )
6	5	ibi	⊢ ( 𝑥 ∈ ω → ( 𝑥 ⊆ ω ∧ 𝑥 ≠ ω ) )
7		df-pss	⊢ ( 𝑥 ⊊ ω ↔ ( 𝑥 ⊆ ω ∧ 𝑥 ≠ ω ) )
8	6 7	sylibr	⊢ ( 𝑥 ∈ ω → 𝑥 ⊊ ω )
9		ensym	⊢ ( ω ≈ 𝑥 → 𝑥 ≈ ω )
10		pssinf	⊢ ( ( 𝑥 ⊊ ω ∧ 𝑥 ≈ ω ) → ¬ ω ∈ Fin )
11	8 9 10	syl2an	⊢ ( ( 𝑥 ∈ ω ∧ ω ≈ 𝑥 ) → ¬ ω ∈ Fin )
12	11	rexlimiva	⊢ ( ∃ 𝑥 ∈ ω ω ≈ 𝑥 → ¬ ω ∈ Fin )
13	1 12	sylbi	⊢ ( ω ∈ Fin → ¬ ω ∈ Fin )
14		pm2.01	⊢ ( ( ω ∈ Fin → ¬ ω ∈ Fin ) → ¬ ω ∈ Fin )
15	13 14	ax-mp	⊢ ¬ ω ∈ Fin