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 ( 𝑆 , ℝ , < ) ≤ 𝐴 )