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ω↪ℕ ‘ ω ) = +∞

Proof

Step	Hyp	Ref	Expression
1		df-bj-iomnn	⊢ iω↪ℕ = ( ( 𝑛 ∈ ω ↦ ⟨ [ ⟨ { 𝑟 ∈ Q ∣ 𝑟 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R , 0R ⟩ ) ∪ { ⟨ ω , +∞ ⟩ } )
2	1	a1i	⊢ ( ⊤ → iω↪ℕ = ( ( 𝑛 ∈ ω ↦ ⟨ [ ⟨ { 𝑟 ∈ Q ∣ 𝑟 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R , 0R ⟩ ) ∪ { ⟨ ω , +∞ ⟩ } ) )
3		elirr	⊢ ¬ ω ∈ ω
4	3	a1i	⊢ ( ⊤ → ¬ ω ∈ ω )
5		omex	⊢ ω ∈ V
6	5	a1i	⊢ ( ⊤ → ω ∈ V )
7		bj-pinftyccb	⊢ +∞ ∈ ℂ̅
8	7	a1i	⊢ ( ⊤ → +∞ ∈ ℂ̅ )
9	2 4 6 8	bj-fvmptunsn1	⊢ ( ⊤ → ( iω↪ℕ ‘ ω ) = +∞ )
10	9	mptru	⊢ ( iω↪ℕ ‘ ω ) = +∞