Metamath Proof Explorer

Theorem negiso

Description: Negation is an order anti-isomorphism of the real numbers, which is its own inverse. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis negiso.1 
|- F = ( x e. RR |-> -u x )
Assertion negiso 
|- ( F Isom < , `' < ( RR , RR ) /\ `' F = F )

Proof

Step Hyp Ref Expression
1 negiso.1 
 |-  F = ( x e. RR |-> -u x )
2 simpr 
 |-  ( ( T. /\ x e. RR ) -> x e. RR )
3 2 renegcld 
 |-  ( ( T. /\ x e. RR ) -> -u x e. RR )
4 simpr 
 |-  ( ( T. /\ y e. RR ) -> y e. RR )
5 4 renegcld 
 |-  ( ( T. /\ y e. RR ) -> -u y e. RR )
6 recn 
 |-  ( x e. RR -> x e. CC )
7 recn 
 |-  ( y e. RR -> y e. CC )
8 negcon2 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x = -u y <-> y = -u x ) )
9 6 7 8 syl2an 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x = -u y <-> y = -u x ) )
10 9 adantl 
 |-  ( ( T. /\ ( x e. RR /\ y e. RR ) ) -> ( x = -u y <-> y = -u x ) )
11 1 3 5 10 f1ocnv2d 
 |-  ( T. -> ( F : RR -1-1-onto-> RR /\ `' F = ( y e. RR |-> -u y ) ) )
12 11 mptru 
 |-  ( F : RR -1-1-onto-> RR /\ `' F = ( y e. RR |-> -u y ) )
13 12 simpli 
 |-  F : RR -1-1-onto-> RR
14 ltneg 
 |-  ( ( z e. RR /\ y e. RR ) -> ( z < y <-> -u y < -u z ) )
15 negex 
 |-  -u z e. _V
16 negex 
 |-  -u y e. _V
17 15 16 brcnv 
 |-  ( -u z `' < -u y <-> -u y < -u z )
18 14 17 bitr4di 
 |-  ( ( z e. RR /\ y e. RR ) -> ( z < y <-> -u z `' < -u y ) )
19 negeq 
 |-  ( x = z -> -u x = -u z )
20 19 1 15 fvmpt 
 |-  ( z e. RR -> ( F ` z ) = -u z )
21 negeq 
 |-  ( x = y -> -u x = -u y )
22 21 1 16 fvmpt 
 |-  ( y e. RR -> ( F ` y ) = -u y )
23 20 22 breqan12d 
 |-  ( ( z e. RR /\ y e. RR ) -> ( ( F ` z ) `' < ( F ` y ) <-> -u z `' < -u y ) )
24 18 23 bitr4d 
 |-  ( ( z e. RR /\ y e. RR ) -> ( z < y <-> ( F ` z ) `' < ( F ` y ) ) )
25 24 rgen2 
 |-  A. z e. RR A. y e. RR ( z < y <-> ( F ` z ) `' < ( F ` y ) )
26 df-isom 
 |-  ( F Isom < , `' < ( RR , RR ) <-> ( F : RR -1-1-onto-> RR /\ A. z e. RR A. y e. RR ( z < y <-> ( F ` z ) `' < ( F ` y ) ) ) )
27 13 25 26 mpbir2an 
 |-  F Isom < , `' < ( RR , RR )
28 negeq 
 |-  ( y = x -> -u y = -u x )
29 28 cbvmptv 
 |-  ( y e. RR |-> -u y ) = ( x e. RR |-> -u x )
30 12 simpri 
 |-  `' F = ( y e. RR |-> -u y )
31 29 30 1 3eqtr4i 
 |-  `' F = F
32 27 31 pm3.2i 
 |-  ( F Isom < , `' < ( RR , RR ) /\ `' F = F )