Theorem 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_{\omega \hookrightarrow \mathbb{N}}\left(\mathrm{\omega }\right)=+\infty$$

Proof

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