Definition df-bj-iomnn 37273

Description: Definition of the canonical bijection from (ω ∪ {ω}) onto (ℕ₀ ∪ {+∞}).

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

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

TODO:

Prove ⊢ (i_ω↪ℕ‘∅) = 0.

Define ⊢ ℕ₀ = (i_ω↪ℕ “ ω) and ⊢ ℕ = (ℕ₀ ∖ {0}).

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

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

Step	Hyp	Ref	Expression
1		ciomnn 37272	. 2 class iω↪ℕ
2		vn	. . . 4 setvar 𝑛
3		com 7866	. . . 4 class ω
4		vr	. . . . . . . . . 10 setvar 𝑟
5	4	cv 1539	. . . . . . . . 9 class 𝑟
6	2	cv 1539	. . . . . . . . . . 11 class 𝑛
7	6	csuc 6359	. . . . . . . . . 10 class suc 𝑛
8		c1o 8478	. . . . . . . . . 10 class 1o
9	7, 8	cop 4612	. . . . . . . . 9 class ⟨suc 𝑛, 1o⟩
10		cltq 10877	. . . . . . . . 9 class <Q
11	5, 9, 10	wbr 5124	. . . . . . . 8 wff 𝑟 <Q ⟨suc 𝑛, 1o⟩
12		cnq 10871	. . . . . . . 8 class Q
13	11, 4, 12	crab 3420	. . . . . . 7 class {𝑟 ∈ Q ∣ 𝑟 <Q ⟨suc 𝑛, 1o⟩}
14		c1p 10879	. . . . . . 7 class 1P
15	13, 14	cop 4612	. . . . . 6 class ⟨{𝑟 ∈ Q ∣ 𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩
16		cer 10883	. . . . . 6 class ~R
17	15, 16	cec 8722	. . . . 5 class [⟨{𝑟 ∈ Q ∣ 𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R
18		c0r 10885	. . . . 5 class 0R
19	17, 18	cop 4612	. . . 4 class ⟨[⟨{𝑟 ∈ Q ∣ 𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R⟩
20	2, 3, 19	cmpt 5206	. . 3 class (𝑛 ∈ ω ↦ ⟨[⟨{𝑟 ∈ Q ∣ 𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R⟩)
21		cpinfty 37242	. . . . 5 class +∞
22	3, 21	cop 4612	. . . 4 class ⟨ω, +∞⟩
23	22	csn 4606	. . 3 class {⟨ω, +∞⟩}
24	20, 23	cun 3929	. 2 class ((𝑛 ∈ ω ↦ ⟨[⟨{𝑟 ∈ Q ∣ 𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R⟩) ∪ {⟨ω, +∞⟩})
25	1, 24	wceq 1540	1 wff iω↪ℕ = ((𝑛 ∈ ω ↦ ⟨[⟨{𝑟 ∈ Q ∣ 𝑟 <Q ⟨suc 𝑛, 1o⟩}, 1P⟩] ~R , 0R⟩) ∪ {⟨ω, +∞⟩})

This definition is referenced by:  bj-iomnnom  37282