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	37	rexlimdva	⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑎 ∈ 𝐴 𝑛 = - 𝑎 → ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) ) )
39		simprr	⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) ) → - 𝑛 ∈ 𝐴 )
40		negeq	⊢ ( 𝑎 = - 𝑛 → - 𝑎 = - - 𝑛 )
41	40	eqeq2d	⊢ ( 𝑎 = - 𝑛 → ( 𝑛 = - 𝑎 ↔ 𝑛 = - - 𝑛 ) )
42	41	adantl	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) ) ∧ 𝑎 = - 𝑛 ) → ( 𝑛 = - 𝑎 ↔ 𝑛 = - - 𝑛 ) )
43		recn	⊢ ( 𝑛 ∈ ℝ → 𝑛 ∈ ℂ )
44		negneg	⊢ ( 𝑛 ∈ ℂ → - - 𝑛 = 𝑛 )
45	44	eqcomd	⊢ ( 𝑛 ∈ ℂ → 𝑛 = - - 𝑛 )
46	43 45	syl	⊢ ( 𝑛 ∈ ℝ → 𝑛 = - - 𝑛 )
47	46	ad2antrl	⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) ) → 𝑛 = - - 𝑛 )
48	39 42 47	rspcedvd	⊢ ( ( 𝐴 ⊆ ℝ ∧ ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) ) → ∃ 𝑎 ∈ 𝐴 𝑛 = - 𝑎 )
49	48	ex	⊢ ( 𝐴 ⊆ ℝ → ( ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) → ∃ 𝑎 ∈ 𝐴 𝑛 = - 𝑎 ) )
50	38 49	impbid	⊢ ( 𝐴 ⊆ ℝ → ( ∃ 𝑎 ∈ 𝐴 𝑛 = - 𝑎 ↔ ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) ) )
51	50	abbidv	⊢ ( 𝐴 ⊆ ℝ → { 𝑛 ∣ ∃ 𝑎 ∈ 𝐴 𝑛 = - 𝑎 } = { 𝑛 ∣ ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) } )
52	16	rnmpt	⊢ ran ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) = { 𝑛 ∣ ∃ 𝑎 ∈ 𝐴 𝑛 = - 𝑎 }
53		df-rab	⊢ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } = { 𝑛 ∣ ( 𝑛 ∈ ℝ ∧ - 𝑛 ∈ 𝐴 ) }
54	51 52 53	3eqtr4g	⊢ ( 𝐴 ⊆ ℝ → ran ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) = { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } )
55	54	eleq1d	⊢ ( 𝐴 ⊆ ℝ → ( ran ( 𝑎 ∈ 𝐴 ↦ - 𝑎 ) ∈ Fin ↔ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } ∈ Fin ) )
56	12 21 55	3bitrd	⊢ ( 𝐴 ⊆ ℝ → ( 𝐴 ∈ Fin ↔ { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } ∈ Fin ) )
57	56	biimpa	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ∈ Fin ) → { 𝑛 ∈ ℝ ∣ - 𝑛 ∈ 𝐴 } ∈ Fin )