Definition df-uz 9684

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 9685 for its value, uzssz 9703 for its relationship to ZZ, nnuz 9719 and nn0uz 9718 for its relationships to NN and NN0, and eluz1 9687 and eluz2 9689 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 9683	. 2 class ZZ>=
2		vj	. . 3 setvar j
3		cz 9407	. . 3 class ZZ
4	2	cv 1372	. . . . 5 class j
5		vk	. . . . . 6 setvar k
6	5	cv 1372	. . . . 5 class k
7		cle 8143	. . . . 5 class <_
8	4, 6, 7	wbr 4059	. . . 4 wff j <_ k
9	8, 5, 3	crab 2490	. . 3 class { k e. ZZ | j <_ k }
10	2, 3, 9	cmpt 4121	. 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  9685  uzf  9686  uzennn  10618