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

Metamath Proof Explorer

Theorem uzval

Description: The value of the upper integers function. (Contributed by NM, 5-Sep-2005) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion uzval ⊢ N ∈ ℤ → ℤ ≥ N = k ∈ ℤ | N ≤ k

Proof

Step Hyp Ref Expression
1 breq1 ⊢ j = N → j ≤ k ↔ N ≤ k
2 1 rabbidv ⊢ j = N → k ∈ ℤ | j ≤ k = k ∈ ℤ | N ≤ k
3 df-uz ⊢ ℤ ≥ = j ∈ ℤ ⟼ k ∈ ℤ | j ≤ k
4 zex ⊢ ℤ ∈ V
5 4 rabex ⊢ k ∈ ℤ | N ≤ k ∈ V
6 2 3 5 fvmpt ⊢ N ∈ ℤ → ℤ ≥ N = k ∈ ℤ | N ≤ k