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

Definition df-bj-iomnn 37232
Description: Definition of the canonical bijection from (ω ∪ {ω}) onto (ℕ0 ∪ {+∞}).

To understand this definition, recall that set.mm constructs reals as couples whose first component is a prereal and second component is the zero prereal (in order that one have ℝ ⊆ ℂ), that prereals are equivalence classes of couples of positive reals, the latter are Dedekind cuts of positive rationals, which are equivalence classes of positive ordinals. In partiular, we take the successor ordinal at the beginning and subtract 1 at the end since the intermediate systems contain only (strictly) positive numbers.

Note the similarity with df-bj-fractemp 37179 but we did not use the present definition there since we wanted to have defined +∞ first.

See bj-iomnnom 37241 for its value at +∞.

TODO:

Prove (iω↪ℕ‘∅) = 0.

Define 0 = (iω↪ℕ “ ω) and ℕ = (ℕ0 ∖ {0}).

Prove iω↪ℕ:(ω ∪ {ω})–1-1-onto→(ℕ0 ∪ {+∞}) and (iω↪ℕ ↾ ω):ω–1-1-onto→ℕ0.

Prove that these bijections are respectively an isomorphism of ordered "extended rigs" and of ordered rigs.

Prove (iω↪ℕ ↾ ω) = rec((𝑥 ∈ ℝ ↦ (𝑥 + 1)), 0).

(Contributed by BJ, 18-Feb-2023.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)

Assertion
Ref Expression
df-bj-iomnn iω↪ℕ = ((𝑛 ∈ ω ↦ ⟨[⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R⟩) ∪ {⟨ω, +∞⟩})
Distinct variable group:   𝑛,𝑟

Detailed syntax breakdown of Definition df-bj-iomnn
StepHypRef Expression
1 ciomnn 37231 . 2 class iω↪ℕ
2 vn . . . 4 setvar 𝑛
3 com 7886 . . . 4 class ω
4 vr . . . . . . . . . 10 setvar 𝑟
54cv 1535 . . . . . . . . 9 class 𝑟
62cv 1535 . . . . . . . . . . 11 class 𝑛
76csuc 6387 . . . . . . . . . 10 class suc 𝑛
8 c1o 8497 . . . . . . . . . 10 class 1o
97, 8cop 4636 . . . . . . . . 9 class ⟨suc 𝑛, 1o
10 cltq 10895 . . . . . . . . 9 class <Q
115, 9, 10wbr 5147 . . . . . . . 8 wff 𝑟 <Q ⟨suc 𝑛, 1o
12 cnq 10889 . . . . . . . 8 class Q
1311, 4, 12crab 3432 . . . . . . 7 class {𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}
14 c1p 10897 . . . . . . 7 class 1P
1513, 14cop 4636 . . . . . 6 class ⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P
16 cer 10901 . . . . . 6 class ~R
1715, 16cec 8741 . . . . 5 class [⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R
18 c0r 10903 . . . . 5 class 0R
1917, 18cop 4636 . . . 4 class ⟨[⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R
202, 3, 19cmpt 5230 . . 3 class (𝑛 ∈ ω ↦ ⟨[⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R⟩)
21 cpinfty 37201 . . . . 5 class +∞
223, 21cop 4636 . . . 4 class ⟨ω, +∞⟩
2322csn 4630 . . 3 class {⟨ω, +∞⟩}
2420, 23cun 3960 . 2 class ((𝑛 ∈ ω ↦ ⟨[⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R⟩) ∪ {⟨ω, +∞⟩})
251, 24wceq 1536 1 wff iω↪ℕ = ((𝑛 ∈ ω ↦ ⟨[⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R⟩) ∪ {⟨ω, +∞⟩})
Colors of variables: wff setvar class
This definition is referenced by:  bj-iomnnom  37241
  Copyright terms: Public domain W3C validator