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

Metamath Proof Explorer

Theorem nn0nepnf

Description: No standard nonnegative integer equals positive infinity. (Contributed by AV, 10-Dec-2020)

Ref Expression
Assertion nn0nepnf ( 𝐴 ∈ ℕ0 → 𝐴 ≠ +∞ )

Proof

Step Hyp Ref Expression
1 pnfnre ⊢ +∞ ∉ ℝ
2 1 neli ⊢ ¬ +∞ ∈ ℝ
3 nn0re ⊢ ( +∞ ∈ ℕ0 → +∞ ∈ ℝ )
4 2 3 mto ⊢ ¬ +∞ ∈ ℕ0
5 eleq1 ⊢ ( 𝐴 = +∞ → ( 𝐴 ∈ ℕ0 ↔ +∞ ∈ ℕ0 ) )
6 4 5 mtbiri ⊢ ( 𝐴 = +∞ → ¬ 𝐴 ∈ ℕ0 )
7 6 necon2ai ⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ≠ +∞ )