# Metamath Proof Explorer

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

### Detailed syntax breakdown

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