Theorem xrge0infssd

Description: Inequality deduction for infimum of a nonnegative extended real subset. (Contributed by Thierry Arnoux, 16-Sep-2019) (Revised by AV, 4-Oct-2020)

	Ref	Expression
Hypotheses	xrge0infssd.1	⊢ ( 𝜑 → 𝐶 ⊆ 𝐵 )
	xrge0infssd.2	⊢ ( 𝜑 → 𝐵 ⊆ ( 0 [,] +∞ ) )
Assertion	xrge0infssd	⊢ ( 𝜑 → inf ( 𝐵 , ( 0 [,] +∞ ) , < ) ≤ inf ( 𝐶 , ( 0 [,] +∞ ) , < ) )

Proof

Step	Hyp	Ref	Expression
1		xrge0infssd.1	⊢ ( 𝜑 → 𝐶 ⊆ 𝐵 )
2		xrge0infssd.2	⊢ ( 𝜑 → 𝐵 ⊆ ( 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	2 8	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐵 𝑧 < 𝑦 ) ) )
10	7 9	infcl	⊢ ( 𝜑 → inf ( 𝐵 , ( 0 [,] +∞ ) , < ) ∈ ( 0 [,] +∞ ) )
11	3 10	sselid	⊢ ( 𝜑 → inf ( 𝐵 , ( 0 [,] +∞ ) , < ) ∈ ℝ* )
12	1 2	sstrd	⊢ ( 𝜑 → 𝐶 ⊆ ( 0 [,] +∞ ) )
13		xrge0infss	⊢ ( 𝐶 ⊆ ( 0 [,] +∞ ) → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐶 𝑧 < 𝑦 ) ) )
14	12 13	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐶 𝑧 < 𝑦 ) ) )
15	7 14	infcl	⊢ ( 𝜑 → inf ( 𝐶 , ( 0 [,] +∞ ) , < ) ∈ ( 0 [,] +∞ ) )
16	3 15	sselid	⊢ ( 𝜑 → inf ( 𝐶 , ( 0 [,] +∞ ) , < ) ∈ ℝ* )
17	7 1 14 9	infssd	⊢ ( 𝜑 → ¬ inf ( 𝐶 , ( 0 [,] +∞ ) , < ) < inf ( 𝐵 , ( 0 [,] +∞ ) , < ) )
18	11 16 17	xrnltled	⊢ ( 𝜑 → inf ( 𝐵 , ( 0 [,] +∞ ) , < ) ≤ inf ( 𝐶 , ( 0 [,] +∞ ) , < ) )