Definition df-uz 12487

Description: Define a function whose value at 𝑗 is the semi-infinite set of contiguous integers starting at 𝑗, which we will also call the upper integers starting at 𝑗. Read "ℤ_≥‘𝑀 " as "the set of integers greater than or equal to 𝑀". See uzval 12488 for its value, uzssz 12507 for its relationship to ℤ, nnuz 12525 and nn0uz 12524 for its relationships to ℕ and ℕ₀, and eluz1 12490 and eluz2 12492 for its membership relations. (Contributed by NM, 5-Sep-2005.)

Assertion

Ref	Expression
df-uz	⊢ ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘})

Distinct variable group:   𝑗,𝑘

Detailed syntax breakdown of Definition df-uz

Step	Hyp	Ref	Expression
1		cuz 12486	. 2 class ℤ≥
2		vj	. . 3 setvar 𝑗
3		cz 12224	. . 3 class ℤ
4	2	cv 1542	. . . . 5 class 𝑗
5		vk	. . . . . 6 setvar 𝑘
6	5	cv 1542	. . . . 5 class 𝑘
7		cle 10916	. . . . 5 class ≤
8	4, 6, 7	wbr 5070	. . . 4 wff 𝑗 ≤ 𝑘
9	8, 5, 3	crab 3068	. . 3 class {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}
10	2, 3, 9	cmpt 5152	. 2 class (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘})
11	1, 10	wceq 1543	1 wff ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘})

This definition is referenced by:  uzval  12488  uzf  12489