Metamath Proof Explorer

Theorem nn0uz

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

Ref Expression
Assertion nn0uz 
|- NN0 = ( ZZ>= ` 0 )

Proof

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