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

Metamath Proof Explorer

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 )