Definition df-uz 7587

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 7588 for its value, uzssz 7599 for its relationship to ZZ, nnuz 7608 and nn0uz 7607 for its relationships to NN and NN0, and eluz1 7589 and eluz2 7590 for its membership relations.

Assertion

Ref	Expression
df-uz	|- ZZ>= = {<.j, y>. | (j e. ZZ /\ y = {k e. ZZ | j <_ k})}

Distinct variable group:   j,k,y

Detailed syntax breakdown of Definition df-uz

Step	Hyp	Ref	Expression
1		cuz 7586	. 2 class ZZ>=
2		vj	. . . . . 6 set j
3	2	cv 1297	. . . . 5 class j
4		cz 6451	. . . . 5 class ZZ
5	3, 4	wcel 1300	. . . 4 wff j e. ZZ
6		vy	. . . . . 6 set y
7	6	cv 1297	. . . . 5 class y
8		vk	. . . . . . . 8 set k
9	8	cv 1297	. . . . . . 7 class k
10		cle 6448	. . . . . . 7 class <_
11	3, 9, 10	wbr 3338	. . . . . 6 wff j <_ k
12	11, 8, 4	crab 2108	. . . . 5 class {k e. ZZ | j <_ k}
13	7, 12	wceq 1298	. . . 4 wff y = {k e. ZZ | j <_ k}
14	5, 13	wa 240	. . 3 wff (j e. ZZ /\ y = {k e. ZZ | j <_ k})
15	14, 2, 6	copab 3395	. 2 class {<.j, y>. | (j e. ZZ /\ y = {k e. ZZ | j <_ k})}
16	1, 15	wceq 1298	1 wff ZZ>= = {<.j, y>. | (j e. ZZ /\ y = {k e. ZZ | j <_ k})}

This definition is referenced by:  uzval 7588  eluz2 7590  uzssz 7599

Copyright terms: Public domain