Metamath Proof Explorer

Theorem negf1o

Description: Negation is an isomorphism of a subset of the real numbers to the negated elements of the subset. (Contributed by AV, 9-Aug-2020)

Ref Expression
Hypothesis negf1o.1 ⊢ F = x ∈ A ⟼ − x
Assertion negf1o ⊢ A ⊆ ℝ → F : A ⟶ 1-1 onto n ∈ ℝ | − n ∈ A

Proof

Step Hyp Ref Expression
1 negf1o.1 ⊢ F = x ∈ A ⟼ − x
2 negeq ⊢ n = − x → − n = − − x
3 2 eleq1d ⊢ n = − x → − n ∈ A ↔ − − x ∈ A
4 ssel ⊢ A ⊆ ℝ → x ∈ A → x ∈ ℝ
5 renegcl ⊢ x ∈ ℝ → − x ∈ ℝ
6 4 5 syl6 ⊢ A ⊆ ℝ → x ∈ A → − x ∈ ℝ
7 6 imp ⊢ A ⊆ ℝ ∧ x ∈ A → − x ∈ ℝ
8 4 imp ⊢ A ⊆ ℝ ∧ x ∈ A → x ∈ ℝ
9 recn ⊢ x ∈ ℝ → x ∈ ℂ
10 negneg ⊢ x ∈ ℂ → − − x = x
11 10 eqcomd ⊢ x ∈ ℂ → x = − − x
12 9 11 syl ⊢ x ∈ ℝ → x = − − x
13 12 eleq1d ⊢ x ∈ ℝ → x ∈ A ↔ − − x ∈ A
14 13 biimpcd ⊢ x ∈ A → x ∈ ℝ → − − x ∈ A
15 14 adantl ⊢ A ⊆ ℝ ∧ x ∈ A → x ∈ ℝ → − − x ∈ A
16 8 15 mpd ⊢ A ⊆ ℝ ∧ x ∈ A → − − x ∈ A
17 3 7 16 elrabd ⊢ A ⊆ ℝ ∧ x ∈ A → − x ∈ n ∈ ℝ | − n ∈ A
18 negeq ⊢ n = y → − n = − y
19 18 eleq1d ⊢ n = y → − n ∈ A ↔ − y ∈ A
20 19 elrab ⊢ y ∈ n ∈ ℝ | − n ∈ A ↔ y ∈ ℝ ∧ − y ∈ A
21 simpr ⊢ y ∈ ℝ ∧ − y ∈ A → − y ∈ A
22 21 a1i ⊢ A ⊆ ℝ → y ∈ ℝ ∧ − y ∈ A → − y ∈ A
23 20 22 syl5bi ⊢ A ⊆ ℝ → y ∈ n ∈ ℝ | − n ∈ A → − y ∈ A
24 23 imp ⊢ A ⊆ ℝ ∧ y ∈ n ∈ ℝ | − n ∈ A → − y ∈ A
25 4 9 syl6com ⊢ x ∈ A → A ⊆ ℝ → x ∈ ℂ
26 25 adantl ⊢ y ∈ ℝ ∧ − y ∈ A ∧ x ∈ A → A ⊆ ℝ → x ∈ ℂ
27 26 imp ⊢ y ∈ ℝ ∧ − y ∈ A ∧ x ∈ A ∧ A ⊆ ℝ → x ∈ ℂ
28 recn ⊢ y ∈ ℝ → y ∈ ℂ
29 28 ad3antrrr ⊢ y ∈ ℝ ∧ − y ∈ A ∧ x ∈ A ∧ A ⊆ ℝ → y ∈ ℂ
30 negcon2 ⊢ x ∈ ℂ ∧ y ∈ ℂ → x = − y ↔ y = − x
31 27 29 30 syl2anc ⊢ y ∈ ℝ ∧ − y ∈ A ∧ x ∈ A ∧ A ⊆ ℝ → x = − y ↔ y = − x
32 31 exp31 ⊢ y ∈ ℝ ∧ − y ∈ A → x ∈ A → A ⊆ ℝ → x = − y ↔ y = − x
33 20 32 sylbi ⊢ y ∈ n ∈ ℝ | − n ∈ A → x ∈ A → A ⊆ ℝ → x = − y ↔ y = − x
34 33 impcom ⊢ x ∈ A ∧ y ∈ n ∈ ℝ | − n ∈ A → A ⊆ ℝ → x = − y ↔ y = − x
35 34 impcom ⊢ A ⊆ ℝ ∧ x ∈ A ∧ y ∈ n ∈ ℝ | − n ∈ A → x = − y ↔ y = − x
36 1 17 24 35 f1o2d ⊢ A ⊆ ℝ → F : A ⟶ 1-1 onto n ∈ ℝ | − n ∈ A