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 → 𝐴 ≠ +∞ )