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		ordom	⊢ Ord ω
4		ordirr	⊢ ( Ord ω → ¬ ω ∈ ω )
5	3 4	ax-mp	⊢ ¬ ω ∈ ω
6	5	a1i	⊢ ( ⊤ → ¬ ω ∈ ω )
7		omex	⊢ ω ∈ V
8	7	a1i	⊢ ( ⊤ → ω ∈ V )
9		bj-pinftyccb	⊢ +∞ ∈ ℂ̅
10	9	a1i	⊢ ( ⊤ → +∞ ∈ ℂ̅ )
11	2 6 8 10	bj-fvmptunsn1	⊢ ( ⊤ → ( iω↪ℕ ‘ ω ) = +∞ )
12	11	mptru	⊢ ( iω↪ℕ ‘ ω ) = +∞