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

Metamath Proof Explorer

Theorem infssuzle

Description: The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by NM, 11-Oct-2005) (Revised by AV, 5-Sep-2020)

Ref Expression
Assertion infssuzle ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐴 ∈ 𝑆 ) → inf ( 𝑆 , ℝ , < ) ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 ne0i ⊢ ( 𝐴 ∈ 𝑆 → 𝑆 ≠ ∅ )
2 uzwo ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑆 ≠ ∅ ) → ∃ 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 )
3 1 2 sylan2 ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐴 ∈ 𝑆 ) → ∃ 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 )
4 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
5 zssre ⊢ ℤ ⊆ ℝ
6 4 5 sstri ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ
7 sstr ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ ( ℤ≥ ‘ 𝑀 ) ⊆ ℝ ) → 𝑆 ⊆ ℝ )
8 6 7 mpan2 ⊢ ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) → 𝑆 ⊆ ℝ )
9 lbinfle ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 ∧ 𝐴 ∈ 𝑆 ) → inf ( 𝑆 , ℝ , < ) ≤ 𝐴 )
10 9 3com23 ⊢ ( ( 𝑆 ⊆ ℝ ∧ 𝐴 ∈ 𝑆 ∧ ∃ 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 ) → inf ( 𝑆 , ℝ , < ) ≤ 𝐴 )
11 8 10 syl3an1 ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐴 ∈ 𝑆 ∧ ∃ 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 ) → inf ( 𝑆 , ℝ , < ) ≤ 𝐴 )
12 3 11 mpd3an3 ⊢ ( ( 𝑆 ⊆ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐴 ∈ 𝑆 ) → inf ( 𝑆 , ℝ , < ) ≤ 𝐴 )