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 zre
 |-  ( M e. ZZ -> M e. RR )
2 1 leidd
 |-  ( M e. ZZ -> M <_ M )
3 2 ancli
 |-  ( M e. ZZ -> ( M e. ZZ /\ M <_ M ) )
4 eluz1
 |-  ( M e. ZZ -> ( M e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ M <_ M ) ) )
5 3 4 mpbird
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )