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 ⊢φ→supB0+∞<≤supC0+∞<

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ℝ*→<Or0+∞
6 3 4 5 mp2 ⊢<Or0+∞
7 6 a1i ⊢φ→<Or0+∞
8 xrge0infss ⊢B⊆0+∞→∃x∈0+∞∀y∈B¬y<x∧∀y∈0+∞x<y→∃z∈Bz<y
9 2 8 syl ⊢φ→∃x∈0+∞∀y∈B¬y<x∧∀y∈0+∞x<y→∃z∈Bz<y
10 7 9 infcl ⊢φ→supB0+∞<∈0+∞
11 3 10 sselid ⊢φ→supB0+∞<∈ℝ*
12 1 2 sstrd ⊢φ→C⊆0+∞
13 xrge0infss ⊢C⊆0+∞→∃x∈0+∞∀y∈C¬y<x∧∀y∈0+∞x<y→∃z∈Cz<y
14 12 13 syl ⊢φ→∃x∈0+∞∀y∈C¬y<x∧∀y∈0+∞x<y→∃z∈Cz<y
15 7 14 infcl ⊢φ→supC0+∞<∈0+∞
16 3 15 sselid ⊢φ→supC0+∞<∈ℝ*
17 7 1 14 9 infssd ⊢φ→¬supC0+∞<<supB0+∞<
18 11 16 17 xrnltled ⊢φ→supB0+∞<≤supC0+∞<