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 𝐹 = ( 𝑥 ∈ ℝ ↦ - 𝑥 )
Assertion negiso ( 𝐹 Isom < , < ( ℝ , ℝ ) ∧ 𝐹 = 𝐹 )

Proof

Step Hyp Ref Expression
1 negiso.1 𝐹 = ( 𝑥 ∈ ℝ ↦ - 𝑥 )
2 simpr ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
3 2 renegcld ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → - 𝑥 ∈ ℝ )
4 simpr ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
5 4 renegcld ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → - 𝑦 ∈ ℝ )
6 recn ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
7 recn ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
8 negcon2 ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 = - 𝑦𝑦 = - 𝑥 ) )
9 6 7 8 syl2an ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 = - 𝑦𝑦 = - 𝑥 ) )
10 9 adantl ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 = - 𝑦𝑦 = - 𝑥 ) )
11 1 3 5 10 f1ocnv2d ( ⊤ → ( 𝐹 : ℝ –1-1-onto→ ℝ ∧ 𝐹 = ( 𝑦 ∈ ℝ ↦ - 𝑦 ) ) )
12 11 mptru ( 𝐹 : ℝ –1-1-onto→ ℝ ∧ 𝐹 = ( 𝑦 ∈ ℝ ↦ - 𝑦 ) )
13 12 simpli 𝐹 : ℝ –1-1-onto→ ℝ
14 ltneg ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 < 𝑦 ↔ - 𝑦 < - 𝑧 ) )
15 negex - 𝑧 ∈ V
16 negex - 𝑦 ∈ V
17 15 16 brcnv ( - 𝑧 < - 𝑦 ↔ - 𝑦 < - 𝑧 )
18 14 17 bitr4di ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 < 𝑦 ↔ - 𝑧 < - 𝑦 ) )
19 negeq ( 𝑥 = 𝑧 → - 𝑥 = - 𝑧 )
20 19 1 15 fvmpt ( 𝑧 ∈ ℝ → ( 𝐹𝑧 ) = - 𝑧 )
21 negeq ( 𝑥 = 𝑦 → - 𝑥 = - 𝑦 )
22 21 1 16 fvmpt ( 𝑦 ∈ ℝ → ( 𝐹𝑦 ) = - 𝑦 )
23 20 22 breqan12d ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝐹𝑧 ) < ( 𝐹𝑦 ) ↔ - 𝑧 < - 𝑦 ) )
24 18 23 bitr4d ( ( 𝑧 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑧 < 𝑦 ↔ ( 𝐹𝑧 ) < ( 𝐹𝑦 ) ) )
25 24 rgen2 𝑧 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑧 < 𝑦 ↔ ( 𝐹𝑧 ) < ( 𝐹𝑦 ) )
26 df-isom ( 𝐹 Isom < , < ( ℝ , ℝ ) ↔ ( 𝐹 : ℝ –1-1-onto→ ℝ ∧ ∀ 𝑧 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑧 < 𝑦 ↔ ( 𝐹𝑧 ) < ( 𝐹𝑦 ) ) ) )
27 13 25 26 mpbir2an 𝐹 Isom < , < ( ℝ , ℝ )
28 negeq ( 𝑦 = 𝑥 → - 𝑦 = - 𝑥 )
29 28 cbvmptv ( 𝑦 ∈ ℝ ↦ - 𝑦 ) = ( 𝑥 ∈ ℝ ↦ - 𝑥 )
30 12 simpri 𝐹 = ( 𝑦 ∈ ℝ ↦ - 𝑦 )
31 29 30 1 3eqtr4i 𝐹 = 𝐹
32 27 31 pm3.2i ( 𝐹 Isom < , < ( ℝ , ℝ ) ∧ 𝐹 = 𝐹 )