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