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		ordom	$⊢ Ord ω$
4		ordirr	$⊢ Ord ω \to \neg ω \in ω$
5	3 4	ax-mp	$⊢ \neg ω \in ω$
6	5	a1i	$⊢ ⊤ \to \neg ω \in ω$
7		omex	$⊢ ω \in V$
8	7	a1i	$⊢ ⊤ \to ω \in V$
9		bj-pinftyccb	$⊢ +\infty \in \overline{ℂ}$
10	9	a1i	$⊢ ⊤ \to +\infty \in \overline{ℂ}$
11	2 6 8 10	bj-fvmptunsn1	$⊢ ⊤ \to i_{ω↪ℕ} (ω) = +\infty$
12	11	mptru	$⊢ i_{ω↪ℕ} (ω) = +\infty$

Metamath Proof Explorer