Metamath Proof Explorer

Theorem supminfrnmpt

Description: The indexed supremum of a bounded-above 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 supminfrnmpt.x 
|- F/ x ph
supminfrnmpt.a 
|- ( ph -> A =/= (/) )
supminfrnmpt.b 
|- ( ( ph /\ x e. A ) -> B e. RR )
supminfrnmpt.y 
|- ( ph -> E. y e. RR A. x e. A B <_ y )
Assertion supminfrnmpt 
|- ( ph -> sup ( ran ( x e. A |-> B ) , RR , < ) = -u inf ( ran ( x e. A |-> -u B ) , RR , < ) )

Proof

Step Hyp Ref Expression
1 supminfrnmpt.x 
 |-  F/ x ph
2 supminfrnmpt.a 
 |-  ( ph -> A =/= (/) )
3 supminfrnmpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
4 supminfrnmpt.y 
 |-  ( ph -> E. y e. RR A. x e. A B <_ y )
5 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
6 1 5 3 rnmptssd 
 |-  ( ph -> ran ( x e. A |-> B ) C_ RR )
7 1 3 5 2 rnmptn0 
 |-  ( ph -> ran ( x e. A |-> B ) =/= (/) )
8 1 3 rnmptbd 
 |-  ( ph -> ( E. y e. RR A. x e. A B <_ y <-> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y ) )
9 4 8 mpbid 
 |-  ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y )
10 supminf 
 |-  ( ( ran ( x e. A |-> B ) C_ RR /\ ran ( x e. A |-> B ) =/= (/) /\ E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y ) -> sup ( ran ( x e. A |-> B ) , RR , < ) = -u inf ( { w e. RR | -u w e. ran ( x e. A |-> B ) } , RR , < ) )
11 6 7 9 10 syl3anc 
 |-  ( ph -> sup ( ran ( x e. A |-> B ) , RR , < ) = -u inf ( { w e. RR | -u w e. ran ( x e. A |-> B ) } , RR , < ) )
12 eqid 
 |-  ( x e. A |-> -u B ) = ( x e. A |-> -u B )
13 simpr 
 |-  ( ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) -> -u w e. ran ( x e. A |-> B ) )
14 renegcl 
 |-  ( w e. RR -> -u w e. RR )
15 5 elrnmpt 
 |-  ( -u w e. RR -> ( -u w e. ran ( x e. A |-> B ) <-> E. x e. A -u w = B ) )
16 14 15 syl 
 |-  ( w e. RR -> ( -u w e. ran ( x e. A |-> B ) <-> E. x e. A -u w = B ) )
17 16 adantr 
 |-  ( ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) -> ( -u w e. ran ( x e. A |-> B ) <-> E. x e. A -u w = B ) )
18 13 17 mpbid 
 |-  ( ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) -> E. x e. A -u w = B )
19 18 adantll 
 |-  ( ( ( ph /\ w e. RR ) /\ -u w e. ran ( x e. A |-> B ) ) -> E. x e. A -u w = B )
20 nfv 
 |-  F/ x w e. RR
21 1 20 nfan 
 |-  F/ x ( ph /\ w e. RR )
22 negeq 
 |-  ( -u w = B -> -u -u w = -u B )
23 22 eqcomd 
 |-  ( -u w = B -> -u B = -u -u w )
24 23 adantl 
 |-  ( ( w e. RR /\ -u w = B ) -> -u B = -u -u w )
25 recn 
 |-  ( w e. RR -> w e. CC )
26 25 negnegd 
 |-  ( w e. RR -> -u -u w = w )
27 26 adantr 
 |-  ( ( w e. RR /\ -u w = B ) -> -u -u w = w )
28 24 27 eqtr2d 
 |-  ( ( w e. RR /\ -u w = B ) -> w = -u B )
29 28 ex 
 |-  ( w e. RR -> ( -u w = B -> w = -u B ) )
30 29 adantl 
 |-  ( ( ph /\ w e. RR ) -> ( -u w = B -> w = -u B ) )
31 30 adantr 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A ) -> ( -u w = B -> w = -u B ) )
32 negeq 
 |-  ( w = -u B -> -u w = -u -u B )
33 32 adantl 
 |-  ( ( ( ph /\ x e. A ) /\ w = -u B ) -> -u w = -u -u B )
34 3 recnd 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
35 34 negnegd 
 |-  ( ( ph /\ x e. A ) -> -u -u B = B )
36 35 adantr 
 |-  ( ( ( ph /\ x e. A ) /\ w = -u B ) -> -u -u B = B )
37 33 36 eqtrd 
 |-  ( ( ( ph /\ x e. A ) /\ w = -u B ) -> -u w = B )
38 37 ex 
 |-  ( ( ph /\ x e. A ) -> ( w = -u B -> -u w = B ) )
39 38 adantlr 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A ) -> ( w = -u B -> -u w = B ) )
40 31 39 impbid 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A ) -> ( -u w = B <-> w = -u B ) )
41 21 40 rexbida 
 |-  ( ( ph /\ w e. RR ) -> ( E. x e. A -u w = B <-> E. x e. A w = -u B ) )
42 41 adantr 
 |-  ( ( ( ph /\ w e. RR ) /\ -u w e. ran ( x e. A |-> B ) ) -> ( E. x e. A -u w = B <-> E. x e. A w = -u B ) )
43 19 42 mpbid 
 |-  ( ( ( ph /\ w e. RR ) /\ -u w e. ran ( x e. A |-> B ) ) -> E. x e. A w = -u B )
44 simplr 
 |-  ( ( ( ph /\ w e. RR ) /\ -u w e. ran ( x e. A |-> B ) ) -> w e. RR )
45 12 43 44 elrnmptd 
 |-  ( ( ( ph /\ w e. RR ) /\ -u w e. ran ( x e. A |-> B ) ) -> w e. ran ( x e. A |-> -u B ) )
46 45 ex 
 |-  ( ( ph /\ w e. RR ) -> ( -u w e. ran ( x e. A |-> B ) -> w e. ran ( x e. A |-> -u B ) ) )
47 46 ralrimiva 
 |-  ( ph -> A. w e. RR ( -u w e. ran ( x e. A |-> B ) -> w e. ran ( x e. A |-> -u B ) ) )
48 rabss 
 |-  ( { w e. RR | -u w e. ran ( x e. A |-> B ) } C_ ran ( x e. A |-> -u B ) <-> A. w e. RR ( -u w e. ran ( x e. A |-> B ) -> w e. ran ( x e. A |-> -u B ) ) )
49 47 48 sylibr 
 |-  ( ph -> { w e. RR | -u w e. ran ( x e. A |-> B ) } C_ ran ( x e. A |-> -u B ) )
50 nfcv 
 |-  F/_ x -u w
51 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
52 51 nfrn 
 |-  F/_ x ran ( x e. A |-> B )
53 50 52 nfel 
 |-  F/ x -u w e. ran ( x e. A |-> B )
54 nfcv 
 |-  F/_ x RR
55 53 54 nfrabw 
 |-  F/_ x { w e. RR | -u w e. ran ( x e. A |-> B ) }
56 32 eleq1d 
 |-  ( w = -u B -> ( -u w e. ran ( x e. A |-> B ) <-> -u -u B e. ran ( x e. A |-> B ) ) )
57 3 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. RR )
58 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
59 5 elrnmpt1 
 |-  ( ( x e. A /\ B e. RR ) -> B e. ran ( x e. A |-> B ) )
60 58 3 59 syl2anc 
 |-  ( ( ph /\ x e. A ) -> B e. ran ( x e. A |-> B ) )
61 35 60 eqeltrd 
 |-  ( ( ph /\ x e. A ) -> -u -u B e. ran ( x e. A |-> B ) )
62 56 57 61 elrabd 
 |-  ( ( ph /\ x e. A ) -> -u B e. { w e. RR | -u w e. ran ( x e. A |-> B ) } )
63 1 55 12 62 rnmptssdf 
 |-  ( ph -> ran ( x e. A |-> -u B ) C_ { w e. RR | -u w e. ran ( x e. A |-> B ) } )
64 49 63 eqssd 
 |-  ( ph -> { w e. RR | -u w e. ran ( x e. A |-> B ) } = ran ( x e. A |-> -u B ) )
65 64 infeq1d 
 |-  ( ph -> inf ( { w e. RR | -u w e. ran ( x e. A |-> B ) } , RR , < ) = inf ( ran ( x e. A |-> -u B ) , RR , < ) )
66 65 negeqd 
 |-  ( ph -> -u inf ( { w e. RR | -u w e. ran ( x e. A |-> B ) } , RR , < ) = -u inf ( ran ( x e. A |-> -u B ) , RR , < ) )
67 11 66 eqtrd 
 |-  ( ph -> sup ( ran ( x e. A |-> B ) , RR , < ) = -u inf ( ran ( x e. A |-> -u B ) , RR , < ) )