Definition df-uz 9817

Description: Define a function whose value at j is the semi-infinite set of contiguous integers starting at j, which we will also call the upper integers starting at j. Read " ZZ>= ` M " as "the set of integers greater than or equal to M". See uzval 9818 for its value, uzssz 9837 for its relationship to ZZ, nnuz 9853 and nn0uz 9852 for its relationships to NN and NN0, and eluz1 9820 and eluz2 9822 for its membership relations. (Contributed by NM, 5-Sep-2005.)

Assertion

Ref	Expression
df-uz	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )

Distinct variable group:   j, k

Detailed syntax breakdown of Definition df-uz

Step	Hyp	Ref	Expression
1		cuz 9816	. 2 class ZZ>=
2		vj	. . 3 setvar j
3		cz 9540	. . 3 class ZZ
4	2	cv 1397	. . . . 5 class j
5		vk	. . . . . 6 setvar k
6	5	cv 1397	. . . . 5 class k
7		cle 8274	. . . . 5 class <_
8	4, 6, 7	wbr 4093	. . . 4 wff j <_ k
9	8, 5, 3	crab 2515	. . 3 class { k e. ZZ | j <_ k }
10	2, 3, 9	cmpt 4155	. 2 class ( j e. ZZ |-> { k e. ZZ | j <_ k } )
11	1, 10	wceq 1398	1 wff ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )

This definition is referenced by:  uzval  9818  uzf  9819  uzennn  10761