Metamath Proof Explorer

Theorem eluzel2

Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005) (Revised by Mario Carneiro, 3-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( N e. ( ZZ>= ` M ) -> M e. dom ZZ>= )
2 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
3 2 fdmi 
 |-  dom ZZ>= = ZZ
4 1 3 eleqtrdi 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )