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 )