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→ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } )