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

Metamath Proof Explorer

Theorem infxrge0lb

Description: A member of a set of nonnegative extended reals is greater than or equal to the set's infimum. (Contributed by Thierry Arnoux, 19-Jul-2020) (Revised by AV, 4-Oct-2020)

		Ref	Expression
	Hypotheses	infxrge0lb.a	⊢ ( 𝜑 → 𝐴 ⊆ ( 0 [,] +∞ ) )
		infxrge0lb.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
	Assertion	infxrge0lb	⊢ ( 𝜑 → inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ≤ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		infxrge0lb.a	⊢ ( 𝜑 → 𝐴 ⊆ ( 0 [,] +∞ ) )
2		infxrge0lb.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐴 )
3		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ^*
4		xrltso	⊢ < Or ℝ^*
5		soss	⊢ ( ( 0 [,] +∞ ) ⊆ ℝ^* → ( < Or ℝ^* → < Or ( 0 [,] +∞ ) ) )
6	3 4 5	mp2	⊢ < Or ( 0 [,] +∞ )
7	6	a1i	⊢ ( 𝜑 → < Or ( 0 [,] +∞ ) )
8		xrge0infss	⊢ ( 𝐴 ⊆ ( 0 [,] +∞ ) → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
9	1 8	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
10	7 9	infcl	⊢ ( 𝜑 → inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ∈ ( 0 [,] +∞ ) )
11	3 10	sselid	⊢ ( 𝜑 → inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ∈ ℝ^* )
12	1 2	sseldd	⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
13	3 12	sselid	⊢ ( 𝜑 → 𝐵 ∈ ℝ^* )
14	7 9	inflb	⊢ ( 𝜑 → ( 𝐵 ∈ 𝐴 → ¬ 𝐵 < inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ) )
15	2 14	mpd	⊢ ( 𝜑 → ¬ 𝐵 < inf ( 𝐴 , ( 0 [,] +∞ ) , < ) )
16	11 13 15	xrnltled	⊢ ( 𝜑 → inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ≤ 𝐵 )