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

Metamath Proof Explorer

Theorem infxrge0glb

Description: The infimum of a set of nonnegative extended reals is the greatest lower bound. (Contributed by Thierry Arnoux, 19-Jul-2020) (Revised by AV, 4-Oct-2020)

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

Proof

Step	Hyp	Ref	Expression
1		infxrge0glb.a	⊢ ( 𝜑 → 𝐴 ⊆ ( 0 [,] +∞ ) )
2		infxrge0glb.b	⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
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 1	infglbb	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) → ( inf ( 𝐴 , ( 0 [,] +∞ ) , < ) < 𝐵 ↔ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝐵 ) )
11	2 10	mpdan	⊢ ( 𝜑 → ( inf ( 𝐴 , ( 0 [,] +∞ ) , < ) < 𝐵 ↔ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝐵 ) )
12		breq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 < 𝐵 ↔ 𝑧 < 𝐵 ) )
13	12	cbvrexvw	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 ↔ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝐵 )
14	11 13	bitr4di	⊢ ( 𝜑 → ( inf ( 𝐴 , ( 0 [,] +∞ ) , < ) < 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 ) )