Definition df-uz 11111

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 "`M " as "the set of integers greater than or equal to ." See uzval 11112 for its value, uzssz 11129 for its relationship to , nnuz 11145 and nn0uz 11144 for its relationships to and , and eluz1 11114 and eluz2 11116 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 11110	. 2
2		vj	. . 3
3		cz 10889	. . 3
4	2	cv 1394	. . . . 5
5		vk	. . . . . 6
6	5	cv 1394	. . . . 5
7		cle 9650	. . . . 5
8	4, 6, 7	wbr 4452	. . . 4
9	8, 5, 3	crab 2811	. . 3
10	2, 3, 9	cmpt 4510	. 2
11	1, 10	wceq 1395	1

This definition is referenced by:  uzval  11112  uzf  11113