Theorem negfi

Description: The negation of a finite set of real numbers is finite. (Contributed by AV, 9-Aug-2020)

	Ref	Expression
Assertion	negfi	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ) → { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		ssel	⊢ ( 𝐴 ⊆ ℝ → ( 𝑎 ∈ 𝐴 → 𝑎 ∈ ℝ ) )
2		renegcl	⊢ ( 𝑎 ∈ ℝ → - 𝑎 ∈ ℝ )
3	1 2	syl6	⊢ ( 𝐴 ⊆ ℝ → ( 𝑎 ∈ 𝐴 → - 𝑎 ∈ ℝ ) )
4	3	ralrimiv	⊢ ( 𝐴 ⊆ ℝ → ∀ 𝑎 ∈ 𝐴 - 𝑎 ∈ ℝ )
5		dmmptg	⊢ ( ∀ 𝑎 ∈ 𝐴 - 𝑎 ∈ ℝ → dom ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) = 𝐴 )
6	4 5	syl	⊢ ( 𝐴 ⊆ ℝ → dom ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) = 𝐴 )
7	6	eqcomd	⊢ ( 𝐴 ⊆ ℝ → 𝐴 = dom ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) )
8	7	eleq1d	⊢ ( 𝐴 ⊆ ℝ → ( 𝐴 ∈ Fin ↔ dom ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) ∈ Fin ) )
9		funmpt	⊢ Fun ( 𝑎 ∈ 𝐴 ↦ - 𝑎 )
10		fundmfibi	⊢ ( Fun ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) → ( ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) ∈ Fin ↔ dom ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) ∈ Fin ) )
11	9 10	mp1i	⊢ ( 𝐴 ⊆ ℝ → ( ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) ∈ Fin ↔ dom ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) ∈ Fin ) )
12	8 11	bitr4d	⊢ ( 𝐴 ⊆ ℝ → ( 𝐴 ∈ Fin ↔ ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) ∈ Fin ) )
13		reex	⊢ ℝ ∈ V
14	13	ssex	⊢ ( 𝐴 ⊆ ℝ → 𝐴 ∈ V )
15	14	mptexd	⊢ ( 𝐴 ⊆ ℝ → ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) ∈ V )
16		eqid	⊢ ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) = ( 𝑎 ∈ 𝐴 ↦ - 𝑎 )
17	16	negf1o	⊢ ( 𝐴 ⊆ ℝ → ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) : 𝐴 –1-1-onto→ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } )
18		f1of1	⊢ ( ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) : 𝐴 –1-1-onto→ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } → ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) : 𝐴 –1-1→ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } )
19	17 18	syl	⊢ ( 𝐴 ⊆ ℝ → ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) : 𝐴 –1-1→ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } )
20		f1vrnfibi	⊢ ( ( ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) ∈ V ∧ ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) : 𝐴 –1-1→ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ) → ( ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) ∈ Fin ↔ ran ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) ∈ Fin ) )
21	15 19 20	syl2anc	⊢ ( 𝐴 ⊆ ℝ → ( ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) ∈ Fin ↔ ran ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) ∈ Fin ) )
22	1	imp	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ ℝ )
23	2	adantl	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑎 ∈ ℝ ) → - 𝑎 ∈ ℝ )
24		recn	⊢ ( 𝑎 ∈ ℝ → 𝑎 ∈ ℂ )
25	24	negnegd	⊢ ( 𝑎 ∈ ℝ → - - 𝑎 = 𝑎 )
26	25	eqcomd	⊢ ( 𝑎 ∈ ℝ → 𝑎 = - - 𝑎 )
27	26	eleq1d	⊢ ( 𝑎 ∈ ℝ → ( 𝑎 ∈ 𝐴 ↔ - - 𝑎 ∈ 𝐴 ) )
28	27	biimpcd	⊢ ( 𝑎 ∈ 𝐴 → ( 𝑎 ∈ ℝ → - - 𝑎 ∈ 𝐴 ) )
29	28	adantl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 ∈ ℝ → - - 𝑎 ∈ 𝐴 ) )
30	29	imp	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑎 ∈ ℝ ) → - - 𝑎 ∈ 𝐴 )
31	23 30	jca	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑎 ∈ ℝ ) → ( - 𝑎 ∈ ℝ ∧ - - 𝑎 ∈ 𝐴 ) )
32	22 31	mpdan	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑎 ∈ 𝐴 ) → ( - 𝑎 ∈ ℝ ∧ - - 𝑎 ∈ 𝐴 ) )
33		eleq1	⊢ ( 𝑛 = - 𝑎 → ( 𝑛 ∈ ℝ ↔ - 𝑎 ∈ ℝ ) )
34		negeq	⊢ ( 𝑛 = - 𝑎 → - 𝑛 = - - 𝑎 )
35	34	eleq1d	⊢ ( 𝑛 = - 𝑎 → ( - 𝑛 ∈ 𝐴 ↔ - - 𝑎 ∈ 𝐴 ) )
36	33 35	anbi12d	⊢ ( 𝑛 = - 𝑎 → ( ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) ↔ ( - 𝑎 ∈ ℝ ∧ - - 𝑎 ∈ 𝐴 ) ) )
37	32 36	syl5ibrcom	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑎 ∈ 𝐴 ) → ( 𝑛 = - 𝑎 → ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) ) )
38		simprr	⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) ) → - 𝑛 ∈ 𝐴 )
39		recn	⊢ ( 𝑛 ∈ ℝ → 𝑛 ∈ ℂ )
40		negneg	⊢ ( 𝑛 ∈ ℂ → - - 𝑛 = 𝑛 )
41	40	eqcomd	⊢ ( 𝑛 ∈ ℂ → 𝑛 = - - 𝑛 )
42	39 41	syl	⊢ ( 𝑛 ∈ ℝ → 𝑛 = - - 𝑛 )
43	42	ad2antrl	⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) ) → 𝑛 = - - 𝑛 )
44		negeq	⊢ ( 𝑎 = - 𝑛 → - 𝑎 = - - 𝑛 )
45	44	eqeq2d	⊢ ( 𝑎 = - 𝑛 → ( 𝑛 = - 𝑎 ↔ 𝑛 = - - 𝑛 ) )
46	37 38 43 45	rspceb2dv	⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑎 ∈ 𝐴 𝑛 = - 𝑎 ↔ ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) ) )
47	46	abbidv	⊢ ( 𝐴 ⊆ ℝ → { 𝑛 ∣ ∃ 𝑎 ∈ 𝐴 𝑛 = - 𝑎 } = { 𝑛 ∣ ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) } )
48	16	rnmpt	⊢ ran ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) = { 𝑛 ∣ ∃ 𝑎 ∈ 𝐴 𝑛 = - 𝑎 }
49		df-rab	⊢ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } = { 𝑛 ∣ ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) }
50	47 48 49	3eqtr4g	⊢ ( 𝐴 ⊆ ℝ → ran ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) = { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } )
51	50	eleq1d	⊢ ( 𝐴 ⊆ ℝ → ( ran ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) ∈ Fin ↔ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } ∈ Fin ) )
52	12 21 51	3bitrd	⊢ ( 𝐴 ⊆ ℝ → ( 𝐴 ∈ Fin ↔ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } ∈ Fin ) )
53	52	biimpa	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ) → { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } ∈ Fin )