This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ℤ ≥ = j ∈ ℤ ⟼ k ∈ ℤ | j ≤ k

Detailed syntax breakdown

Step Hyp Ref Expression
0 cuz class ℤ ≥
1 vj setvar j
2 cz class ℤ
3 vk setvar k
4 1 cv setvar j
5 cle class ≤
6 3 cv setvar k
7 4 6 5 wbr wff j ≤ k
8 7 3 2 crab class k ∈ ℤ | j ≤ k
9 1 2 8 cmpt class j ∈ ℤ ⟼ k ∈ ℤ | j ≤ k
10 0 9 wceq wff ℤ ≥ = j ∈ ℤ ⟼ k ∈ ℤ | j ≤ k