elxnn0

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

		Ref	Expression
	Assertion	elxnn0	$⊢ A \in ℕ_{0}^{*} \leftrightarrow (A \in ℕ_{0} \lor A = +∞)$

Step	Hyp	Ref	Expression
1		df-xnn0	$⊢ ℕ_{0}^{*} = ℕ_{0} \cup \{+∞\}$
2	1	eleq2i	$⊢ A \in ℕ_{0}^{*} \leftrightarrow A \in (ℕ_{0} \cup \{+∞\})$
3		elun	$⊢ A \in (ℕ_{0} \cup \{+∞\}) \leftrightarrow (A \in ℕ_{0} \lor A \in \{+∞\})$
4		pnfex	$⊢ +∞ \in V$
5	4	elsn2	$⊢ A \in \{+∞\} \leftrightarrow A = +∞$
6	5	orbi2i	$⊢ (A \in ℕ_{0} \lor A \in \{+∞\}) \leftrightarrow (A \in ℕ_{0} \lor A = +∞)$
7	2 3 6	3bitri	$⊢ A \in ℕ_{0}^{*} \leftrightarrow (A \in ℕ_{0} \lor A = +∞)$

Metamath Proof Explorer