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 37251
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 37198 but we did not use the present definition there since we wanted to have defined +∞ first.

See bj-iomnnom 37260 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 37250 . 2 class iω↪ℕ
2 vn . . . 4 setvar 𝑛
3 com 7887 . . . 4 class ω
4 vr . . . . . . . . . 10 setvar 𝑟
54cv 1539 . . . . . . . . 9 class 𝑟
62cv 1539 . . . . . . . . . . 11 class 𝑛
76csuc 6386 . . . . . . . . . 10 class suc 𝑛
8 c1o 8499 . . . . . . . . . 10 class 1o
97, 8cop 4632 . . . . . . . . 9 class ⟨suc 𝑛, 1o
10 cltq 10898 . . . . . . . . 9 class <Q
115, 9, 10wbr 5143 . . . . . . . 8 wff 𝑟 <Q ⟨suc 𝑛, 1o
12 cnq 10892 . . . . . . . 8 class Q
1311, 4, 12crab 3436 . . . . . . 7 class {𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}
14 c1p 10900 . . . . . . 7 class 1P
1513, 14cop 4632 . . . . . 6 class ⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P
16 cer 10904 . . . . . 6 class ~R
1715, 16cec 8743 . . . . 5 class [⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R
18 c0r 10906 . . . . 5 class 0R
1917, 18cop 4632 . . . 4 class ⟨[⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R
202, 3, 19cmpt 5225 . . 3 class (𝑛 ∈ ω ↦ ⟨[⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R⟩)
21 cpinfty 37220 . . . . 5 class +∞
223, 21cop 4632 . . . 4 class ⟨ω, +∞⟩
2322csn 4626 . . 3 class {⟨ω, +∞⟩}
2420, 23cun 3949 . 2 class ((𝑛 ∈ ω ↦ ⟨[⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R⟩) ∪ {⟨ω, +∞⟩})
251, 24wceq 1540 1 wff iω↪ℕ = ((𝑛 ∈ ω ↦ ⟨[⟨{𝑟Q𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R⟩) ∪ {⟨ω, +∞⟩})
Colors of variables: wff setvar class
This definition is referenced by:  bj-iomnnom  37260
  Copyright terms: Public domain W3C validator