Definition df-uz

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 for its value, uzssz for its relationship to ZZ , nnuz and nn0uz for its relationships to NN and NN0 , and eluz1 and eluz2 for its membership relations. (Contributed by NM, 5-Sep-2005)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuz	|- ZZ>=
1		vj	|- j
2		cz	|- ZZ
3		vk	|- k
4	1	cv	|- j
5		cle	|- <_
6	3	cv	|- k
7	4 6 5	wbr	|- j <_ k
8	7 3 2	crab	|- { k e. ZZ | j <_ k }
9	1 2 8	cmpt	|- ( j e. ZZ |-> { k e. ZZ | j <_ k } )
10	0 9	wceq	|- ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )