Metamath Proof Explorer

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 ⊢ φ → C ⊆ B
xrge0infssd.2 ⊢ φ → B ⊆ 0 +∞
Assertion xrge0infssd ⊢ φ → inf B 0 +∞ < ≤ inf C 0 +∞ <

Proof

Step Hyp Ref Expression
1 xrge0infssd.1 ⊢ φ → C ⊆ B
2 xrge0infssd.2 ⊢ φ → 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 ⊢ B ⊆ 0 +∞ → ∃ x ∈ 0 +∞ ∀ y ∈ B ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ B z < y
9 2 8 syl ⊢ φ → ∃ x ∈ 0 +∞ ∀ y ∈ B ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ B z < y
10 7 9 infcl ⊢ φ → inf B 0 +∞ < ∈ 0 +∞
11 3 10 sselid ⊢ φ → inf B 0 +∞ < ∈ ℝ *
12 1 2 sstrd ⊢ φ → C ⊆ 0 +∞
13 xrge0infss ⊢ C ⊆ 0 +∞ → ∃ x ∈ 0 +∞ ∀ y ∈ C ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ C z < y
14 12 13 syl ⊢ φ → ∃ x ∈ 0 +∞ ∀ y ∈ C ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ C z < y
15 7 14 infcl ⊢ φ → inf C 0 +∞ < ∈ 0 +∞
16 3 15 sselid ⊢ φ → inf C 0 +∞ < ∈ ℝ *
17 7 1 14 9 infssd ⊢ φ → ¬ inf C 0 +∞ < < inf B 0 +∞ <
18 11 16 17 xrnltled ⊢ φ → inf B 0 +∞ < ≤ inf C 0 +∞ <