Definition df-uz 9649

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 9650 for its value, uzssz 9668 for its relationship to ZZ, nnuz 9684 and nn0uz 9683 for its relationships to NN and NN0, and eluz1 9652 and eluz2 9654 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 9648	. 2 class ZZ>=
2		vj	. . 3 setvar j
3		cz 9372	. . 3 class ZZ
4	2	cv 1372	. . . . 5 class j
5		vk	. . . . . 6 setvar k
6	5	cv 1372	. . . . 5 class k
7		cle 8108	. . . . 5 class <_
8	4, 6, 7	wbr 4044	. . . 4 wff j <_ k
9	8, 5, 3	crab 2488	. . 3 class { k e. ZZ | j <_ k }
10	2, 3, 9	cmpt 4105	. 2 class ( j e. ZZ |-> { k e. ZZ | j <_ k } )
11	1, 10	wceq 1373	1 wff ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )

This definition is referenced by:  uzval  9650  uzf  9651  uzennn  10581