bj-iomnnom

Description: The canonical bijection from (om u. { om } ) onto ( NN0 u. { pinfty } ) maps _om to pinfty . (Contributed by BJ, 18-Feb-2023)

		Ref	Expression
	Assertion	bj-iomnnom	$⊢ i_{ω↪ℕ} (ω) = +\infty$

Step	Hyp	Ref	Expression
1		df-bj-iomnn	$⊢ i_{ω↪ℕ} = (n \in ω ⟼ ⟨[⟨\{r \in 𝑸 \| r <_{𝑸} ⟨suc n, 1_{𝑜}⟩\}, 1_{𝑷}⟩] ~_{𝑹}, 0_{𝑹}⟩) \cup \{⟨ω +\infty⟩\}$
2	1	a1i	$⊢ ⊤ \to i_{ω↪ℕ} = (n \in ω ⟼ ⟨[⟨\{r \in 𝑸 \| r <_{𝑸} ⟨suc n, 1_{𝑜}⟩\}, 1_{𝑷}⟩] ~_{𝑹}, 0_{𝑹}⟩) \cup \{⟨ω +\infty⟩\}$
3		elirr	$⊢ \neg ω \in ω$
4	3	a1i	$⊢ ⊤ \to \neg ω \in ω$
5		omex	$⊢ ω \in V$
6	5	a1i	$⊢ ⊤ \to ω \in V$
7		bj-pinftyccb	$⊢ +\infty \in \overline{ℂ}$
8	7	a1i	$⊢ ⊤ \to +\infty \in \overline{ℂ}$
9	2 4 6 8	bj-fvmptunsn1	$⊢ ⊤ \to i_{ω↪ℕ} (ω) = +\infty$
10	9	mptru	$⊢ i_{ω↪ℕ} (ω) = +\infty$

Metamath Proof Explorer