Metamath Proof Explorer

Theorem supminfxr

Description: The extended real suprema of a set of reals is the extended real negative of the extended real infima of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis supminfxr.1 
|- ( ph -> A C_ RR )
Assertion supminfxr 
|- ( ph -> sup ( A , RR* , < ) = -e inf ( { x e. RR | -u x e. A } , RR* , < ) )

Proof

Step Hyp Ref Expression
1 supminfxr.1 
 |-  ( ph -> A C_ RR )
2 supeq1 
 |-  ( A = (/) -> sup ( A , RR* , < ) = sup ( (/) , RR* , < ) )
3 xrsup0 
 |-  sup ( (/) , RR* , < ) = -oo
4 3 a1i 
 |-  ( A = (/) -> sup ( (/) , RR* , < ) = -oo )
5 2 4 eqtrd 
 |-  ( A = (/) -> sup ( A , RR* , < ) = -oo )
6 5 adantl 
 |-  ( ( ph /\ A = (/) ) -> sup ( A , RR* , < ) = -oo )
7 eleq2 
 |-  ( A = (/) -> ( -u x e. A <-> -u x e. (/) ) )
8 7 rabbidv 
 |-  ( A = (/) -> { x e. RR | -u x e. A } = { x e. RR | -u x e. (/) } )
9 noel 
 |-  -. -u x e. (/)
10 9 a1i 
 |-  ( x e. RR -> -. -u x e. (/) )
11 10 rgen 
 |-  A. x e. RR -. -u x e. (/)
12 rabeq0 
 |-  ( { x e. RR | -u x e. (/) } = (/) <-> A. x e. RR -. -u x e. (/) )
13 11 12 mpbir 
 |-  { x e. RR | -u x e. (/) } = (/)
14 13 a1i 
 |-  ( A = (/) -> { x e. RR | -u x e. (/) } = (/) )
15 8 14 eqtrd 
 |-  ( A = (/) -> { x e. RR | -u x e. A } = (/) )
16 15 infeq1d 
 |-  ( A = (/) -> inf ( { x e. RR | -u x e. A } , RR* , < ) = inf ( (/) , RR* , < ) )
17 xrinf0 
 |-  inf ( (/) , RR* , < ) = +oo
18 17 a1i 
 |-  ( A = (/) -> inf ( (/) , RR* , < ) = +oo )
19 16 18 eqtrd 
 |-  ( A = (/) -> inf ( { x e. RR | -u x e. A } , RR* , < ) = +oo )
20 19 xnegeqd 
 |-  ( A = (/) -> -e inf ( { x e. RR | -u x e. A } , RR* , < ) = -e +oo )
21 xnegpnf 
 |-  -e +oo = -oo
22 21 a1i 
 |-  ( A = (/) -> -e +oo = -oo )
23 20 22 eqtrd 
 |-  ( A = (/) -> -e inf ( { x e. RR | -u x e. A } , RR* , < ) = -oo )
24 23 adantl 
 |-  ( ( ph /\ A = (/) ) -> -e inf ( { x e. RR | -u x e. A } , RR* , < ) = -oo )
25 6 24 eqtr4d 
 |-  ( ( ph /\ A = (/) ) -> sup ( A , RR* , < ) = -e inf ( { x e. RR | -u x e. A } , RR* , < ) )
26 neqne 
 |-  ( -. A = (/) -> A =/= (/) )
27 1 ad2antrr 
 |-  ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> A C_ RR )
28 simplr 
 |-  ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> A =/= (/) )
29 simpr 
 |-  ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> E. y e. RR A. z e. A z <_ y )
30 negn0 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> { x e. RR | -u x e. A } =/= (/) )
31 ublbneg 
 |-  ( E. y e. RR A. z e. A z <_ y -> E. y e. RR A. z e. { x e. RR | -u x e. A } y <_ z )
32 ssrab2 
 |-  { x e. RR | -u x e. A } C_ RR
33 infrenegsup 
 |-  ( ( { x e. RR | -u x e. A } C_ RR /\ { x e. RR | -u x e. A } =/= (/) /\ E. y e. RR A. z e. { x e. RR | -u x e. A } y <_ z ) -> inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( { w e. RR | -u w e. { x e. RR | -u x e. A } } , RR , < ) )
34 32 33 mp3an1 
 |-  ( ( { x e. RR | -u x e. A } =/= (/) /\ E. y e. RR A. z e. { x e. RR | -u x e. A } y <_ z ) -> inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( { w e. RR | -u w e. { x e. RR | -u x e. A } } , RR , < ) )
35 30 31 34 syl2an 
 |-  ( ( ( A C_ RR /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( { w e. RR | -u w e. { x e. RR | -u x e. A } } , RR , < ) )
36 35 3impa 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( { w e. RR | -u w e. { x e. RR | -u x e. A } } , RR , < ) )
37 elrabi 
 |-  ( y e. { w e. RR | -u w e. { x e. RR | -u x e. A } } -> y e. RR )
38 37 adantl 
 |-  ( ( A C_ RR /\ y e. { w e. RR | -u w e. { x e. RR | -u x e. A } } ) -> y e. RR )
39 ssel2 
 |-  ( ( A C_ RR /\ y e. A ) -> y e. RR )
40 negeq 
 |-  ( w = y -> -u w = -u y )
41 40 eleq1d 
 |-  ( w = y -> ( -u w e. { x e. RR | -u x e. A } <-> -u y e. { x e. RR | -u x e. A } ) )
42 41 elrab3 
 |-  ( y e. RR -> ( y e. { w e. RR | -u w e. { x e. RR | -u x e. A } } <-> -u y e. { x e. RR | -u x e. A } ) )
43 renegcl 
 |-  ( y e. RR -> -u y e. RR )
44 negeq 
 |-  ( x = -u y -> -u x = -u -u y )
45 44 eleq1d 
 |-  ( x = -u y -> ( -u x e. A <-> -u -u y e. A ) )
46 45 elrab3 
 |-  ( -u y e. RR -> ( -u y e. { x e. RR | -u x e. A } <-> -u -u y e. A ) )
47 43 46 syl 
 |-  ( y e. RR -> ( -u y e. { x e. RR | -u x e. A } <-> -u -u y e. A ) )
48 recn 
 |-  ( y e. RR -> y e. CC )
49 48 negnegd 
 |-  ( y e. RR -> -u -u y = y )
50 49 eleq1d 
 |-  ( y e. RR -> ( -u -u y e. A <-> y e. A ) )
51 42 47 50 3bitrd 
 |-  ( y e. RR -> ( y e. { w e. RR | -u w e. { x e. RR | -u x e. A } } <-> y e. A ) )
52 51 adantl 
 |-  ( ( A C_ RR /\ y e. RR ) -> ( y e. { w e. RR | -u w e. { x e. RR | -u x e. A } } <-> y e. A ) )
53 38 39 52 eqrdav 
 |-  ( A C_ RR -> { w e. RR | -u w e. { x e. RR | -u x e. A } } = A )
54 53 supeq1d 
 |-  ( A C_ RR -> sup ( { w e. RR | -u w e. { x e. RR | -u x e. A } } , RR , < ) = sup ( A , RR , < ) )
55 54 3ad2ant1 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( { w e. RR | -u w e. { x e. RR | -u x e. A } } , RR , < ) = sup ( A , RR , < ) )
56 55 negeqd 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> -u sup ( { w e. RR | -u w e. { x e. RR | -u x e. A } } , RR , < ) = -u sup ( A , RR , < ) )
57 36 56 eqtrd 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( A , RR , < ) )
58 infrecl 
 |-  ( ( { x e. RR | -u x e. A } C_ RR /\ { x e. RR | -u x e. A } =/= (/) /\ E. y e. RR A. z e. { x e. RR | -u x e. A } y <_ z ) -> inf ( { x e. RR | -u x e. A } , RR , < ) e. RR )
59 32 58 mp3an1 
 |-  ( ( { x e. RR | -u x e. A } =/= (/) /\ E. y e. RR A. z e. { x e. RR | -u x e. A } y <_ z ) -> inf ( { x e. RR | -u x e. A } , RR , < ) e. RR )
60 30 31 59 syl2an 
 |-  ( ( ( A C_ RR /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> inf ( { x e. RR | -u x e. A } , RR , < ) e. RR )
61 60 3impa 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> inf ( { x e. RR | -u x e. A } , RR , < ) e. RR )
62 suprcl 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR , < ) e. RR )
63 recn 
 |-  ( inf ( { x e. RR | -u x e. A } , RR , < ) e. RR -> inf ( { x e. RR | -u x e. A } , RR , < ) e. CC )
64 recn 
 |-  ( sup ( A , RR , < ) e. RR -> sup ( A , RR , < ) e. CC )
65 negcon2 
 |-  ( ( inf ( { x e. RR | -u x e. A } , RR , < ) e. CC /\ sup ( A , RR , < ) e. CC ) -> ( inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( A , RR , < ) <-> sup ( A , RR , < ) = -u inf ( { x e. RR | -u x e. A } , RR , < ) ) )
66 63 64 65 syl2an 
 |-  ( ( inf ( { x e. RR | -u x e. A } , RR , < ) e. RR /\ sup ( A , RR , < ) e. RR ) -> ( inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( A , RR , < ) <-> sup ( A , RR , < ) = -u inf ( { x e. RR | -u x e. A } , RR , < ) ) )
67 61 62 66 syl2anc 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> ( inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( A , RR , < ) <-> sup ( A , RR , < ) = -u inf ( { x e. RR | -u x e. A } , RR , < ) ) )
68 57 67 mpbid 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR , < ) = -u inf ( { x e. RR | -u x e. A } , RR , < ) )
69 27 28 29 68 syl3anc 
 |-  ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR , < ) = -u inf ( { x e. RR | -u x e. A } , RR , < ) )
70 supxrre 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR* , < ) = sup ( A , RR , < ) )
71 27 28 29 70 syl3anc 
 |-  ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR* , < ) = sup ( A , RR , < ) )
72 32 a1i 
 |-  ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> { x e. RR | -u x e. A } C_ RR )
73 27 28 30 syl2anc 
 |-  ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> { x e. RR | -u x e. A } =/= (/) )
74 29 31 syl 
 |-  ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> E. y e. RR A. z e. { x e. RR | -u x e. A } y <_ z )
75 infxrre 
 |-  ( ( { x e. RR | -u x e. A } C_ RR /\ { x e. RR | -u x e. A } =/= (/) /\ E. y e. RR A. z e. { x e. RR | -u x e. A } y <_ z ) -> inf ( { x e. RR | -u x e. A } , RR* , < ) = inf ( { x e. RR | -u x e. A } , RR , < ) )
76 72 73 74 75 syl3anc 
 |-  ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> inf ( { x e. RR | -u x e. A } , RR* , < ) = inf ( { x e. RR | -u x e. A } , RR , < ) )
77 76 xnegeqd 
 |-  ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> -e inf ( { x e. RR | -u x e. A } , RR* , < ) = -e inf ( { x e. RR | -u x e. A } , RR , < ) )
78 1 60 sylanl1 
 |-  ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> inf ( { x e. RR | -u x e. A } , RR , < ) e. RR )
79 78 rexnegd 
 |-  ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> -e inf ( { x e. RR | -u x e. A } , RR , < ) = -u inf ( { x e. RR | -u x e. A } , RR , < ) )
80 77 79 eqtrd 
 |-  ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> -e inf ( { x e. RR | -u x e. A } , RR* , < ) = -u inf ( { x e. RR | -u x e. A } , RR , < ) )
81 69 71 80 3eqtr4d 
 |-  ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR* , < ) = -e inf ( { x e. RR | -u x e. A } , RR* , < ) )
82 simpr 
 |-  ( ( ph /\ -. E. y e. RR A. z e. A z <_ y ) -> -. E. y e. RR A. z e. A z <_ y )
83 simplr 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. A ) -> y e. RR )
84 1 sselda 
 |-  ( ( ph /\ z e. A ) -> z e. RR )
85 84 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. A ) -> z e. RR )
86 83 85 ltnled 
 |-  ( ( ( ph /\ y e. RR ) /\ z e. A ) -> ( y < z <-> -. z <_ y ) )
87 86 rexbidva 
 |-  ( ( ph /\ y e. RR ) -> ( E. z e. A y < z <-> E. z e. A -. z <_ y ) )
88 rexnal 
 |-  ( E. z e. A -. z <_ y <-> -. A. z e. A z <_ y )
89 88 a1i 
 |-  ( ( ph /\ y e. RR ) -> ( E. z e. A -. z <_ y <-> -. A. z e. A z <_ y ) )
90 87 89 bitrd 
 |-  ( ( ph /\ y e. RR ) -> ( E. z e. A y < z <-> -. A. z e. A z <_ y ) )
91 90 ralbidva 
 |-  ( ph -> ( A. y e. RR E. z e. A y < z <-> A. y e. RR -. A. z e. A z <_ y ) )
92 ralnex 
 |-  ( A. y e. RR -. A. z e. A z <_ y <-> -. E. y e. RR A. z e. A z <_ y )
93 92 a1i 
 |-  ( ph -> ( A. y e. RR -. A. z e. A z <_ y <-> -. E. y e. RR A. z e. A z <_ y ) )
94 91 93 bitrd 
 |-  ( ph -> ( A. y e. RR E. z e. A y < z <-> -. E. y e. RR A. z e. A z <_ y ) )
95 94 adantr 
 |-  ( ( ph /\ -. E. y e. RR A. z e. A z <_ y ) -> ( A. y e. RR E. z e. A y < z <-> -. E. y e. RR A. z e. A z <_ y ) )
96 82 95 mpbird 
 |-  ( ( ph /\ -. E. y e. RR A. z e. A z <_ y ) -> A. y e. RR E. z e. A y < z )
97 xnegmnf 
 |-  -e -oo = +oo
98 97 eqcomi 
 |-  +oo = -e -oo
99 98 a1i 
 |-  ( ( ph /\ A. y e. RR E. z e. A y < z ) -> +oo = -e -oo )
100 simpr 
 |-  ( ( ph /\ A. y e. RR E. z e. A y < z ) -> A. y e. RR E. z e. A y < z )
101 ressxr 
 |-  RR C_ RR*
102 101 a1i 
 |-  ( ph -> RR C_ RR* )
103 1 102 sstrd 
 |-  ( ph -> A C_ RR* )
104 supxrunb2 
 |-  ( A C_ RR* -> ( A. y e. RR E. z e. A y < z <-> sup ( A , RR* , < ) = +oo ) )
105 103 104 syl 
 |-  ( ph -> ( A. y e. RR E. z e. A y < z <-> sup ( A , RR* , < ) = +oo ) )
106 105 adantr 
 |-  ( ( ph /\ A. y e. RR E. z e. A y < z ) -> ( A. y e. RR E. z e. A y < z <-> sup ( A , RR* , < ) = +oo ) )
107 100 106 mpbid 
 |-  ( ( ph /\ A. y e. RR E. z e. A y < z ) -> sup ( A , RR* , < ) = +oo )
108 renegcl 
 |-  ( v e. RR -> -u v e. RR )
109 108 adantl 
 |-  ( ( A. y e. RR E. z e. A y < z /\ v e. RR ) -> -u v e. RR )
110 simpl 
 |-  ( ( A. y e. RR E. z e. A y < z /\ v e. RR ) -> A. y e. RR E. z e. A y < z )
111 breq1 
 |-  ( y = -u v -> ( y < z <-> -u v < z ) )
112 111 rexbidv 
 |-  ( y = -u v -> ( E. z e. A y < z <-> E. z e. A -u v < z ) )
113 112 rspcva 
 |-  ( ( -u v e. RR /\ A. y e. RR E. z e. A y < z ) -> E. z e. A -u v < z )
114 109 110 113 syl2anc 
 |-  ( ( A. y e. RR E. z e. A y < z /\ v e. RR ) -> E. z e. A -u v < z )
115 114 adantll 
 |-  ( ( ( ph /\ A. y e. RR E. z e. A y < z ) /\ v e. RR ) -> E. z e. A -u v < z )
116 negeq 
 |-  ( x = -u z -> -u x = -u -u z )
117 116 eleq1d 
 |-  ( x = -u z -> ( -u x e. A <-> -u -u z e. A ) )
118 84 renegcld 
 |-  ( ( ph /\ z e. A ) -> -u z e. RR )
119 118 ad4ant13 
 |-  ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u z e. RR )
120 84 recnd 
 |-  ( ( ph /\ z e. A ) -> z e. CC )
121 120 negnegd 
 |-  ( ( ph /\ z e. A ) -> -u -u z = z )
122 simpr 
 |-  ( ( ph /\ z e. A ) -> z e. A )
123 121 122 eqeltrd 
 |-  ( ( ph /\ z e. A ) -> -u -u z e. A )
124 123 ad4ant13 
 |-  ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u -u z e. A )
125 117 119 124 elrabd 
 |-  ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u z e. { x e. RR | -u x e. A } )
126 simpr 
 |-  ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u v < z )
127 108 ad3antlr 
 |-  ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u v e. RR )
128 84 ad4ant13 
 |-  ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> z e. RR )
129 127 128 ltnegd 
 |-  ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> ( -u v < z <-> -u z < -u -u v ) )
130 126 129 mpbid 
 |-  ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u z < -u -u v )
131 simpllr 
 |-  ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> v e. RR )
132 recn 
 |-  ( v e. RR -> v e. CC )
133 negneg 
 |-  ( v e. CC -> -u -u v = v )
134 131 132 133 3syl 
 |-  ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u -u v = v )
135 130 134 breqtrd 
 |-  ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u z < v )
136 breq1 
 |-  ( w = -u z -> ( w < v <-> -u z < v ) )
137 136 rspcev 
 |-  ( ( -u z e. { x e. RR | -u x e. A } /\ -u z < v ) -> E. w e. { x e. RR | -u x e. A } w < v )
138 125 135 137 syl2anc 
 |-  ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> E. w e. { x e. RR | -u x e. A } w < v )
139 138 rexlimdva2 
 |-  ( ( ph /\ v e. RR ) -> ( E. z e. A -u v < z -> E. w e. { x e. RR | -u x e. A } w < v ) )
140 139 adantlr 
 |-  ( ( ( ph /\ A. y e. RR E. z e. A y < z ) /\ v e. RR ) -> ( E. z e. A -u v < z -> E. w e. { x e. RR | -u x e. A } w < v ) )
141 115 140 mpd 
 |-  ( ( ( ph /\ A. y e. RR E. z e. A y < z ) /\ v e. RR ) -> E. w e. { x e. RR | -u x e. A } w < v )
142 141 ralrimiva 
 |-  ( ( ph /\ A. y e. RR E. z e. A y < z ) -> A. v e. RR E. w e. { x e. RR | -u x e. A } w < v )
143 32 101 sstri 
 |-  { x e. RR | -u x e. A } C_ RR*
144 infxrunb2 
 |-  ( { x e. RR | -u x e. A } C_ RR* -> ( A. v e. RR E. w e. { x e. RR | -u x e. A } w < v <-> inf ( { x e. RR | -u x e. A } , RR* , < ) = -oo ) )
145 143 144 ax-mp 
 |-  ( A. v e. RR E. w e. { x e. RR | -u x e. A } w < v <-> inf ( { x e. RR | -u x e. A } , RR* , < ) = -oo )
146 142 145 sylib 
 |-  ( ( ph /\ A. y e. RR E. z e. A y < z ) -> inf ( { x e. RR | -u x e. A } , RR* , < ) = -oo )
147 146 xnegeqd 
 |-  ( ( ph /\ A. y e. RR E. z e. A y < z ) -> -e inf ( { x e. RR | -u x e. A } , RR* , < ) = -e -oo )
148 99 107 147 3eqtr4d 
 |-  ( ( ph /\ A. y e. RR E. z e. A y < z ) -> sup ( A , RR* , < ) = -e inf ( { x e. RR | -u x e. A } , RR* , < ) )
149 96 148 syldan 
 |-  ( ( ph /\ -. E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR* , < ) = -e inf ( { x e. RR | -u x e. A } , RR* , < ) )
150 149 adantlr 
 |-  ( ( ( ph /\ A =/= (/) ) /\ -. E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR* , < ) = -e inf ( { x e. RR | -u x e. A } , RR* , < ) )
151 81 150 pm2.61dan 
 |-  ( ( ph /\ A =/= (/) ) -> sup ( A , RR* , < ) = -e inf ( { x e. RR | -u x e. A } , RR* , < ) )
152 26 151 sylan2 
 |-  ( ( ph /\ -. A = (/) ) -> sup ( A , RR* , < ) = -e inf ( { x e. RR | -u x e. A } , RR* , < ) )
153 25 152 pm2.61dan 
 |-  ( ph -> sup ( A , RR* , < ) = -e inf ( { x e. RR | -u x e. A } , RR* , < ) )