Metamath Proof Explorer

Theorem infrenegsup

Description: The infimum of a set of reals A is the negative of the supremum of the negatives of its elements. The antecedent ensures that A is nonempty and has a lower bound. (Contributed by NM, 14-Jun-2005) (Revised by AV, 4-Sep-2020)

Ref Expression
Assertion infrenegsup 
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> inf ( A , RR , < ) = -u sup ( { z e. RR | -u z e. A } , RR , < ) )

Proof

Step Hyp Ref Expression
1 infrecl 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> inf ( A , RR , < ) e. RR )
2 1 recnd 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> inf ( A , RR , < ) e. CC )
3 2 negnegd 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> -u -u inf ( A , RR , < ) = inf ( A , RR , < ) )
4 negeq 
 |-  ( w = z -> -u w = -u z )
5 4 cbvmptv 
 |-  ( w e. RR |-> -u w ) = ( z e. RR |-> -u z )
6 5 mptpreima 
 |-  ( `' ( w e. RR |-> -u w ) " A ) = { z e. RR | -u z e. A }
7 eqid 
 |-  ( w e. RR |-> -u w ) = ( w e. RR |-> -u w )
8 7 negiso 
 |-  ( ( w e. RR |-> -u w ) Isom < , `' < ( RR , RR ) /\ `' ( w e. RR |-> -u w ) = ( w e. RR |-> -u w ) )
9 8 simpri 
 |-  `' ( w e. RR |-> -u w ) = ( w e. RR |-> -u w )
10 9 imaeq1i 
 |-  ( `' ( w e. RR |-> -u w ) " A ) = ( ( w e. RR |-> -u w ) " A )
11 6 10 eqtr3i 
 |-  { z e. RR | -u z e. A } = ( ( w e. RR |-> -u w ) " A )
12 11 supeq1i 
 |-  sup ( { z e. RR | -u z e. A } , RR , < ) = sup ( ( ( w e. RR |-> -u w ) " A ) , RR , < )
13 8 simpli 
 |-  ( w e. RR |-> -u w ) Isom < , `' < ( RR , RR )
14 isocnv 
 |-  ( ( w e. RR |-> -u w ) Isom < , `' < ( RR , RR ) -> `' ( w e. RR |-> -u w ) Isom `' < , < ( RR , RR ) )
15 13 14 ax-mp 
 |-  `' ( w e. RR |-> -u w ) Isom `' < , < ( RR , RR )
16 isoeq1 
 |-  ( `' ( w e. RR |-> -u w ) = ( w e. RR |-> -u w ) -> ( `' ( w e. RR |-> -u w ) Isom `' < , < ( RR , RR ) <-> ( w e. RR |-> -u w ) Isom `' < , < ( RR , RR ) ) )
17 9 16 ax-mp 
 |-  ( `' ( w e. RR |-> -u w ) Isom `' < , < ( RR , RR ) <-> ( w e. RR |-> -u w ) Isom `' < , < ( RR , RR ) )
18 15 17 mpbi 
 |-  ( w e. RR |-> -u w ) Isom `' < , < ( RR , RR )
19 18 a1i 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> ( w e. RR |-> -u w ) Isom `' < , < ( RR , RR ) )
20 simp1 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> A C_ RR )
21 infm3 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> E. x e. RR ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) )
22 vex 
 |-  x e. _V
23 vex 
 |-  y e. _V
24 22 23 brcnv 
 |-  ( x `' < y <-> y < x )
25 24 notbii 
 |-  ( -. x `' < y <-> -. y < x )
26 25 ralbii 
 |-  ( A. y e. A -. x `' < y <-> A. y e. A -. y < x )
27 23 22 brcnv 
 |-  ( y `' < x <-> x < y )
28 vex 
 |-  z e. _V
29 23 28 brcnv 
 |-  ( y `' < z <-> z < y )
30 29 rexbii 
 |-  ( E. z e. A y `' < z <-> E. z e. A z < y )
31 27 30 imbi12i 
 |-  ( ( y `' < x -> E. z e. A y `' < z ) <-> ( x < y -> E. z e. A z < y ) )
32 31 ralbii 
 |-  ( A. y e. RR ( y `' < x -> E. z e. A y `' < z ) <-> A. y e. RR ( x < y -> E. z e. A z < y ) )
33 26 32 anbi12i 
 |-  ( ( A. y e. A -. x `' < y /\ A. y e. RR ( y `' < x -> E. z e. A y `' < z ) ) <-> ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) )
34 33 rexbii 
 |-  ( E. x e. RR ( A. y e. A -. x `' < y /\ A. y e. RR ( y `' < x -> E. z e. A y `' < z ) ) <-> E. x e. RR ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) )
35 21 34 sylibr 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> E. x e. RR ( A. y e. A -. x `' < y /\ A. y e. RR ( y `' < x -> E. z e. A y `' < z ) ) )
36 gtso 
 |-  `' < Or RR
37 36 a1i 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> `' < Or RR )
38 19 20 35 37 supiso 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> sup ( ( ( w e. RR |-> -u w ) " A ) , RR , < ) = ( ( w e. RR |-> -u w ) ` sup ( A , RR , `' < ) ) )
39 12 38 eqtrid 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> sup ( { z e. RR | -u z e. A } , RR , < ) = ( ( w e. RR |-> -u w ) ` sup ( A , RR , `' < ) ) )
40 df-inf 
 |-  inf ( A , RR , < ) = sup ( A , RR , `' < )
41 40 eqcomi 
 |-  sup ( A , RR , `' < ) = inf ( A , RR , < )
42 41 fveq2i 
 |-  ( ( w e. RR |-> -u w ) ` sup ( A , RR , `' < ) ) = ( ( w e. RR |-> -u w ) ` inf ( A , RR , < ) )
43 negeq 
 |-  ( w = inf ( A , RR , < ) -> -u w = -u inf ( A , RR , < ) )
44 negex 
 |-  -u inf ( A , RR , < ) e. _V
45 43 7 44 fvmpt 
 |-  ( inf ( A , RR , < ) e. RR -> ( ( w e. RR |-> -u w ) ` inf ( A , RR , < ) ) = -u inf ( A , RR , < ) )
46 42 45 eqtrid 
 |-  ( inf ( A , RR , < ) e. RR -> ( ( w e. RR |-> -u w ) ` sup ( A , RR , `' < ) ) = -u inf ( A , RR , < ) )
47 1 46 syl 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> ( ( w e. RR |-> -u w ) ` sup ( A , RR , `' < ) ) = -u inf ( A , RR , < ) )
48 39 47 eqtr2d 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> -u inf ( A , RR , < ) = sup ( { z e. RR | -u z e. A } , RR , < ) )
49 48 negeqd 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> -u -u inf ( A , RR , < ) = -u sup ( { z e. RR | -u z e. A } , RR , < ) )
50 3 49 eqtr3d 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> inf ( A , RR , < ) = -u sup ( { z e. RR | -u z e. A } , RR , < ) )