This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ - 𝑥 )
Assertion negf1o ( 𝐴 ⊆ ℝ → 𝐹 : 𝐴 –1-1-onto→ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } )

Proof

Step Hyp Ref Expression
1 negf1o.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ - 𝑥 )
2 negeq ⊢ ( 𝑛 = - 𝑥 → - 𝑛 = - - 𝑥 )
3 2 eleq1d ⊢ ( 𝑛 = - 𝑥 → ( - 𝑛 ∈ 𝐴 ↔ - - 𝑥 ∈ 𝐴 ) )
4 ssel ⊢ ( 𝐴 ⊆ ℝ → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ℝ ) )
5 renegcl ⊢ ( 𝑥 ∈ ℝ → - 𝑥 ∈ ℝ )
6 4 5 syl6 ⊢ ( 𝐴 ⊆ ℝ → ( 𝑥 ∈ 𝐴 → - 𝑥 ∈ ℝ ) )
7 6 imp ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → - 𝑥 ∈ ℝ )
8 4 imp ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
9 recn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
10 negneg ⊢ ( 𝑥 ∈ ℂ → - - 𝑥 = 𝑥 )
11 10 eqcomd ⊢ ( 𝑥 ∈ ℂ → 𝑥 = - - 𝑥 )
12 9 11 syl ⊢ ( 𝑥 ∈ ℝ → 𝑥 = - - 𝑥 )
13 12 eleq1d ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ 𝐴 ↔ - - 𝑥 ∈ 𝐴 ) )
14 13 biimpcd ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ℝ → - - 𝑥 ∈ 𝐴 ) )
15 14 adantl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ℝ → - - 𝑥 ∈ 𝐴 ) )
16 8 15 mpd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → - - 𝑥 ∈ 𝐴 )
17 3 7 16 elrabd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → - 𝑥 ∈ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } )
18 negeq ⊢ ( 𝑛 = 𝑦 → - 𝑛 = - 𝑦 )
19 18 eleq1d ⊢ ( 𝑛 = 𝑦 → ( - 𝑛 ∈ 𝐴 ↔ - 𝑦 ∈ 𝐴 ) )
20 19 elrab ⊢ ( 𝑦 ∈ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } ↔ ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ 𝐴 ) )
21 simpr ⊢ ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ 𝐴 ) → - 𝑦 ∈ 𝐴 )
22 21 a1i ⊢ ( 𝐴 ⊆ ℝ → ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ 𝐴 ) → - 𝑦 ∈ 𝐴 ) )
23 20 22 biimtrid ⊢ ( 𝐴 ⊆ ℝ → ( 𝑦 ∈ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } → - 𝑦 ∈ 𝐴 ) )
24 23 imp ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } ) → - 𝑦 ∈ 𝐴 )
25 4 9 syl6com ⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 ⊆ ℝ → 𝑥 ∈ ℂ ) )
26 25 adantl ⊢ ( ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ⊆ ℝ → 𝑥 ∈ ℂ ) )
27 26 imp ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐴 ⊆ ℝ ) → 𝑥 ∈ ℂ )
28 recn ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
29 28 ad3antrrr ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐴 ⊆ ℝ ) → 𝑦 ∈ ℂ )
30 negcon2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) )
31 27 29 30 syl2anc ⊢ ( ( ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝐴 ⊆ ℝ ) → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) )
32 31 exp31 ⊢ ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 → ( 𝐴 ⊆ ℝ → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) ) ) )
33 20 32 sylbi ⊢ ( 𝑦 ∈ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } → ( 𝑥 ∈ 𝐴 → ( 𝐴 ⊆ ℝ → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) ) ) )
34 33 impcom ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } ) → ( 𝐴 ⊆ ℝ → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) ) )
35 34 impcom ⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } ) ) → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) )
36 1 17 24 35 f1o2d ⊢ ( 𝐴 ⊆ ℝ → 𝐹 : 𝐴 –1-1-onto→ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } )