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 sselid 
 |-  ( 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* , < ) )