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 < , ◡ < ( ℝ , ℝ ) ∧ ◡ 𝐹 = 𝐹 ) |