Metamath Proof Explorer

Theorem uzid

Description: Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005)

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( M e. ZZ -> M e. ZZ )
2 zre 
 |-  ( M e. ZZ -> M e. RR )
3 2 leidd 
 |-  ( M e. ZZ -> M <_ M )
4 eluz1 
 |-  ( M e. ZZ -> ( M e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ M <_ M ) ) )
5 1 3 4 mpbir2and 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )