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 e. ZZ -> ( ZZ>= ` N ) = { k e. ZZ | N <_ k } )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( j = N -> ( j <_ k <-> N <_ k ) )
2 1 rabbidv 
 |-  ( j = N -> { k e. ZZ | j <_ k } = { k e. ZZ | N <_ k } )
3 df-uz 
 |-  ZZ>= = ( j e. ZZ |-> { k e. ZZ | j <_ k } )
4 zex 
 |-  ZZ e. _V
5 4 rabex 
 |-  { k e. ZZ | N <_ k } e. _V
6 2 3 5 fvmpt 
 |-  ( N e. ZZ -> ( ZZ>= ` N ) = { k e. ZZ | N <_ k } )