Definition df-uz 9799

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 9800 for its value, uzssz 9819 for its relationship to ℤ, nnuz 9835 and nn0uz 9834 for its relationships to ℕ and ℕ₀, and eluz1 9802 and eluz2 9804 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 9798	. 2 class ℤ≥
2		vj	. . 3 setvar 𝑗
3		cz 9522	. . 3 class ℤ
4	2	cv 1397	. . . . 5 class 𝑗
5		vk	. . . . . 6 setvar 𝑘
6	5	cv 1397	. . . . 5 class 𝑘
7		cle 8258	. . . . 5 class ≤
8	4, 6, 7	wbr 4093	. . . 4 wff 𝑗 ≤ 𝑘
9	8, 5, 3	crab 2515	. . 3 class {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘}
10	2, 3, 9	cmpt 4155	. 2 class (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘})
11	1, 10	wceq 1398	1 wff ℤ≥ = (𝑗 ∈ ℤ ↦ {𝑘 ∈ ℤ ∣ 𝑗 ≤ 𝑘})

This definition is referenced by:  uzval  9800  uzf  9801  uzennn  10742