Metamath Proof Explorer

Theorem eluznn0

Description: Membership in a nonnegative upper set of integers implies membership in NN0 . (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion eluznn0 
|- ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) ) -> M e. NN0 )

Proof

Step Hyp Ref Expression
1 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
2 1 uztrn2 
 |-  ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) ) -> M e. NN0 )