negfi

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

		Ref	Expression
	Assertion	negfi	$⊢ (A \subseteq ℝ \land A \in Fin) \to \{n \in ℝ \| - n \in A\} \in Fin$

Proof

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq ℝ \to (a \in A \to a \in ℝ)$
2		renegcl	$⊢ a \in ℝ \to - a \in ℝ$
3	1 2	syl6	$⊢ A \subseteq ℝ \to (a \in A \to - a \in ℝ)$
4	3	ralrimiv	$⊢ A \subseteq ℝ \to \forall a \in A - a \in ℝ$
5		dmmptg	$⊢ \forall a \in A - a \in ℝ \to dom (a \in A ⟼ - a) = A$
6	4 5	syl	$⊢ A \subseteq ℝ \to dom (a \in A ⟼ - a) = A$
7	6	eqcomd	$⊢ A \subseteq ℝ \to A = dom (a \in A ⟼ - a)$
8	7	eleq1d	$⊢ A \subseteq ℝ \to (A \in Fin \leftrightarrow dom (a \in A ⟼ - a) \in Fin)$
9		funmpt	$⊢ Fun (a \in A ⟼ - a)$
10		fundmfibi	$⊢ Fun (a \in A ⟼ - a) \to ((a \in A ⟼ - a) \in Fin \leftrightarrow dom (a \in A ⟼ - a) \in Fin)$
11	9 10	mp1i	$⊢ A \subseteq ℝ \to ((a \in A ⟼ - a) \in Fin \leftrightarrow dom (a \in A ⟼ - a) \in Fin)$
12	8 11	bitr4d	$⊢ A \subseteq ℝ \to (A \in Fin \leftrightarrow (a \in A ⟼ - a) \in Fin)$
13		reex	$⊢ ℝ \in V$
14	13	ssex	$⊢ A \subseteq ℝ \to A \in V$
15	14	mptexd	$⊢ A \subseteq ℝ \to (a \in A ⟼ - a) \in V$
16		eqid	$⊢ (a \in A ⟼ - a) = (a \in A ⟼ - a)$
17	16	negf1o	$⊢ A \subseteq ℝ \to (a \in A ⟼ - a) : A \underset{1-1 onto}{⟶} \{x \in ℝ \| - x \in A\}$
18		f1of1	$⊢ (a \in A ⟼ - a) : A \underset{1-1 onto}{⟶} \{x \in ℝ \| - x \in A\} \to (a \in A ⟼ - a) : A \underset{1-1}{⟶} \{x \in ℝ \| - x \in A\}$
19	17 18	syl	$⊢ A \subseteq ℝ \to (a \in A ⟼ - a) : A \underset{1-1}{⟶} \{x \in ℝ \| - x \in A\}$
20		f1vrnfibi	$⊢ ((a \in A ⟼ - a) \in V \land (a \in A ⟼ - a) : A \underset{1-1}{⟶} \{x \in ℝ \| - x \in A\}) \to ((a \in A ⟼ - a) \in Fin \leftrightarrow ran (a \in A ⟼ - a) \in Fin)$
21	15 19 20	syl2anc	$⊢ A \subseteq ℝ \to ((a \in A ⟼ - a) \in Fin \leftrightarrow ran (a \in A ⟼ - a) \in Fin)$
22	1	imp	$⊢ (A \subseteq ℝ \land a \in A) \to a \in ℝ$
23	2	adantl	$⊢ ((A \subseteq ℝ \land a \in A) \land a \in ℝ) \to - a \in ℝ$
24		recn	$⊢ a \in ℝ \to a \in ℂ$
25	24	negnegd	$⊢ a \in ℝ \to - (- a) = a$
26	25	eqcomd	$⊢ a \in ℝ \to a = - (- a)$
27	26	eleq1d	$⊢ a \in ℝ \to (a \in A \leftrightarrow - (- a) \in A)$
28	27	biimpcd	$⊢ a \in A \to (a \in ℝ \to - (- a) \in A)$
29	28	adantl	$⊢ (A \subseteq ℝ \land a \in A) \to (a \in ℝ \to - (- a) \in A)$
30	29	imp	$⊢ ((A \subseteq ℝ \land a \in A) \land a \in ℝ) \to - (- a) \in A$
31	23 30	jca	$⊢ ((A \subseteq ℝ \land a \in A) \land a \in ℝ) \to (- a \in ℝ \land - (- a) \in A)$
32	22 31	mpdan	$⊢ (A \subseteq ℝ \land a \in A) \to (- a \in ℝ \land - (- a) \in A)$
33		eleq1	$⊢ n = - a \to (n \in ℝ \leftrightarrow - a \in ℝ)$
34		negeq	$⊢ n = - a \to - n = - (- a)$
35	34	eleq1d	$⊢ n = - a \to (- n \in A \leftrightarrow - (- a) \in A)$
36	33 35	anbi12d	$⊢ n = - a \to ((n \in ℝ \land - n \in A) \leftrightarrow (- a \in ℝ \land - (- a) \in A))$
37	32 36	syl5ibrcom	$⊢ (A \subseteq ℝ \land a \in A) \to (n = - a \to (n \in ℝ \land - n \in A))$
38		simprr	$⊢ (A \subseteq ℝ \land (n \in ℝ \land - n \in A)) \to - n \in A$
39		recn	$⊢ n \in ℝ \to n \in ℂ$
40		negneg	$⊢ n \in ℂ \to - (- n) = n$
41	40	eqcomd	$⊢ n \in ℂ \to n = - (- n)$
42	39 41	syl	$⊢ n \in ℝ \to n = - (- n)$
43	42	ad2antrl	$⊢ (A \subseteq ℝ \land (n \in ℝ \land - n \in A)) \to n = - (- n)$
44		negeq	$⊢ a = - n \to - a = - (- n)$
45	44	eqeq2d	$⊢ a = - n \to (n = - a \leftrightarrow n = - (- n))$
46	37 38 43 45	rspceb2dv	$⊢ A \subseteq ℝ \to (\exists a \in A n = - a \leftrightarrow (n \in ℝ \land - n \in A))$
47	46	abbidv	$⊢ A \subseteq ℝ \to \{n \| \exists a \in A n = - a\} = \{n \| (n \in ℝ \land - n \in A)\}$
48	16	rnmpt	$⊢ ran (a \in A ⟼ - a) = \{n \| \exists a \in A n = - a\}$
49		df-rab	$⊢ \{n \in ℝ \| - n \in A\} = \{n \| (n \in ℝ \land - n \in A)\}$
50	47 48 49	3eqtr4g	$⊢ A \subseteq ℝ \to ran (a \in A ⟼ - a) = \{n \in ℝ \| - n \in A\}$
51	50	eleq1d	$⊢ A \subseteq ℝ \to (ran (a \in A ⟼ - a) \in Fin \leftrightarrow \{n \in ℝ \| - n \in A\} \in Fin)$
52	12 21 51	3bitrd	$⊢ A \subseteq ℝ \to (A \in Fin \leftrightarrow \{n \in ℝ \| - n \in A\} \in Fin)$
53	52	biimpa	$⊢ (A \subseteq ℝ \land A \in Fin) \to \{n \in ℝ \| - n \in A\} \in Fin$

Metamath Proof Explorer

Theorem negfi

Proof