Step | Hyp | Ref
| Expression |
1 | | negf1o.1 |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥) |
2 | | ssel 3134 |
. . . . . 6
⊢ (𝐴 ⊆ ℝ → (𝑥 ∈ 𝐴 → 𝑥 ∈ ℝ)) |
3 | | renegcl 8153 |
. . . . . 6
⊢ (𝑥 ∈ ℝ → -𝑥 ∈
ℝ) |
4 | 2, 3 | syl6 33 |
. . . . 5
⊢ (𝐴 ⊆ ℝ → (𝑥 ∈ 𝐴 → -𝑥 ∈ ℝ)) |
5 | 4 | imp 123 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴) → -𝑥 ∈ ℝ) |
6 | 2 | imp 123 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
7 | | recn 7880 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
8 | | negneg 8142 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℂ → --𝑥 = 𝑥) |
9 | 8 | eqcomd 2170 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → 𝑥 = --𝑥) |
10 | 7, 9 | syl 14 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ → 𝑥 = --𝑥) |
11 | 10 | eleq1d 2233 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ → (𝑥 ∈ 𝐴 ↔ --𝑥 ∈ 𝐴)) |
12 | 11 | biimpcd 158 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ ℝ → --𝑥 ∈ 𝐴)) |
13 | 12 | adantl 275 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ ℝ → --𝑥 ∈ 𝐴)) |
14 | 6, 13 | mpd 13 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴) → --𝑥 ∈ 𝐴) |
15 | | negeq 8085 |
. . . . . 6
⊢ (𝑛 = -𝑥 → -𝑛 = --𝑥) |
16 | 15 | eleq1d 2233 |
. . . . 5
⊢ (𝑛 = -𝑥 → (-𝑛 ∈ 𝐴 ↔ --𝑥 ∈ 𝐴)) |
17 | 16 | elrab 2880 |
. . . 4
⊢ (-𝑥 ∈ {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴} ↔ (-𝑥 ∈ ℝ ∧ --𝑥 ∈ 𝐴)) |
18 | 5, 14, 17 | sylanbrc 414 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴) → -𝑥 ∈ {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴}) |
19 | | negeq 8085 |
. . . . . . 7
⊢ (𝑛 = 𝑦 → -𝑛 = -𝑦) |
20 | 19 | eleq1d 2233 |
. . . . . 6
⊢ (𝑛 = 𝑦 → (-𝑛 ∈ 𝐴 ↔ -𝑦 ∈ 𝐴)) |
21 | 20 | elrab 2880 |
. . . . 5
⊢ (𝑦 ∈ {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴} ↔ (𝑦 ∈ ℝ ∧ -𝑦 ∈ 𝐴)) |
22 | | simpr 109 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ ∧ -𝑦 ∈ 𝐴) → -𝑦 ∈ 𝐴) |
23 | 22 | a1i 9 |
. . . . 5
⊢ (𝐴 ⊆ ℝ → ((𝑦 ∈ ℝ ∧ -𝑦 ∈ 𝐴) → -𝑦 ∈ 𝐴)) |
24 | 21, 23 | syl5bi 151 |
. . . 4
⊢ (𝐴 ⊆ ℝ → (𝑦 ∈ {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴} → -𝑦 ∈ 𝐴)) |
25 | 24 | imp 123 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝑦 ∈ {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴}) → -𝑦 ∈ 𝐴) |
26 | 2, 7 | syl6com 35 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → (𝐴 ⊆ ℝ → 𝑥 ∈ ℂ)) |
27 | 26 | adantl 275 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℝ ∧ -𝑦 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) → (𝐴 ⊆ ℝ → 𝑥 ∈ ℂ)) |
28 | 27 | imp 123 |
. . . . . . . 8
⊢ ((((𝑦 ∈ ℝ ∧ -𝑦 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝐴 ⊆ ℝ) → 𝑥 ∈ ℂ) |
29 | | recn 7880 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
30 | 29 | ad3antrrr 484 |
. . . . . . . 8
⊢ ((((𝑦 ∈ ℝ ∧ -𝑦 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝐴 ⊆ ℝ) → 𝑦 ∈ ℂ) |
31 | | negcon2 8145 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 = -𝑦 ↔ 𝑦 = -𝑥)) |
32 | 28, 30, 31 | syl2anc 409 |
. . . . . . 7
⊢ ((((𝑦 ∈ ℝ ∧ -𝑦 ∈ 𝐴) ∧ 𝑥 ∈ 𝐴) ∧ 𝐴 ⊆ ℝ) → (𝑥 = -𝑦 ↔ 𝑦 = -𝑥)) |
33 | 32 | exp31 362 |
. . . . . 6
⊢ ((𝑦 ∈ ℝ ∧ -𝑦 ∈ 𝐴) → (𝑥 ∈ 𝐴 → (𝐴 ⊆ ℝ → (𝑥 = -𝑦 ↔ 𝑦 = -𝑥)))) |
34 | 21, 33 | sylbi 120 |
. . . . 5
⊢ (𝑦 ∈ {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴} → (𝑥 ∈ 𝐴 → (𝐴 ⊆ ℝ → (𝑥 = -𝑦 ↔ 𝑦 = -𝑥)))) |
35 | 34 | impcom 124 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴}) → (𝐴 ⊆ ℝ → (𝑥 = -𝑦 ↔ 𝑦 = -𝑥))) |
36 | 35 | impcom 124 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴})) → (𝑥 = -𝑦 ↔ 𝑦 = -𝑥)) |
37 | 1, 18, 25, 36 | f1ocnv2d 6039 |
. 2
⊢ (𝐴 ⊆ ℝ → (𝐹:𝐴–1-1-onto→{𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴} ∧ ◡𝐹 = (𝑦 ∈ {𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴} ↦ -𝑦))) |
38 | 37 | simpld 111 |
1
⊢ (𝐴 ⊆ ℝ → 𝐹:𝐴–1-1-onto→{𝑛 ∈ ℝ ∣ -𝑛 ∈ 𝐴}) |