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	⊢ ¬ ω ∈ 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		nnfi	⊢ ( 𝑥 ∈ ω → 𝑥 ∈ Fin )
10		ensymfib	⊢ ( 𝑥 ∈ Fin → ( 𝑥 ≈ ω ↔ ω ≈ 𝑥 ) )
11	9 10	syl	⊢ ( 𝑥 ∈ ω → ( 𝑥 ≈ ω ↔ ω ≈ 𝑥 ) )
12	11	biimpar	⊢ ( ( 𝑥 ∈ ω ∧ ω ≈ 𝑥 ) → 𝑥 ≈ ω )
13		pssinf	⊢ ( ( 𝑥 ⊊ ω ∧ 𝑥 ≈ ω ) → ¬ ω ∈ Fin )
14	8 12 13	syl2an2r	⊢ ( ( 𝑥 ∈ ω ∧ ω ≈ 𝑥 ) → ¬ ω ∈ Fin )
15	14	rexlimiva	⊢ ( ∃ 𝑥 ∈ ω ω ≈ 𝑥 → ¬ ω ∈ Fin )
16	1 15	sylbi	⊢ ( ω ∈ Fin → ¬ ω ∈ Fin )
17		pm2.01	⊢ ( ( ω ∈ Fin → ¬ ω ∈ Fin ) → ¬ ω ∈ Fin )
18	16 17	ax-mp	⊢ ¬ ω ∈ Fin