This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem supminfxrrnmpt

Description: The indexed supremum of a set of reals is the negation of the indexed infimum of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses supminfxrrnmpt.x 
|- F/ x ph
supminfxrrnmpt.b 
|- ( ( ph /\ x e. A ) -> B e. RR* )
Assertion supminfxrrnmpt 
|- ( ph -> sup ( ran ( x e. A |-> B ) , RR* , < ) = -e inf ( ran ( x e. A |-> -e B ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 supminfxrrnmpt.x 
 |-  F/ x ph
2 supminfxrrnmpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR* )
3 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
4 1 3 2 rnmptssd 
 |-  ( ph -> ran ( x e. A |-> B ) C_ RR* )
5 4 supminfxr2 
 |-  ( ph -> sup ( ran ( x e. A |-> B ) , RR* , < ) = -e inf ( { y e. RR* | -e y e. ran ( x e. A |-> B ) } , RR* , < ) )
6 xnegex 
 |-  -e y e. _V
7 3 elrnmpt 
 |-  ( -e y e. _V -> ( -e y e. ran ( x e. A |-> B ) <-> E. x e. A -e y = B ) )
8 6 7 ax-mp 
 |-  ( -e y e. ran ( x e. A |-> B ) <-> E. x e. A -e y = B )
9 8 biimpi 
 |-  ( -e y e. ran ( x e. A |-> B ) -> E. x e. A -e y = B )
10 eqid 
 |-  ( x e. A |-> -e B ) = ( x e. A |-> -e B )
11 xnegneg 
 |-  ( y e. RR* -> -e -e y = y )
12 11 eqcomd 
 |-  ( y e. RR* -> y = -e -e y )
13 12 adantr 
 |-  ( ( y e. RR* /\ -e y = B ) -> y = -e -e y )
14 xnegeq 
 |-  ( -e y = B -> -e -e y = -e B )
15 14 adantl 
 |-  ( ( y e. RR* /\ -e y = B ) -> -e -e y = -e B )
16 13 15 eqtrd 
 |-  ( ( y e. RR* /\ -e y = B ) -> y = -e B )
17 16 ex 
 |-  ( y e. RR* -> ( -e y = B -> y = -e B ) )
18 17 reximdv 
 |-  ( y e. RR* -> ( E. x e. A -e y = B -> E. x e. A y = -e B ) )
19 18 imp 
 |-  ( ( y e. RR* /\ E. x e. A -e y = B ) -> E. x e. A y = -e B )
20 simpl 
 |-  ( ( y e. RR* /\ E. x e. A -e y = B ) -> y e. RR* )
21 10 19 20 elrnmptd 
 |-  ( ( y e. RR* /\ E. x e. A -e y = B ) -> y e. ran ( x e. A |-> -e B ) )
22 9 21 sylan2 
 |-  ( ( y e. RR* /\ -e y e. ran ( x e. A |-> B ) ) -> y e. ran ( x e. A |-> -e B ) )
23 22 ex 
 |-  ( y e. RR* -> ( -e y e. ran ( x e. A |-> B ) -> y e. ran ( x e. A |-> -e B ) ) )
24 23 rgen 
 |-  A. y e. RR* ( -e y e. ran ( x e. A |-> B ) -> y e. ran ( x e. A |-> -e B ) )
25 rabss 
 |-  ( { y e. RR* | -e y e. ran ( x e. A |-> B ) } C_ ran ( x e. A |-> -e B ) <-> A. y e. RR* ( -e y e. ran ( x e. A |-> B ) -> y e. ran ( x e. A |-> -e B ) ) )
26 25 biimpri 
 |-  ( A. y e. RR* ( -e y e. ran ( x e. A |-> B ) -> y e. ran ( x e. A |-> -e B ) ) -> { y e. RR* | -e y e. ran ( x e. A |-> B ) } C_ ran ( x e. A |-> -e B ) )
27 24 26 ax-mp 
 |-  { y e. RR* | -e y e. ran ( x e. A |-> B ) } C_ ran ( x e. A |-> -e B )
28 27 a1i 
 |-  ( ph -> { y e. RR* | -e y e. ran ( x e. A |-> B ) } C_ ran ( x e. A |-> -e B ) )
29 nfcv 
 |-  F/_ x -e y
30 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
31 30 nfrn 
 |-  F/_ x ran ( x e. A |-> B )
32 29 31 nfel 
 |-  F/ x -e y e. ran ( x e. A |-> B )
33 nfcv 
 |-  F/_ x RR*
34 32 33 nfrabw 
 |-  F/_ x { y e. RR* | -e y e. ran ( x e. A |-> B ) }
35 xnegeq 
 |-  ( y = -e B -> -e y = -e -e B )
36 35 eleq1d 
 |-  ( y = -e B -> ( -e y e. ran ( x e. A |-> B ) <-> -e -e B e. ran ( x e. A |-> B ) ) )
37 2 xnegcld 
 |-  ( ( ph /\ x e. A ) -> -e B e. RR* )
38 xnegneg 
 |-  ( B e. RR* -> -e -e B = B )
39 2 38 syl 
 |-  ( ( ph /\ x e. A ) -> -e -e B = B )
40 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
41 3 40 2 elrnmpt1d 
 |-  ( ( ph /\ x e. A ) -> B e. ran ( x e. A |-> B ) )
42 39 41 eqeltrd 
 |-  ( ( ph /\ x e. A ) -> -e -e B e. ran ( x e. A |-> B ) )
43 36 37 42 elrabd 
 |-  ( ( ph /\ x e. A ) -> -e B e. { y e. RR* | -e y e. ran ( x e. A |-> B ) } )
44 1 34 10 43 rnmptssdf 
 |-  ( ph -> ran ( x e. A |-> -e B ) C_ { y e. RR* | -e y e. ran ( x e. A |-> B ) } )
45 28 44 eqssd 
 |-  ( ph -> { y e. RR* | -e y e. ran ( x e. A |-> B ) } = ran ( x e. A |-> -e B ) )
46 45 infeq1d 
 |-  ( ph -> inf ( { y e. RR* | -e y e. ran ( x e. A |-> B ) } , RR* , < ) = inf ( ran ( x e. A |-> -e B ) , RR* , < ) )
47 46 xnegeqd 
 |-  ( ph -> -e inf ( { y e. RR* | -e y e. ran ( x e. A |-> B ) } , RR* , < ) = -e inf ( ran ( x e. A |-> -e B ) , RR* , < ) )
48 5 47 eqtrd 
 |-  ( ph -> sup ( ran ( x e. A |-> B ) , RR* , < ) = -e inf ( ran ( x e. A |-> -e B ) , RR* , < ) )