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 ⊢FIsom<,<-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<-1F⁡y↔−z<-1−y
24 18 23 bitr4d ⊢z∈ℝ∧y∈ℝ→z<y↔F⁡z<-1F⁡y
25 24 rgen2 ⊢∀z∈ℝ∀y∈ℝz<y↔F⁡z<-1F⁡y
26 df-isom ⊢FIsom<,<-1ℝℝ↔F:ℝ⟶1-1 ontoℝ∧∀z∈ℝ∀y∈ℝz<y↔F⁡z<-1F⁡y
27 13 25 26 mpbir2an ⊢FIsom<,<-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 ⊢FIsom<,<-1ℝℝ∧F-1=F