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 C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> E. x e. RR ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) )

Proof

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