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	$$⊢{\mathbb{Z}}_{\ge }=\left(j\in \mathbb{Z}⟼\left\{k\in \mathbb{Z}|j\le k\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cuz	$$class{\mathbb{Z}}_{\ge }$$
1		vj	$$setvarj$$
2		cz	$$class\mathbb{Z}$$
3		vk	$$setvark$$
4	1	cv	$$setvarj$$
5		cle	$$class\le$$
6	3	cv	$$setvark$$
7	4 6 5	wbr	$$wffj\le k$$
8	7 3 2	crab	$$class\left\{k\in \mathbb{Z}|j\le k\right\}$$
9	1 2 8	cmpt	$$class\left(j\in \mathbb{Z}⟼\left\{k\in \mathbb{Z}|j\le k\right\}\right)$$
10	0 9	wceq	$$wff{\mathbb{Z}}_{\ge }=\left(j\in \mathbb{Z}⟼\left\{k\in \mathbb{Z}|j\le k\right\}\right)$$