Metamath Proof Explorer

Theorem eluzelz

Description: A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005)

Ref Expression
Assertion eluzelz 
|- ( N e. ( ZZ>= ` M ) -> N e. ZZ )

Proof

Step Hyp Ref Expression
1 eluz2 
 |-  ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
2 1 simp2bi 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )