Metamath Proof Explorer


Theorem supminfxr2

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

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

Proof

Step Hyp Ref Expression
1 supminfxr2.1
 |-  ( ph -> A C_ RR* )
2 xnegmnf
 |-  -e -oo = +oo
3 2 eqcomi
 |-  +oo = -e -oo
4 3 a1i
 |-  ( ( ph /\ +oo e. A ) -> +oo = -e -oo )
5 supxrpnf
 |-  ( ( A C_ RR* /\ +oo e. A ) -> sup ( A , RR* , < ) = +oo )
6 1 5 sylan
 |-  ( ( ph /\ +oo e. A ) -> sup ( A , RR* , < ) = +oo )
7 ssrab2
 |-  { y e. RR* | -e y e. A } C_ RR*
8 7 a1i
 |-  ( +oo e. A -> { y e. RR* | -e y e. A } C_ RR* )
9 xnegeq
 |-  ( y = -oo -> -e y = -e -oo )
10 2 a1i
 |-  ( y = -oo -> -e -oo = +oo )
11 9 10 eqtrd
 |-  ( y = -oo -> -e y = +oo )
12 11 eleq1d
 |-  ( y = -oo -> ( -e y e. A <-> +oo e. A ) )
13 mnfxr
 |-  -oo e. RR*
14 13 a1i
 |-  ( +oo e. A -> -oo e. RR* )
15 id
 |-  ( +oo e. A -> +oo e. A )
16 12 14 15 elrabd
 |-  ( +oo e. A -> -oo e. { y e. RR* | -e y e. A } )
17 infxrmnf
 |-  ( ( { y e. RR* | -e y e. A } C_ RR* /\ -oo e. { y e. RR* | -e y e. A } ) -> inf ( { y e. RR* | -e y e. A } , RR* , < ) = -oo )
18 8 16 17 syl2anc
 |-  ( +oo e. A -> inf ( { y e. RR* | -e y e. A } , RR* , < ) = -oo )
19 18 adantl
 |-  ( ( ph /\ +oo e. A ) -> inf ( { y e. RR* | -e y e. A } , RR* , < ) = -oo )
20 19 xnegeqd
 |-  ( ( ph /\ +oo e. A ) -> -e inf ( { y e. RR* | -e y e. A } , RR* , < ) = -e -oo )
21 4 6 20 3eqtr4d
 |-  ( ( ph /\ +oo e. A ) -> sup ( A , RR* , < ) = -e inf ( { y e. RR* | -e y e. A } , RR* , < ) )
22 1 ssdifssd
 |-  ( ph -> ( A \ { -oo } ) C_ RR* )
23 22 adantr
 |-  ( ( ph /\ -. +oo e. A ) -> ( A \ { -oo } ) C_ RR* )
24 difssd
 |-  ( -. +oo e. A -> ( A \ { -oo } ) C_ A )
25 id
 |-  ( -. +oo e. A -> -. +oo e. A )
26 ssnel
 |-  ( ( ( A \ { -oo } ) C_ A /\ -. +oo e. A ) -> -. +oo e. ( A \ { -oo } ) )
27 24 25 26 syl2anc
 |-  ( -. +oo e. A -> -. +oo e. ( A \ { -oo } ) )
28 27 adantl
 |-  ( ( ph /\ -. +oo e. A ) -> -. +oo e. ( A \ { -oo } ) )
29 neldifsnd
 |-  ( ( ph /\ -. +oo e. A ) -> -. -oo e. ( A \ { -oo } ) )
30 23 28 29 xrssre
 |-  ( ( ph /\ -. +oo e. A ) -> ( A \ { -oo } ) C_ RR )
31 30 supminfxr
 |-  ( ( ph /\ -. +oo e. A ) -> sup ( ( A \ { -oo } ) , RR* , < ) = -e inf ( { y e. RR | -u y e. ( A \ { -oo } ) } , RR* , < ) )
32 supxrmnf2
 |-  ( A C_ RR* -> sup ( ( A \ { -oo } ) , RR* , < ) = sup ( A , RR* , < ) )
33 1 32 syl
 |-  ( ph -> sup ( ( A \ { -oo } ) , RR* , < ) = sup ( A , RR* , < ) )
34 33 eqcomd
 |-  ( ph -> sup ( A , RR* , < ) = sup ( ( A \ { -oo } ) , RR* , < ) )
35 34 adantr
 |-  ( ( ph /\ -. +oo e. A ) -> sup ( A , RR* , < ) = sup ( ( A \ { -oo } ) , RR* , < ) )
36 rexr
 |-  ( y e. RR -> y e. RR* )
37 36 adantr
 |-  ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> y e. RR* )
38 simpl
 |-  ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> y e. RR )
39 38 rexnegd
 |-  ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> -e y = -u y )
40 eldifi
 |-  ( -u y e. ( A \ { -oo } ) -> -u y e. A )
41 40 adantl
 |-  ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> -u y e. A )
42 39 41 eqeltrd
 |-  ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> -e y e. A )
43 37 42 jca
 |-  ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> ( y e. RR* /\ -e y e. A ) )
44 rabid
 |-  ( y e. { y e. RR* | -e y e. A } <-> ( y e. RR* /\ -e y e. A ) )
45 43 44 sylibr
 |-  ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> y e. { y e. RR* | -e y e. A } )
46 renepnf
 |-  ( y e. RR -> y =/= +oo )
47 elsni
 |-  ( y e. { +oo } -> y = +oo )
48 47 necon3ai
 |-  ( y =/= +oo -> -. y e. { +oo } )
49 46 48 syl
 |-  ( y e. RR -> -. y e. { +oo } )
50 38 49 syl
 |-  ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> -. y e. { +oo } )
51 45 50 eldifd
 |-  ( ( y e. RR /\ -u y e. ( A \ { -oo } ) ) -> y e. ( { y e. RR* | -e y e. A } \ { +oo } ) )
52 51 ex
 |-  ( y e. RR -> ( -u y e. ( A \ { -oo } ) -> y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) )
53 52 rgen
 |-  A. y e. RR ( -u y e. ( A \ { -oo } ) -> y e. ( { y e. RR* | -e y e. A } \ { +oo } ) )
54 53 a1i
 |-  ( -. +oo e. A -> A. y e. RR ( -u y e. ( A \ { -oo } ) -> y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) )
55 nfrab1
 |-  F/_ y { y e. RR* | -e y e. A }
56 nfcv
 |-  F/_ y { +oo }
57 55 56 nfdif
 |-  F/_ y ( { y e. RR* | -e y e. A } \ { +oo } )
58 57 rabssf
 |-  ( { y e. RR | -u y e. ( A \ { -oo } ) } C_ ( { y e. RR* | -e y e. A } \ { +oo } ) <-> A. y e. RR ( -u y e. ( A \ { -oo } ) -> y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) )
59 54 58 sylibr
 |-  ( -. +oo e. A -> { y e. RR | -u y e. ( A \ { -oo } ) } C_ ( { y e. RR* | -e y e. A } \ { +oo } ) )
60 nfv
 |-  F/ y -. +oo e. A
61 nfcv
 |-  F/_ y RR
62 eldifi
 |-  ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -> y e. { y e. RR* | -e y e. A } )
63 7 62 sseldi
 |-  ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -> y e. RR* )
64 63 adantl
 |-  ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> y e. RR* )
65 44 simprbi
 |-  ( y e. { y e. RR* | -e y e. A } -> -e y e. A )
66 62 65 syl
 |-  ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -> -e y e. A )
67 12 biimpac
 |-  ( ( -e y e. A /\ y = -oo ) -> +oo e. A )
68 67 adantll
 |-  ( ( ( -. +oo e. A /\ -e y e. A ) /\ y = -oo ) -> +oo e. A )
69 simpll
 |-  ( ( ( -. +oo e. A /\ -e y e. A ) /\ y = -oo ) -> -. +oo e. A )
70 68 69 pm2.65da
 |-  ( ( -. +oo e. A /\ -e y e. A ) -> -. y = -oo )
71 70 neqned
 |-  ( ( -. +oo e. A /\ -e y e. A ) -> y =/= -oo )
72 66 71 sylan2
 |-  ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> y =/= -oo )
73 eldifsni
 |-  ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -> y =/= +oo )
74 73 adantl
 |-  ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> y =/= +oo )
75 64 72 74 xrred
 |-  ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> y e. RR )
76 60 57 61 75 ssdf2
 |-  ( -. +oo e. A -> ( { y e. RR* | -e y e. A } \ { +oo } ) C_ RR )
77 75 rexnegd
 |-  ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> -e y = -u y )
78 66 adantl
 |-  ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> -e y e. A )
79 63 adantr
 |-  ( ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) /\ -e y e. { -oo } ) -> y e. RR* )
80 elsni
 |-  ( -e y e. { -oo } -> -e y = -oo )
81 80 adantl
 |-  ( ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) /\ -e y e. { -oo } ) -> -e y = -oo )
82 xnegeq
 |-  ( -e y = -oo -> -e -e y = -e -oo )
83 2 a1i
 |-  ( -e y = -oo -> -e -oo = +oo )
84 82 83 eqtr2d
 |-  ( -e y = -oo -> +oo = -e -e y )
85 84 adantl
 |-  ( ( y e. RR* /\ -e y = -oo ) -> +oo = -e -e y )
86 xnegneg
 |-  ( y e. RR* -> -e -e y = y )
87 86 adantr
 |-  ( ( y e. RR* /\ -e y = -oo ) -> -e -e y = y )
88 85 87 eqtr2d
 |-  ( ( y e. RR* /\ -e y = -oo ) -> y = +oo )
89 79 81 88 syl2anc
 |-  ( ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) /\ -e y e. { -oo } ) -> y = +oo )
90 73 neneqd
 |-  ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -> -. y = +oo )
91 90 adantr
 |-  ( ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) /\ -e y e. { -oo } ) -> -. y = +oo )
92 89 91 pm2.65da
 |-  ( y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -> -. -e y e. { -oo } )
93 92 adantl
 |-  ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> -. -e y e. { -oo } )
94 78 93 eldifd
 |-  ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> -e y e. ( A \ { -oo } ) )
95 77 94 eqeltrrd
 |-  ( ( -. +oo e. A /\ y e. ( { y e. RR* | -e y e. A } \ { +oo } ) ) -> -u y e. ( A \ { -oo } ) )
96 95 ralrimiva
 |-  ( -. +oo e. A -> A. y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -u y e. ( A \ { -oo } ) )
97 76 96 jca
 |-  ( -. +oo e. A -> ( ( { y e. RR* | -e y e. A } \ { +oo } ) C_ RR /\ A. y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -u y e. ( A \ { -oo } ) ) )
98 57 61 ssrabf
 |-  ( ( { y e. RR* | -e y e. A } \ { +oo } ) C_ { y e. RR | -u y e. ( A \ { -oo } ) } <-> ( ( { y e. RR* | -e y e. A } \ { +oo } ) C_ RR /\ A. y e. ( { y e. RR* | -e y e. A } \ { +oo } ) -u y e. ( A \ { -oo } ) ) )
99 97 98 sylibr
 |-  ( -. +oo e. A -> ( { y e. RR* | -e y e. A } \ { +oo } ) C_ { y e. RR | -u y e. ( A \ { -oo } ) } )
100 59 99 eqssd
 |-  ( -. +oo e. A -> { y e. RR | -u y e. ( A \ { -oo } ) } = ( { y e. RR* | -e y e. A } \ { +oo } ) )
101 100 infeq1d
 |-  ( -. +oo e. A -> inf ( { y e. RR | -u y e. ( A \ { -oo } ) } , RR* , < ) = inf ( ( { y e. RR* | -e y e. A } \ { +oo } ) , RR* , < ) )
102 infxrpnf2
 |-  ( { y e. RR* | -e y e. A } C_ RR* -> inf ( ( { y e. RR* | -e y e. A } \ { +oo } ) , RR* , < ) = inf ( { y e. RR* | -e y e. A } , RR* , < ) )
103 7 102 ax-mp
 |-  inf ( ( { y e. RR* | -e y e. A } \ { +oo } ) , RR* , < ) = inf ( { y e. RR* | -e y e. A } , RR* , < )
104 103 a1i
 |-  ( -. +oo e. A -> inf ( ( { y e. RR* | -e y e. A } \ { +oo } ) , RR* , < ) = inf ( { y e. RR* | -e y e. A } , RR* , < ) )
105 101 104 eqtr2d
 |-  ( -. +oo e. A -> inf ( { y e. RR* | -e y e. A } , RR* , < ) = inf ( { y e. RR | -u y e. ( A \ { -oo } ) } , RR* , < ) )
106 105 xnegeqd
 |-  ( -. +oo e. A -> -e inf ( { y e. RR* | -e y e. A } , RR* , < ) = -e inf ( { y e. RR | -u y e. ( A \ { -oo } ) } , RR* , < ) )
107 106 adantl
 |-  ( ( ph /\ -. +oo e. A ) -> -e inf ( { y e. RR* | -e y e. A } , RR* , < ) = -e inf ( { y e. RR | -u y e. ( A \ { -oo } ) } , RR* , < ) )
108 31 35 107 3eqtr4d
 |-  ( ( ph /\ -. +oo e. A ) -> sup ( A , RR* , < ) = -e inf ( { y e. RR* | -e y e. A } , RR* , < ) )
109 21 108 pm2.61dan
 |-  ( ph -> sup ( A , RR* , < ) = -e inf ( { y e. RR* | -e y e. A } , RR* , < ) )
110 xnegeq
 |-  ( y = x -> -e y = -e x )
111 110 eleq1d
 |-  ( y = x -> ( -e y e. A <-> -e x e. A ) )
112 111 cbvrabv
 |-  { y e. RR* | -e y e. A } = { x e. RR* | -e x e. A }
113 112 infeq1i
 |-  inf ( { y e. RR* | -e y e. A } , RR* , < ) = inf ( { x e. RR* | -e x e. A } , RR* , < )
114 113 xnegeqi
 |-  -e inf ( { y e. RR* | -e y e. A } , RR* , < ) = -e inf ( { x e. RR* | -e x e. A } , RR* , < )
115 114 a1i
 |-  ( ph -> -e inf ( { y e. RR* | -e y e. A } , RR* , < ) = -e inf ( { x e. RR* | -e x e. A } , RR* , < ) )
116 109 115 eqtrd
 |-  ( ph -> sup ( A , RR* , < ) = -e inf ( { x e. RR* | -e x e. A } , RR* , < ) )