Metamath Proof Explorer

Theorem xrge0infss

Description: Any subset of nonnegative extended reals has an infimum. (Contributed by Thierry Arnoux, 16-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Assertion xrge0infss ⊢ A ⊆ 0 +∞ → ∃ x ∈ 0 +∞ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y

Proof

Step Hyp Ref Expression
1 ssel2 ⊢ A ⊆ 0 +∞ ∧ y ∈ A → y ∈ 0 +∞
2 0xr ⊢ 0 ∈ ℝ *
3 pnfxr ⊢ +∞ ∈ ℝ *
4 iccgelb ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ y ∈ 0 +∞ → 0 ≤ y
5 2 3 4 mp3an12 ⊢ y ∈ 0 +∞ → 0 ≤ y
6 eliccxr ⊢ y ∈ 0 +∞ → y ∈ ℝ *
7 xrlenlt ⊢ 0 ∈ ℝ * ∧ y ∈ ℝ * → 0 ≤ y ↔ ¬ y < 0
8 2 6 7 sylancr ⊢ y ∈ 0 +∞ → 0 ≤ y ↔ ¬ y < 0
9 5 8 mpbid ⊢ y ∈ 0 +∞ → ¬ y < 0
10 1 9 syl ⊢ A ⊆ 0 +∞ ∧ y ∈ A → ¬ y < 0
11 10 ralrimiva ⊢ A ⊆ 0 +∞ → ∀ y ∈ A ¬ y < 0
12 11 ad3antrrr ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y ∧ w ≤ 0 → ∀ y ∈ A ¬ y < 0
13 iccssxr ⊢ 0 +∞ ⊆ ℝ *
14 ssralv ⊢ 0 +∞ ⊆ ℝ * → ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y → ∀ y ∈ 0 +∞ w < y → ∃ z ∈ A z < y
15 13 14 ax-mp ⊢ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y → ∀ y ∈ 0 +∞ w < y → ∃ z ∈ A z < y
16 simplll ⊢ w ∈ ℝ * ∧ w ≤ 0 ∧ y ∈ 0 +∞ ∧ 0 < y → w ∈ ℝ *
17 2 a1i ⊢ w ∈ ℝ * ∧ w ≤ 0 ∧ y ∈ 0 +∞ ∧ 0 < y → 0 ∈ ℝ *
18 simplr ⊢ w ∈ ℝ * ∧ w ≤ 0 ∧ y ∈ 0 +∞ ∧ 0 < y → y ∈ 0 +∞
19 13 18 sseldi ⊢ w ∈ ℝ * ∧ w ≤ 0 ∧ y ∈ 0 +∞ ∧ 0 < y → y ∈ ℝ *
20 simpllr ⊢ w ∈ ℝ * ∧ w ≤ 0 ∧ y ∈ 0 +∞ ∧ 0 < y → w ≤ 0
21 simpr ⊢ w ∈ ℝ * ∧ w ≤ 0 ∧ y ∈ 0 +∞ ∧ 0 < y → 0 < y
22 16 17 19 20 21 xrlelttrd ⊢ w ∈ ℝ * ∧ w ≤ 0 ∧ y ∈ 0 +∞ ∧ 0 < y → w < y
23 22 ex ⊢ w ∈ ℝ * ∧ w ≤ 0 ∧ y ∈ 0 +∞ → 0 < y → w < y
24 23 imim1d ⊢ w ∈ ℝ * ∧ w ≤ 0 ∧ y ∈ 0 +∞ → w < y → ∃ z ∈ A z < y → 0 < y → ∃ z ∈ A z < y
25 24 ralimdva ⊢ w ∈ ℝ * ∧ w ≤ 0 → ∀ y ∈ 0 +∞ w < y → ∃ z ∈ A z < y → ∀ y ∈ 0 +∞ 0 < y → ∃ z ∈ A z < y
26 15 25 syl5 ⊢ w ∈ ℝ * ∧ w ≤ 0 → ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y → ∀ y ∈ 0 +∞ 0 < y → ∃ z ∈ A z < y
27 26 adantll ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ w ≤ 0 → ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y → ∀ y ∈ 0 +∞ 0 < y → ∃ z ∈ A z < y
28 27 imp ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ w ≤ 0 ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y → ∀ y ∈ 0 +∞ 0 < y → ∃ z ∈ A z < y
29 28 adantrl ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ w ≤ 0 ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y → ∀ y ∈ 0 +∞ 0 < y → ∃ z ∈ A z < y
30 29 an32s ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y ∧ w ≤ 0 → ∀ y ∈ 0 +∞ 0 < y → ∃ z ∈ A z < y
31 0e0iccpnf ⊢ 0 ∈ 0 +∞
32 breq2 ⊢ x = 0 → y < x ↔ y < 0
33 32 notbid ⊢ x = 0 → ¬ y < x ↔ ¬ y < 0
34 33 ralbidv ⊢ x = 0 → ∀ y ∈ A ¬ y < x ↔ ∀ y ∈ A ¬ y < 0
35 breq1 ⊢ x = 0 → x < y ↔ 0 < y
36 35 imbi1d ⊢ x = 0 → x < y → ∃ z ∈ A z < y ↔ 0 < y → ∃ z ∈ A z < y
37 36 ralbidv ⊢ x = 0 → ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y ↔ ∀ y ∈ 0 +∞ 0 < y → ∃ z ∈ A z < y
38 34 37 anbi12d ⊢ x = 0 → ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y ↔ ∀ y ∈ A ¬ y < 0 ∧ ∀ y ∈ 0 +∞ 0 < y → ∃ z ∈ A z < y
39 38 rspcev ⊢ 0 ∈ 0 +∞ ∧ ∀ y ∈ A ¬ y < 0 ∧ ∀ y ∈ 0 +∞ 0 < y → ∃ z ∈ A z < y → ∃ x ∈ 0 +∞ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y
40 31 39 mpan ⊢ ∀ y ∈ A ¬ y < 0 ∧ ∀ y ∈ 0 +∞ 0 < y → ∃ z ∈ A z < y → ∃ x ∈ 0 +∞ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y
41 12 30 40 syl2anc ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y ∧ w ≤ 0 → ∃ x ∈ 0 +∞ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y
42 simpllr ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y ∧ 0 ≤ w → w ∈ ℝ *
43 simpr ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y ∧ 0 ≤ w → 0 ≤ w
44 elxrge0 ⊢ w ∈ 0 +∞ ↔ w ∈ ℝ * ∧ 0 ≤ w
45 42 43 44 sylanbrc ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y ∧ 0 ≤ w → w ∈ 0 +∞
46 15 a1i ⊢ A ⊆ 0 +∞ → ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y → ∀ y ∈ 0 +∞ w < y → ∃ z ∈ A z < y
47 46 anim2d ⊢ A ⊆ 0 +∞ → ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y → ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ 0 +∞ w < y → ∃ z ∈ A z < y
48 47 adantr ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * → ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y → ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ 0 +∞ w < y → ∃ z ∈ A z < y
49 48 imp ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y → ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ 0 +∞ w < y → ∃ z ∈ A z < y
50 49 adantr ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y ∧ 0 ≤ w → ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ 0 +∞ w < y → ∃ z ∈ A z < y
51 breq2 ⊢ x = w → y < x ↔ y < w
52 51 notbid ⊢ x = w → ¬ y < x ↔ ¬ y < w
53 52 ralbidv ⊢ x = w → ∀ y ∈ A ¬ y < x ↔ ∀ y ∈ A ¬ y < w
54 breq1 ⊢ x = w → x < y ↔ w < y
55 54 imbi1d ⊢ x = w → x < y → ∃ z ∈ A z < y ↔ w < y → ∃ z ∈ A z < y
56 55 ralbidv ⊢ x = w → ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y ↔ ∀ y ∈ 0 +∞ w < y → ∃ z ∈ A z < y
57 53 56 anbi12d ⊢ x = w → ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y ↔ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ 0 +∞ w < y → ∃ z ∈ A z < y
58 57 rspcev ⊢ w ∈ 0 +∞ ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ 0 +∞ w < y → ∃ z ∈ A z < y → ∃ x ∈ 0 +∞ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y
59 45 50 58 syl2anc ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y ∧ 0 ≤ w → ∃ x ∈ 0 +∞ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y
60 simplr ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y → w ∈ ℝ *
61 2 a1i ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y → 0 ∈ ℝ *
62 xrletri ⊢ w ∈ ℝ * ∧ 0 ∈ ℝ * → w ≤ 0 ∨ 0 ≤ w
63 60 61 62 syl2anc ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y → w ≤ 0 ∨ 0 ≤ w
64 41 59 63 mpjaodan ⊢ A ⊆ 0 +∞ ∧ w ∈ ℝ * ∧ ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y → ∃ x ∈ 0 +∞ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y
65 sstr ⊢ A ⊆ 0 +∞ ∧ 0 +∞ ⊆ ℝ * → A ⊆ ℝ *
66 13 65 mpan2 ⊢ A ⊆ 0 +∞ → A ⊆ ℝ *
67 xrinfmss ⊢ A ⊆ ℝ * → ∃ w ∈ ℝ * ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y
68 66 67 syl ⊢ A ⊆ 0 +∞ → ∃ w ∈ ℝ * ∀ y ∈ A ¬ y < w ∧ ∀ y ∈ ℝ * w < y → ∃ z ∈ A z < y
69 64 68 r19.29a ⊢ A ⊆ 0 +∞ → ∃ x ∈ 0 +∞ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ 0 +∞ x < y → ∃ z ∈ A z < y