| Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-iomnn | Structured version Visualization version GIF version | ||
| 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.) |
| Ref | Expression |
|---|---|
| df-bj-iomnn | ⊢ iω↪ℕ = ((𝑛 ∈ ω ↦ 〈[〈{𝑟 ∈ Q ∣ 𝑟 <Q 〈suc 𝑛, 1o〉}, 1P〉] ~R , 0R〉) ∪ {〈ω, +∞〉}) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ciomnn 37250 | . 2 class iω↪ℕ | |
| 2 | vn | . . . 4 setvar 𝑛 | |
| 3 | com 7887 | . . . 4 class ω | |
| 4 | vr | . . . . . . . . . 10 setvar 𝑟 | |
| 5 | 4 | cv 1539 | . . . . . . . . 9 class 𝑟 |
| 6 | 2 | cv 1539 | . . . . . . . . . . 11 class 𝑛 |
| 7 | 6 | csuc 6386 | . . . . . . . . . 10 class suc 𝑛 |
| 8 | c1o 8499 | . . . . . . . . . 10 class 1o | |
| 9 | 7, 8 | cop 4632 | . . . . . . . . 9 class 〈suc 𝑛, 1o〉 |
| 10 | cltq 10898 | . . . . . . . . 9 class <Q | |
| 11 | 5, 9, 10 | wbr 5143 | . . . . . . . 8 wff 𝑟 <Q 〈suc 𝑛, 1o〉 |
| 12 | cnq 10892 | . . . . . . . 8 class Q | |
| 13 | 11, 4, 12 | crab 3436 | . . . . . . 7 class {𝑟 ∈ Q ∣ 𝑟 <Q 〈suc 𝑛, 1o〉} |
| 14 | c1p 10900 | . . . . . . 7 class 1P | |
| 15 | 13, 14 | cop 4632 | . . . . . 6 class 〈{𝑟 ∈ Q ∣ 𝑟 <Q 〈suc 𝑛, 1o〉}, 1P〉 |
| 16 | cer 10904 | . . . . . 6 class ~R | |
| 17 | 15, 16 | cec 8743 | . . . . 5 class [〈{𝑟 ∈ Q ∣ 𝑟 <Q 〈suc 𝑛, 1o〉}, 1P〉] ~R |
| 18 | c0r 10906 | . . . . 5 class 0R | |
| 19 | 17, 18 | cop 4632 | . . . 4 class 〈[〈{𝑟 ∈ Q ∣ 𝑟 <Q 〈suc 𝑛, 1o〉}, 1P〉] ~R , 0R〉 |
| 20 | 2, 3, 19 | cmpt 5225 | . . 3 class (𝑛 ∈ ω ↦ 〈[〈{𝑟 ∈ Q ∣ 𝑟 <Q 〈suc 𝑛, 1o〉}, 1P〉] ~R , 0R〉) |
| 21 | cpinfty 37220 | . . . . 5 class +∞ | |
| 22 | 3, 21 | cop 4632 | . . . 4 class 〈ω, +∞〉 |
| 23 | 22 | csn 4626 | . . 3 class {〈ω, +∞〉} |
| 24 | 20, 23 | cun 3949 | . 2 class ((𝑛 ∈ ω ↦ 〈[〈{𝑟 ∈ Q ∣ 𝑟 <Q 〈suc 𝑛, 1o〉}, 1P〉] ~R , 0R〉) ∪ {〈ω, +∞〉}) |
| 25 | 1, 24 | wceq 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 |