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