Definition df-bj-iomnn

Description: Definition of the canonical bijection from (om u. { om } ) onto ( NN0 u. { pinfty } ) .

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 RR C_ CC ), 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 but we did not use the present definition there since we wanted to have defined pinfty first.

See bj-iomnnom for its value at pinfty .

TODO:

Prove |- ( iomnn(/) ) = 0 .

Define |- NN0 = ( iomnn "om ) and |- NN = ( NN0 \ { 0 } ) .

Prove |- iomnn : ( om u. {om } ) -1-1-onto-> ( NN0 u. { pinfty } ) and ` |- ( iomnn |`om ) :om -1-1-onto-> NN0 .

Prove ` |- ( iomnn |`om ) = rec ( ( x e. RR |-> ( x + 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
Assertion	df-bj-iomnn	⊢ iω↪ℕ = ( ( 𝑛 ∈ ω ↦ ⟨ [ ⟨ { 𝑟 ∈ Q ∣ 𝑟 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R , 0R ⟩ ) ∪ { ⟨ ω , +∞ ⟩ } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ciomnn	⊢ iω↪ℕ
1		vn	⊢ 𝑛
2		com	⊢ ω
3		vr	⊢ 𝑟
4		cnq	⊢ Q
5	3	cv	⊢ 𝑟
6		cltq	⊢ <Q
7	1	cv	⊢ 𝑛
8	7	csuc	⊢ suc 𝑛
9		c1o	⊢ 1o
10	8 9	cop	⊢ ⟨ suc 𝑛 , 1o ⟩
11	5 10 6	wbr	⊢ 𝑟 <Q ⟨ suc 𝑛 , 1o ⟩
12	11 3 4	crab	⊢ { 𝑟 ∈ Q ∣ 𝑟 <Q ⟨ suc 𝑛 , 1o ⟩ }
13		c1p	⊢ 1P
14	12 13	cop	⊢ ⟨ { 𝑟 ∈ Q ∣ 𝑟 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩
15		cer	⊢ ~R
16	14 15	cec	⊢ [ ⟨ { 𝑟 ∈ Q ∣ 𝑟 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R
17		c0r	⊢ 0R
18	16 17	cop	⊢ ⟨ [ ⟨ { 𝑟 ∈ Q ∣ 𝑟 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R , 0R ⟩
19	1 2 18	cmpt	⊢ ( 𝑛 ∈ ω ↦ ⟨ [ ⟨ { 𝑟 ∈ Q ∣ 𝑟 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R , 0R ⟩ )
20		cpinfty	⊢ +∞
21	2 20	cop	⊢ ⟨ ω , +∞ ⟩
22	21	csn	⊢ { ⟨ ω , +∞ ⟩ }
23	19 22	cun	⊢ ( ( 𝑛 ∈ ω ↦ ⟨ [ ⟨ { 𝑟 ∈ Q ∣ 𝑟 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R , 0R ⟩ ) ∪ { ⟨ ω , +∞ ⟩ } )
24	0 23	wceq	⊢ iω↪ℕ = ( ( 𝑛 ∈ ω ↦ ⟨ [ ⟨ { 𝑟 ∈ Q ∣ 𝑟 <Q ⟨ suc 𝑛 , 1o ⟩ } , 1P ⟩ ] ~R , 0R ⟩ ) ∪ { ⟨ ω , +∞ ⟩ } )