Theorem pnf0xnn0

Description: Positive infinity is an extended nonnegative integer. (Contributed by AV, 10-Dec-2020)

	Ref	Expression
Assertion	pnf0xnn0	⊢ +∞ ∈ ℕ0*

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ +∞ = +∞
2	1	olci	⊢ ( +∞ ∈ ℕ0 ∨ +∞ = +∞ )
3		elxnn0	⊢ ( +∞ ∈ ℕ0* ↔ ( +∞ ∈ ℕ0 ∨ +∞ = +∞ ) )
4	2 3	mpbir	⊢ +∞ ∈ ℕ0*