This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ¬ ω ∈ 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