Metamath Proof Explorer

Theorem nnuz

Description: Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005)

Ref Expression
Assertion nnuz 
|- NN = ( ZZ>= ` 1 )

Proof

Step Hyp Ref Expression
1 nnzrab 
 |-  NN = { k e. ZZ | 1 <_ k }
2 1z 
 |-  1 e. ZZ
3 uzval 
 |-  ( 1 e. ZZ -> ( ZZ>= ` 1 ) = { k e. ZZ | 1 <_ k } )
4 2 3 ax-mp 
 |-  ( ZZ>= ` 1 ) = { k e. ZZ | 1 <_ k }
5 1 4 eqtr4i 
 |-  NN = ( ZZ>= ` 1 )