Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-iomnnom Structured version   Visualization version   GIF version

Theorem bj-iomnnom 34675
 Description: The canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}) maps ω to +∞. (Contributed by BJ, 18-Feb-2023.)
Assertion
Ref Expression
bj-iomnnom (iω↪ℕ‘ω) = +∞

Proof of Theorem bj-iomnnom
Dummy variables 𝑛 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-bj-iomnn 34666 . . . 4 iω↪ℕ = ((𝑛 ∈ ω ↦ ⟨[⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R⟩) ∪ {⟨ω, +∞⟩})
21a1i 11 . . 3 (⊤ → iω↪ℕ = ((𝑛 ∈ ω ↦ ⟨[⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R⟩) ∪ {⟨ω, +∞⟩}))
3 elirr 9049 . . . 4 ¬ ω ∈ ω
43a1i 11 . . 3 (⊤ → ¬ ω ∈ ω)
5 omex 9094 . . . 4 ω ∈ V
65a1i 11 . . 3 (⊤ → ω ∈ V)
7 bj-pinftyccb 34637 . . . 4 +∞ ∈ ℂ̅
87a1i 11 . . 3 (⊤ → +∞ ∈ ℂ̅)
92, 4, 6, 8bj-fvmptunsn1 34673 . 2 (⊤ → (iω↪ℕ‘ω) = +∞)
109mptru 1545 1 (iω↪ℕ‘ω) = +∞
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1538  ⊤wtru 1539   ∈ wcel 2112  {crab 3113  Vcvv 3444   ∪ cun 3882  {csn 4528  ⟨cop 4534   class class class wbr 5033   ↦ cmpt 5113  suc csuc 6165  ‘cfv 6328  ωcom 7564  1oc1o 8082  [cec 8274  Qcnq 10267
 Copyright terms: Public domain W3C validator