Definition df-uz 10947

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 10948 for its value, uzssz 10965 for its relationship to , nnuz 10981 and nn0uz 10980 for its relationships to and , and eluz1 10950 and eluz2 10952 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 10946	. 2
2		vj	. . 3
3		cz 10731	. . 3
4	2	cv 1369	. . . . 5
5		vk	. . . . . 6
6	5	cv 1369	. . . . 5
7		cle 9504	. . . . 5
8	4, 6, 7	wbr 4374	. . . 4
9	8, 5, 3	crab 2796	. . 3
10	2, 3, 9	cmpt 4432	. 2
11	1, 10	wceq 1370	1

This definition is referenced by:  uzval  10948  uzf  10949