Theorem infxrge0gelb

Description: The infimum of a set of nonnegative extended reals is greater than or equal to a 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	infxrge0gelb	⊢ ( 𝜑 → ( 𝐵 ≤ inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		infxrge0glb.a	⊢ ( 𝜑 → 𝐴 ⊆ ( 0 [,] +∞ ) )
2		infxrge0glb.b	⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
3	1 2	infxrge0glb	⊢ ( 𝜑 → ( inf ( 𝐴 , ( 0 [,] +∞ ) , < ) < 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 ) )
4	3	notbid	⊢ ( 𝜑 → ( ¬ inf ( 𝐴 , ( 0 [,] +∞ ) , < ) < 𝐵 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 ) )
5		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
6	5 2	sselid	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
7		xrltso	⊢ < Or ℝ*
8		soss	⊢ ( ( 0 [,] +∞ ) ⊆ ℝ* → ( < Or ℝ* → < Or ( 0 [,] +∞ ) ) )
9	5 7 8	mp2	⊢ < Or ( 0 [,] +∞ )
10	9	a1i	⊢ ( 𝜑 → < Or ( 0 [,] +∞ ) )
11		xrge0infss	⊢ ( 𝐴 ⊆ ( 0 [,] +∞ ) → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
12	1 11	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
13	10 12	infcl	⊢ ( 𝜑 → inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ∈ ( 0 [,] +∞ ) )
14	5 13	sselid	⊢ ( 𝜑 → inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ∈ ℝ* )
15	6 14	xrlenltd	⊢ ( 𝜑 → ( 𝐵 ≤ inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ↔ ¬ inf ( 𝐴 , ( 0 [,] +∞ ) , < ) < 𝐵 ) )
16	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
17	1 5	sstrdi	⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
18	17	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
19	16 18	xrlenltd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ≤ 𝑥 ↔ ¬ 𝑥 < 𝐵 ) )
20	19	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ) )
21		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 )
22	20 21	bitrdi	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑥 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 ) )
23	4 15 22	3bitr4d	⊢ ( 𝜑 → ( 𝐵 ≤ inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑥 ) )