Metamath Proof Explorer


Theorem uzinfi

Description: Extract the lower bound of an upper set of integers as its infimum. (Contributed by NM, 7-Oct-2005) (Revised by AV, 4-Sep-2020)

Ref Expression
Hypothesis uzinfi.1 𝑀 ∈ ℤ
Assertion uzinfi inf ( ( ℤ𝑀 ) , ℝ , < ) = 𝑀

Proof

Step Hyp Ref Expression
1 uzinfi.1 𝑀 ∈ ℤ
2 ltso < Or ℝ
3 2 a1i ( 𝑀 ∈ ℤ → < Or ℝ )
4 zre ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
5 uzid ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ𝑀 ) )
6 eluz2 ( 𝑘 ∈ ( ℤ𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀𝑘 ) )
7 4 adantr ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → 𝑀 ∈ ℝ )
8 zre ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
9 8 adantl ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℝ )
10 7 9 lenltd ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑀𝑘 ↔ ¬ 𝑘 < 𝑀 ) )
11 10 biimp3a ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀𝑘 ) → ¬ 𝑘 < 𝑀 )
12 11 a1d ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀𝑘 ) → ( 𝑀 ∈ ℤ → ¬ 𝑘 < 𝑀 ) )
13 6 12 sylbi ( 𝑘 ∈ ( ℤ𝑀 ) → ( 𝑀 ∈ ℤ → ¬ 𝑘 < 𝑀 ) )
14 13 impcom ( ( 𝑀 ∈ ℤ ∧ 𝑘 ∈ ( ℤ𝑀 ) ) → ¬ 𝑘 < 𝑀 )
15 3 4 5 14 infmin ( 𝑀 ∈ ℤ → inf ( ( ℤ𝑀 ) , ℝ , < ) = 𝑀 )
16 1 15 ax-mp inf ( ( ℤ𝑀 ) , ℝ , < ) = 𝑀