Theorem xnn0nnn0pnf

Description: An extended nonnegative integer which is not a standard nonnegative integer is positive infinity. (Contributed by AV, 10-Dec-2020)

	Ref	Expression
Assertion	xnn0nnn0pnf	⊢ ( ( 𝑁 ∈ ℕ0* ∧ ¬ 𝑁 ∈ ℕ0 ) → 𝑁 = +∞ )

Proof

Step	Hyp	Ref	Expression
1		elxnn0	⊢ ( 𝑁 ∈ ℕ0* ↔ ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) )
2		pm2.53	⊢ ( ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) → ( ¬ 𝑁 ∈ ℕ0 → 𝑁 = +∞ ) )
3	1 2	sylbi	⊢ ( 𝑁 ∈ ℕ0* → ( ¬ 𝑁 ∈ ℕ0 → 𝑁 = +∞ ) )
4	3	imp	⊢ ( ( 𝑁 ∈ ℕ0* ∧ ¬ 𝑁 ∈ ℕ0 ) → 𝑁 = +∞ )