Description: The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by NM, 11-Oct-2005) (Revised by AV, 5-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | infssuzcl | ⊢ ( ( 𝑆 ⊆ ( ℤ_{≥} ‘ 𝑀 ) ∧ 𝑆 ≠ ∅ ) → inf ( 𝑆 , ℝ , < ) ∈ 𝑆 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uzssz | ⊢ ( ℤ_{≥} ‘ 𝑀 ) ⊆ ℤ | |
2 | zssre | ⊢ ℤ ⊆ ℝ | |
3 | 1 2 | sstri | ⊢ ( ℤ_{≥} ‘ 𝑀 ) ⊆ ℝ |
4 | sstr | ⊢ ( ( 𝑆 ⊆ ( ℤ_{≥} ‘ 𝑀 ) ∧ ( ℤ_{≥} ‘ 𝑀 ) ⊆ ℝ ) → 𝑆 ⊆ ℝ ) | |
5 | 3 4 | mpan2 | ⊢ ( 𝑆 ⊆ ( ℤ_{≥} ‘ 𝑀 ) → 𝑆 ⊆ ℝ ) |
6 | uzwo | ⊢ ( ( 𝑆 ⊆ ( ℤ_{≥} ‘ 𝑀 ) ∧ 𝑆 ≠ ∅ ) → ∃ 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 ) | |
7 | lbinfcl | ⊢ ( ( 𝑆 ⊆ ℝ ∧ ∃ 𝑗 ∈ 𝑆 ∀ 𝑘 ∈ 𝑆 𝑗 ≤ 𝑘 ) → inf ( 𝑆 , ℝ , < ) ∈ 𝑆 ) | |
8 | 5 6 7 | syl2an2r | ⊢ ( ( 𝑆 ⊆ ( ℤ_{≥} ‘ 𝑀 ) ∧ 𝑆 ≠ ∅ ) → inf ( 𝑆 , ℝ , < ) ∈ 𝑆 ) |