This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uzid3

Description: Membership of the least member in an upper set of integers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis uzid3.1 ⊢ Z = ℤ ≥ M
Assertion uzid3 ⊢ N ∈ Z → N ∈ ℤ ≥ N

Proof

Step Hyp Ref Expression
1 uzid3.1 ⊢ Z = ℤ ≥ M
2 1 eleq2i ⊢ N ∈ Z ↔ N ∈ ℤ ≥ M
3 2 biimpi ⊢ N ∈ Z → N ∈ ℤ ≥ M
4 uzid2 ⊢ N ∈ ℤ ≥ M → N ∈ ℤ ≥ N
5 3 4 syl ⊢ N ∈ Z → N ∈ ℤ ≥ N