Metamath Proof Explorer


Theorem supminf

Description: The supremum of a bounded-above set of reals is the negation of the infimum of that set's image under negation. (Contributed by Paul Chapman, 21-Mar-2011) ( Revised by AV, 13-Sep-2020.)

Ref Expression
Assertion supminf AAxyAyxsupA<=supz|zA<

Proof

Step Hyp Ref Expression
1 ssrab2 z|zA
2 negn0 AAz|zA
3 ublbneg xyAyxxyz|zAxy
4 infrenegsup z|zAz|zAxyz|zAxysupz|zA<=supw|wz|zA<
5 1 2 3 4 mp3an3an AAxyAyxsupz|zA<=supw|wz|zA<
6 5 3impa AAxyAyxsupz|zA<=supw|wz|zA<
7 elrabi xw|wz|zAx
8 7 adantl Axw|wz|zAx
9 ssel2 AxAx
10 negeq w=xw=x
11 10 eleq1d w=xwz|zAxz|zA
12 11 elrab3 xxw|wz|zAxz|zA
13 renegcl xx
14 negeq z=xz=x
15 14 eleq1d z=xzAxA
16 15 elrab3 xxz|zAxA
17 13 16 syl xxz|zAxA
18 recn xx
19 18 negnegd xx=x
20 19 eleq1d xxAxA
21 12 17 20 3bitrd xxw|wz|zAxA
22 21 adantl Axxw|wz|zAxA
23 8 9 22 eqrdav Aw|wz|zA=A
24 23 supeq1d Asupw|wz|zA<=supA<
25 24 3ad2ant1 AAxyAyxsupw|wz|zA<=supA<
26 25 negeqd AAxyAyxsupw|wz|zA<=supA<
27 6 26 eqtrd AAxyAyxsupz|zA<=supA<
28 infrecl z|zAz|zAxyz|zAxysupz|zA<
29 1 2 3 28 mp3an3an AAxyAyxsupz|zA<
30 29 3impa AAxyAyxsupz|zA<
31 suprcl AAxyAyxsupA<
32 recn supz|zA<supz|zA<
33 recn supA<supA<
34 negcon2 supz|zA<supA<supz|zA<=supA<supA<=supz|zA<
35 32 33 34 syl2an supz|zA<supA<supz|zA<=supA<supA<=supz|zA<
36 30 31 35 syl2anc AAxyAyxsupz|zA<=supA<supA<=supz|zA<
37 27 36 mpbid AAxyAyxsupA<=supz|zA<