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 x
Assertion negiso F Isom < , < -1 F -1 = F

Proof

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