Metamath Proof Explorer

Theorem infm3

Description: The completeness axiom for reals in terms of infimum: a nonempty, bounded-below set of reals has an infimum. (This theorem is the dual of sup3 .) (Contributed by NM, 14-Jun-2005)

Ref Expression
Assertion infm3 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y → ∃ x ∈ ℝ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y

Proof

Step Hyp Ref Expression
1 ssel ⊢ A ⊆ ℝ → v ∈ A → v ∈ ℝ
2 1 pm4.71rd ⊢ A ⊆ ℝ → v ∈ A ↔ v ∈ ℝ ∧ v ∈ A
3 2 exbidv ⊢ A ⊆ ℝ → ∃ v v ∈ A ↔ ∃ v v ∈ ℝ ∧ v ∈ A
4 df-rex ⊢ ∃ v ∈ ℝ v ∈ A ↔ ∃ v v ∈ ℝ ∧ v ∈ A
5 renegcl ⊢ w ∈ ℝ → − w ∈ ℝ
6 infm3lem ⊢ v ∈ ℝ → ∃ w ∈ ℝ v = − w
7 eleq1 ⊢ v = − w → v ∈ A ↔ − w ∈ A
8 5 6 7 rexxfr ⊢ ∃ v ∈ ℝ v ∈ A ↔ ∃ w ∈ ℝ − w ∈ A
9 4 8 bitr3i ⊢ ∃ v v ∈ ℝ ∧ v ∈ A ↔ ∃ w ∈ ℝ − w ∈ A
10 3 9 bitrdi ⊢ A ⊆ ℝ → ∃ v v ∈ A ↔ ∃ w ∈ ℝ − w ∈ A
11 n0 ⊢ A ≠ ∅ ↔ ∃ v v ∈ A
12 rabn0 ⊢ w ∈ ℝ | − w ∈ A ≠ ∅ ↔ ∃ w ∈ ℝ − w ∈ A
13 10 11 12 3bitr4g ⊢ A ⊆ ℝ → A ≠ ∅ ↔ w ∈ ℝ | − w ∈ A ≠ ∅
14 ssel ⊢ A ⊆ ℝ → y ∈ A → y ∈ ℝ
15 14 pm4.71rd ⊢ A ⊆ ℝ → y ∈ A ↔ y ∈ ℝ ∧ y ∈ A
16 15 imbi1d ⊢ A ⊆ ℝ → y ∈ A → x ≤ y ↔ y ∈ ℝ ∧ y ∈ A → x ≤ y
17 impexp ⊢ y ∈ ℝ ∧ y ∈ A → x ≤ y ↔ y ∈ ℝ → y ∈ A → x ≤ y
18 16 17 bitrdi ⊢ A ⊆ ℝ → y ∈ A → x ≤ y ↔ y ∈ ℝ → y ∈ A → x ≤ y
19 18 albidv ⊢ A ⊆ ℝ → ∀ y y ∈ A → x ≤ y ↔ ∀ y y ∈ ℝ → y ∈ A → x ≤ y
20 df-ral ⊢ ∀ y ∈ A x ≤ y ↔ ∀ y y ∈ A → x ≤ y
21 renegcl ⊢ v ∈ ℝ → − v ∈ ℝ
22 infm3lem ⊢ y ∈ ℝ → ∃ v ∈ ℝ y = − v
23 eleq1 ⊢ y = − v → y ∈ A ↔ − v ∈ A
24 breq2 ⊢ y = − v → x ≤ y ↔ x ≤ − v
25 23 24 imbi12d ⊢ y = − v → y ∈ A → x ≤ y ↔ − v ∈ A → x ≤ − v
26 21 22 25 ralxfr ⊢ ∀ y ∈ ℝ y ∈ A → x ≤ y ↔ ∀ v ∈ ℝ − v ∈ A → x ≤ − v
27 df-ral ⊢ ∀ y ∈ ℝ y ∈ A → x ≤ y ↔ ∀ y y ∈ ℝ → y ∈ A → x ≤ y
28 26 27 bitr3i ⊢ ∀ v ∈ ℝ − v ∈ A → x ≤ − v ↔ ∀ y y ∈ ℝ → y ∈ A → x ≤ y
29 19 20 28 3bitr4g ⊢ A ⊆ ℝ → ∀ y ∈ A x ≤ y ↔ ∀ v ∈ ℝ − v ∈ A → x ≤ − v
30 29 rexbidv ⊢ A ⊆ ℝ → ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ↔ ∃ x ∈ ℝ ∀ v ∈ ℝ − v ∈ A → x ≤ − v
31 renegcl ⊢ u ∈ ℝ → − u ∈ ℝ
32 infm3lem ⊢ x ∈ ℝ → ∃ u ∈ ℝ x = − u
33 breq1 ⊢ x = − u → x ≤ − v ↔ − u ≤ − v
34 33 imbi2d ⊢ x = − u → − v ∈ A → x ≤ − v ↔ − v ∈ A → − u ≤ − v
35 34 ralbidv ⊢ x = − u → ∀ v ∈ ℝ − v ∈ A → x ≤ − v ↔ ∀ v ∈ ℝ − v ∈ A → − u ≤ − v
36 31 32 35 rexxfr ⊢ ∃ x ∈ ℝ ∀ v ∈ ℝ − v ∈ A → x ≤ − v ↔ ∃ u ∈ ℝ ∀ v ∈ ℝ − v ∈ A → − u ≤ − v
37 negeq ⊢ w = v → − w = − v
38 37 eleq1d ⊢ w = v → − w ∈ A ↔ − v ∈ A
39 38 elrab ⊢ v ∈ w ∈ ℝ | − w ∈ A ↔ v ∈ ℝ ∧ − v ∈ A
40 39 imbi1i ⊢ v ∈ w ∈ ℝ | − w ∈ A → v ≤ u ↔ v ∈ ℝ ∧ − v ∈ A → v ≤ u
41 impexp ⊢ v ∈ ℝ ∧ − v ∈ A → v ≤ u ↔ v ∈ ℝ → − v ∈ A → v ≤ u
42 40 41 bitri ⊢ v ∈ w ∈ ℝ | − w ∈ A → v ≤ u ↔ v ∈ ℝ → − v ∈ A → v ≤ u
43 42 albii ⊢ ∀ v v ∈ w ∈ ℝ | − w ∈ A → v ≤ u ↔ ∀ v v ∈ ℝ → − v ∈ A → v ≤ u
44 df-ral ⊢ ∀ v ∈ w ∈ ℝ | − w ∈ A v ≤ u ↔ ∀ v v ∈ w ∈ ℝ | − w ∈ A → v ≤ u
45 df-ral ⊢ ∀ v ∈ ℝ − v ∈ A → v ≤ u ↔ ∀ v v ∈ ℝ → − v ∈ A → v ≤ u
46 43 44 45 3bitr4ri ⊢ ∀ v ∈ ℝ − v ∈ A → v ≤ u ↔ ∀ v ∈ w ∈ ℝ | − w ∈ A v ≤ u
47 leneg ⊢ v ∈ ℝ ∧ u ∈ ℝ → v ≤ u ↔ − u ≤ − v
48 47 ancoms ⊢ u ∈ ℝ ∧ v ∈ ℝ → v ≤ u ↔ − u ≤ − v
49 48 imbi2d ⊢ u ∈ ℝ ∧ v ∈ ℝ → − v ∈ A → v ≤ u ↔ − v ∈ A → − u ≤ − v
50 49 ralbidva ⊢ u ∈ ℝ → ∀ v ∈ ℝ − v ∈ A → v ≤ u ↔ ∀ v ∈ ℝ − v ∈ A → − u ≤ − v
51 46 50 bitr3id ⊢ u ∈ ℝ → ∀ v ∈ w ∈ ℝ | − w ∈ A v ≤ u ↔ ∀ v ∈ ℝ − v ∈ A → − u ≤ − v
52 51 rexbiia ⊢ ∃ u ∈ ℝ ∀ v ∈ w ∈ ℝ | − w ∈ A v ≤ u ↔ ∃ u ∈ ℝ ∀ v ∈ ℝ − v ∈ A → − u ≤ − v
53 36 52 bitr4i ⊢ ∃ x ∈ ℝ ∀ v ∈ ℝ − v ∈ A → x ≤ − v ↔ ∃ u ∈ ℝ ∀ v ∈ w ∈ ℝ | − w ∈ A v ≤ u
54 30 53 bitrdi ⊢ A ⊆ ℝ → ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ↔ ∃ u ∈ ℝ ∀ v ∈ w ∈ ℝ | − w ∈ A v ≤ u
55 13 54 anbi12d ⊢ A ⊆ ℝ → A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y ↔ w ∈ ℝ | − w ∈ A ≠ ∅ ∧ ∃ u ∈ ℝ ∀ v ∈ w ∈ ℝ | − w ∈ A v ≤ u
56 ssrab2 ⊢ w ∈ ℝ | − w ∈ A ⊆ ℝ
57 sup3 ⊢ w ∈ ℝ | − w ∈ A ⊆ ℝ ∧ w ∈ ℝ | − w ∈ A ≠ ∅ ∧ ∃ u ∈ ℝ ∀ v ∈ w ∈ ℝ | − w ∈ A v ≤ u → ∃ u ∈ ℝ ∀ v ∈ w ∈ ℝ | − w ∈ A ¬ u < v ∧ ∀ v ∈ ℝ v < u → ∃ t ∈ w ∈ ℝ | − w ∈ A v < t
58 56 57 mp3an1 ⊢ w ∈ ℝ | − w ∈ A ≠ ∅ ∧ ∃ u ∈ ℝ ∀ v ∈ w ∈ ℝ | − w ∈ A v ≤ u → ∃ u ∈ ℝ ∀ v ∈ w ∈ ℝ | − w ∈ A ¬ u < v ∧ ∀ v ∈ ℝ v < u → ∃ t ∈ w ∈ ℝ | − w ∈ A v < t
59 55 58 syl6bi ⊢ A ⊆ ℝ → A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y → ∃ u ∈ ℝ ∀ v ∈ w ∈ ℝ | − w ∈ A ¬ u < v ∧ ∀ v ∈ ℝ v < u → ∃ t ∈ w ∈ ℝ | − w ∈ A v < t
60 15 imbi1d ⊢ A ⊆ ℝ → y ∈ A → ¬ y < x ↔ y ∈ ℝ ∧ y ∈ A → ¬ y < x
61 impexp ⊢ y ∈ ℝ ∧ y ∈ A → ¬ y < x ↔ y ∈ ℝ → y ∈ A → ¬ y < x
62 60 61 bitrdi ⊢ A ⊆ ℝ → y ∈ A → ¬ y < x ↔ y ∈ ℝ → y ∈ A → ¬ y < x
63 62 albidv ⊢ A ⊆ ℝ → ∀ y y ∈ A → ¬ y < x ↔ ∀ y y ∈ ℝ → y ∈ A → ¬ y < x
64 df-ral ⊢ ∀ y ∈ A ¬ y < x ↔ ∀ y y ∈ A → ¬ y < x
65 breq1 ⊢ y = − v → y < x ↔ − v < x
66 65 notbid ⊢ y = − v → ¬ y < x ↔ ¬ − v < x
67 23 66 imbi12d ⊢ y = − v → y ∈ A → ¬ y < x ↔ − v ∈ A → ¬ − v < x
68 21 22 67 ralxfr ⊢ ∀ y ∈ ℝ y ∈ A → ¬ y < x ↔ ∀ v ∈ ℝ − v ∈ A → ¬ − v < x
69 df-ral ⊢ ∀ y ∈ ℝ y ∈ A → ¬ y < x ↔ ∀ y y ∈ ℝ → y ∈ A → ¬ y < x
70 68 69 bitr3i ⊢ ∀ v ∈ ℝ − v ∈ A → ¬ − v < x ↔ ∀ y y ∈ ℝ → y ∈ A → ¬ y < x
71 63 64 70 3bitr4g ⊢ A ⊆ ℝ → ∀ y ∈ A ¬ y < x ↔ ∀ v ∈ ℝ − v ∈ A → ¬ − v < x
72 breq2 ⊢ y = − v → x < y ↔ x < − v
73 breq2 ⊢ y = − v → z < y ↔ z < − v
74 73 rexbidv ⊢ y = − v → ∃ z ∈ A z < y ↔ ∃ z ∈ A z < − v
75 72 74 imbi12d ⊢ y = − v → x < y → ∃ z ∈ A z < y ↔ x < − v → ∃ z ∈ A z < − v
76 21 22 75 ralxfr ⊢ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y ↔ ∀ v ∈ ℝ x < − v → ∃ z ∈ A z < − v
77 ssel ⊢ A ⊆ ℝ → z ∈ A → z ∈ ℝ
78 77 adantrd ⊢ A ⊆ ℝ → z ∈ A ∧ z < − v → z ∈ ℝ
79 78 pm4.71rd ⊢ A ⊆ ℝ → z ∈ A ∧ z < − v ↔ z ∈ ℝ ∧ z ∈ A ∧ z < − v
80 79 exbidv ⊢ A ⊆ ℝ → ∃ z z ∈ A ∧ z < − v ↔ ∃ z z ∈ ℝ ∧ z ∈ A ∧ z < − v
81 df-rex ⊢ ∃ z ∈ A z < − v ↔ ∃ z z ∈ A ∧ z < − v
82 renegcl ⊢ t ∈ ℝ → − t ∈ ℝ
83 infm3lem ⊢ z ∈ ℝ → ∃ t ∈ ℝ z = − t
84 eleq1 ⊢ z = − t → z ∈ A ↔ − t ∈ A
85 breq1 ⊢ z = − t → z < − v ↔ − t < − v
86 84 85 anbi12d ⊢ z = − t → z ∈ A ∧ z < − v ↔ − t ∈ A ∧ − t < − v
87 82 83 86 rexxfr ⊢ ∃ z ∈ ℝ z ∈ A ∧ z < − v ↔ ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
88 df-rex ⊢ ∃ z ∈ ℝ z ∈ A ∧ z < − v ↔ ∃ z z ∈ ℝ ∧ z ∈ A ∧ z < − v
89 87 88 bitr3i ⊢ ∃ t ∈ ℝ − t ∈ A ∧ − t < − v ↔ ∃ z z ∈ ℝ ∧ z ∈ A ∧ z < − v
90 80 81 89 3bitr4g ⊢ A ⊆ ℝ → ∃ z ∈ A z < − v ↔ ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
91 90 imbi2d ⊢ A ⊆ ℝ → x < − v → ∃ z ∈ A z < − v ↔ x < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
92 91 ralbidv ⊢ A ⊆ ℝ → ∀ v ∈ ℝ x < − v → ∃ z ∈ A z < − v ↔ ∀ v ∈ ℝ x < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
93 76 92 syl5bb ⊢ A ⊆ ℝ → ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y ↔ ∀ v ∈ ℝ x < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
94 71 93 anbi12d ⊢ A ⊆ ℝ → ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y ↔ ∀ v ∈ ℝ − v ∈ A → ¬ − v < x ∧ ∀ v ∈ ℝ x < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
95 94 rexbidv ⊢ A ⊆ ℝ → ∃ x ∈ ℝ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y ↔ ∃ x ∈ ℝ ∀ v ∈ ℝ − v ∈ A → ¬ − v < x ∧ ∀ v ∈ ℝ x < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
96 breq2 ⊢ x = − u → − v < x ↔ − v < − u
97 96 notbid ⊢ x = − u → ¬ − v < x ↔ ¬ − v < − u
98 97 imbi2d ⊢ x = − u → − v ∈ A → ¬ − v < x ↔ − v ∈ A → ¬ − v < − u
99 98 ralbidv ⊢ x = − u → ∀ v ∈ ℝ − v ∈ A → ¬ − v < x ↔ ∀ v ∈ ℝ − v ∈ A → ¬ − v < − u
100 breq1 ⊢ x = − u → x < − v ↔ − u < − v
101 100 imbi1d ⊢ x = − u → x < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v ↔ − u < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
102 101 ralbidv ⊢ x = − u → ∀ v ∈ ℝ x < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v ↔ ∀ v ∈ ℝ − u < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
103 99 102 anbi12d ⊢ x = − u → ∀ v ∈ ℝ − v ∈ A → ¬ − v < x ∧ ∀ v ∈ ℝ x < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v ↔ ∀ v ∈ ℝ − v ∈ A → ¬ − v < − u ∧ ∀ v ∈ ℝ − u < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
104 31 32 103 rexxfr ⊢ ∃ x ∈ ℝ ∀ v ∈ ℝ − v ∈ A → ¬ − v < x ∧ ∀ v ∈ ℝ x < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v ↔ ∃ u ∈ ℝ ∀ v ∈ ℝ − v ∈ A → ¬ − v < − u ∧ ∀ v ∈ ℝ − u < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
105 39 imbi1i ⊢ v ∈ w ∈ ℝ | − w ∈ A → ¬ u < v ↔ v ∈ ℝ ∧ − v ∈ A → ¬ u < v
106 impexp ⊢ v ∈ ℝ ∧ − v ∈ A → ¬ u < v ↔ v ∈ ℝ → − v ∈ A → ¬ u < v
107 105 106 bitri ⊢ v ∈ w ∈ ℝ | − w ∈ A → ¬ u < v ↔ v ∈ ℝ → − v ∈ A → ¬ u < v
108 107 albii ⊢ ∀ v v ∈ w ∈ ℝ | − w ∈ A → ¬ u < v ↔ ∀ v v ∈ ℝ → − v ∈ A → ¬ u < v
109 df-ral ⊢ ∀ v ∈ w ∈ ℝ | − w ∈ A ¬ u < v ↔ ∀ v v ∈ w ∈ ℝ | − w ∈ A → ¬ u < v
110 df-ral ⊢ ∀ v ∈ ℝ − v ∈ A → ¬ u < v ↔ ∀ v v ∈ ℝ → − v ∈ A → ¬ u < v
111 108 109 110 3bitr4ri ⊢ ∀ v ∈ ℝ − v ∈ A → ¬ u < v ↔ ∀ v ∈ w ∈ ℝ | − w ∈ A ¬ u < v
112 ltneg ⊢ u ∈ ℝ ∧ v ∈ ℝ → u < v ↔ − v < − u
113 112 notbid ⊢ u ∈ ℝ ∧ v ∈ ℝ → ¬ u < v ↔ ¬ − v < − u
114 113 imbi2d ⊢ u ∈ ℝ ∧ v ∈ ℝ → − v ∈ A → ¬ u < v ↔ − v ∈ A → ¬ − v < − u
115 114 ralbidva ⊢ u ∈ ℝ → ∀ v ∈ ℝ − v ∈ A → ¬ u < v ↔ ∀ v ∈ ℝ − v ∈ A → ¬ − v < − u
116 111 115 bitr3id ⊢ u ∈ ℝ → ∀ v ∈ w ∈ ℝ | − w ∈ A ¬ u < v ↔ ∀ v ∈ ℝ − v ∈ A → ¬ − v < − u
117 ltneg ⊢ v ∈ ℝ ∧ u ∈ ℝ → v < u ↔ − u < − v
118 117 ancoms ⊢ u ∈ ℝ ∧ v ∈ ℝ → v < u ↔ − u < − v
119 negeq ⊢ w = t → − w = − t
120 119 eleq1d ⊢ w = t → − w ∈ A ↔ − t ∈ A
121 120 rexrab ⊢ ∃ t ∈ w ∈ ℝ | − w ∈ A v < t ↔ ∃ t ∈ ℝ − t ∈ A ∧ v < t
122 ltneg ⊢ v ∈ ℝ ∧ t ∈ ℝ → v < t ↔ − t < − v
123 122 anbi2d ⊢ v ∈ ℝ ∧ t ∈ ℝ → − t ∈ A ∧ v < t ↔ − t ∈ A ∧ − t < − v
124 123 rexbidva ⊢ v ∈ ℝ → ∃ t ∈ ℝ − t ∈ A ∧ v < t ↔ ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
125 121 124 syl5bb ⊢ v ∈ ℝ → ∃ t ∈ w ∈ ℝ | − w ∈ A v < t ↔ ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
126 125 adantl ⊢ u ∈ ℝ ∧ v ∈ ℝ → ∃ t ∈ w ∈ ℝ | − w ∈ A v < t ↔ ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
127 118 126 imbi12d ⊢ u ∈ ℝ ∧ v ∈ ℝ → v < u → ∃ t ∈ w ∈ ℝ | − w ∈ A v < t ↔ − u < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
128 127 ralbidva ⊢ u ∈ ℝ → ∀ v ∈ ℝ v < u → ∃ t ∈ w ∈ ℝ | − w ∈ A v < t ↔ ∀ v ∈ ℝ − u < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
129 116 128 anbi12d ⊢ u ∈ ℝ → ∀ v ∈ w ∈ ℝ | − w ∈ A ¬ u < v ∧ ∀ v ∈ ℝ v < u → ∃ t ∈ w ∈ ℝ | − w ∈ A v < t ↔ ∀ v ∈ ℝ − v ∈ A → ¬ − v < − u ∧ ∀ v ∈ ℝ − u < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
130 129 rexbiia ⊢ ∃ u ∈ ℝ ∀ v ∈ w ∈ ℝ | − w ∈ A ¬ u < v ∧ ∀ v ∈ ℝ v < u → ∃ t ∈ w ∈ ℝ | − w ∈ A v < t ↔ ∃ u ∈ ℝ ∀ v ∈ ℝ − v ∈ A → ¬ − v < − u ∧ ∀ v ∈ ℝ − u < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v
131 104 130 bitr4i ⊢ ∃ x ∈ ℝ ∀ v ∈ ℝ − v ∈ A → ¬ − v < x ∧ ∀ v ∈ ℝ x < − v → ∃ t ∈ ℝ − t ∈ A ∧ − t < − v ↔ ∃ u ∈ ℝ ∀ v ∈ w ∈ ℝ | − w ∈ A ¬ u < v ∧ ∀ v ∈ ℝ v < u → ∃ t ∈ w ∈ ℝ | − w ∈ A v < t
132 95 131 bitrdi ⊢ A ⊆ ℝ → ∃ x ∈ ℝ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y ↔ ∃ u ∈ ℝ ∀ v ∈ w ∈ ℝ | − w ∈ A ¬ u < v ∧ ∀ v ∈ ℝ v < u → ∃ t ∈ w ∈ ℝ | − w ∈ A v < t
133 59 132 sylibrd ⊢ A ⊆ ℝ → A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y → ∃ x ∈ ℝ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y
134 133 3impib ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A x ≤ y → ∃ x ∈ ℝ ∀ y ∈ A ¬ y < x ∧ ∀ y ∈ ℝ x < y → ∃ z ∈ A z < y