Theorem negfi 10110

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

Assertion

Ref	Expression
negfi	|- ( ( A C_ RR /\ A e. Fin ) -> { n e. RR | -u n e. A } e. Fin )

Distinct variable group:   A, n

Proof of Theorem negfi

Dummy variables a x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 2993	. . . . . . . . . 10 |- ( A C_ RR -> ( a e. A -> a e. RR ) )
2		renegcl 7369	. . . . . . . . . 10 |- ( a e. RR -> -u a e. RR )
3	1, 2	syl6 33	. . . . . . . . 9 |- ( A C_ RR -> ( a e. A -> -u a e. RR ) )
4	3	imp 122	. . . . . . . 8 |- ( ( A C_ RR /\ a e. A ) -> -u a e. RR )
5	4	ralrimiva 2434	. . . . . . 7 |- ( A C_ RR -> A. a e. A -u a e. RR )
6		dmmptg 4838	. . . . . . 7 |- ( A. a e. A -u a e. RR -> dom ( a e. A |-> -u a ) = A )
7	5, 6	syl 14	. . . . . 6 |- ( A C_ RR -> dom ( a e. A |-> -u a ) = A )
8	7	eqcomd 2086	. . . . 5 |- ( A C_ RR -> A = dom ( a e. A |-> -u a ) )
9	8	eleq1d 2147	. . . 4 |- ( A C_ RR -> ( A e. Fin <-> dom ( a e. A |-> -u a ) e. Fin ) )
10		funmpt 4958	. . . . 5 |- Fun ( a e. A |-> -u a )
11		fundmfibi 6390	. . . . 5 |- ( Fun ( a e. A |-> -u a ) -> ( ( a e. A |-> -u a ) e. Fin <-> dom ( a e. A |-> -u a ) e. Fin ) )
12	10, 11	mp1i 10	. . . 4 |- ( A C_ RR -> ( ( a e. A |-> -u a ) e. Fin <-> dom ( a e. A |-> -u a ) e. Fin ) )
13	9, 12	bitr4d 189	. . 3 |- ( A C_ RR -> ( A e. Fin <-> ( a e. A |-> -u a ) e. Fin ) )
14		reex 7107	. . . . . 6 |- RR e. _V
15	14	ssex 3915	. . . . 5 |- ( A C_ RR -> A e. _V )
16		mptexg 5407	. . . . 5 |- ( A e. _V -> ( a e. A |-> -u a ) e. _V )
17	15, 16	syl 14	. . . 4 |- ( A C_ RR -> ( a e. A |-> -u a ) e. _V )
18		eqid 2081	. . . . . 6 |- ( a e. A |-> -u a ) = ( a e. A |-> -u a )
19	18	negf1o 7486	. . . . 5 |- ( A C_ RR -> ( a e. A |-> -u a ) : A -1-1-onto-> { x e. RR | -u x e. A } )
20		f1of1 5145	. . . . 5 |- ( ( a e. A |-> -u a ) : A -1-1-onto-> { x e. RR | -u x e. A } -> ( a e. A |-> -u a ) : A -1-1-> { x e. RR | -u x e. A } )
21	19, 20	syl 14	. . . 4 |- ( A C_ RR -> ( a e. A |-> -u a ) : A -1-1-> { x e. RR | -u x e. A } )
22		f1vrnfibi 6394	. . . 4 |- ( ( ( a e. A |-> -u a ) e. _V /\ ( a e. A |-> -u a ) : A -1-1-> { x e. RR | -u x e. A } ) -> ( ( a e. A |-> -u a ) e. Fin <-> ran ( a e. A |-> -u a ) e. Fin ) )
23	17, 21, 22	syl2anc 403	. . 3 |- ( A C_ RR -> ( ( a e. A |-> -u a ) e. Fin <-> ran ( a e. A |-> -u a ) e. Fin ) )
24	1	imp 122	. . . . . . . . . 10 |- ( ( A C_ RR /\ a e. A ) -> a e. RR )
25	2	adantl 271	. . . . . . . . . . 11 |- ( ( ( A C_ RR /\ a e. A ) /\ a e. RR ) -> -u a e. RR )
26		recn 7106	. . . . . . . . . . . . . . . . 17 |- ( a e. RR -> a e. CC )
27	26	negnegd 7410	. . . . . . . . . . . . . . . 16 |- ( a e. RR -> -u -u a = a )
28	27	eqcomd 2086	. . . . . . . . . . . . . . 15 |- ( a e. RR -> a = -u -u a )
29	28	eleq1d 2147	. . . . . . . . . . . . . 14 |- ( a e. RR -> ( a e. A <-> -u -u a e. A ) )
30	29	biimpcd 157	. . . . . . . . . . . . 13 |- ( a e. A -> ( a e. RR -> -u -u a e. A ) )
31	30	adantl 271	. . . . . . . . . . . 12 |- ( ( A C_ RR /\ a e. A ) -> ( a e. RR -> -u -u a e. A ) )
32	31	imp 122	. . . . . . . . . . 11 |- ( ( ( A C_ RR /\ a e. A ) /\ a e. RR ) -> -u -u a e. A )
33	25, 32	jca 300	. . . . . . . . . 10 |- ( ( ( A C_ RR /\ a e. A ) /\ a e. RR ) -> ( -u a e. RR /\ -u -u a e. A ) )
34	24, 33	mpdan 412	. . . . . . . . 9 |- ( ( A C_ RR /\ a e. A ) -> ( -u a e. RR /\ -u -u a e. A ) )
35		eleq1 2141	. . . . . . . . . 10 |- ( n = -u a -> ( n e. RR <-> -u a e. RR ) )
36		negeq 7301	. . . . . . . . . . 11 |- ( n = -u a -> -u n = -u -u a )
37	36	eleq1d 2147	. . . . . . . . . 10 |- ( n = -u a -> ( -u n e. A <-> -u -u a e. A ) )
38	35, 37	anbi12d 456	. . . . . . . . 9 |- ( n = -u a -> ( ( n e. RR /\ -u n e. A ) <-> ( -u a e. RR /\ -u -u a e. A ) ) )
39	34, 38	syl5ibrcom 155	. . . . . . . 8 |- ( ( A C_ RR /\ a e. A ) -> ( n = -u a -> ( n e. RR /\ -u n e. A ) ) )
40	39	rexlimdva 2477	. . . . . . 7 |- ( A C_ RR -> ( E. a e. A n = -u a -> ( n e. RR /\ -u n e. A ) ) )
41		simprr 498	. . . . . . . . 9 |- ( ( A C_ RR /\ ( n e. RR /\ -u n e. A ) ) -> -u n e. A )
42		negeq 7301	. . . . . . . . . . 11 |- ( a = -u n -> -u a = -u -u n )
43	42	eqeq2d 2092	. . . . . . . . . 10 |- ( a = -u n -> ( n = -u a <-> n = -u -u n ) )
44	43	adantl 271	. . . . . . . . 9 |- ( ( ( A C_ RR /\ ( n e. RR /\ -u n e. A ) ) /\ a = -u n ) -> ( n = -u a <-> n = -u -u n ) )
45		recn 7106	. . . . . . . . . . 11 |- ( n e. RR -> n e. CC )
46		negneg 7358	. . . . . . . . . . . 12 |- ( n e. CC -> -u -u n = n )
47	46	eqcomd 2086	. . . . . . . . . . 11 |- ( n e. CC -> n = -u -u n )
48	45, 47	syl 14	. . . . . . . . . 10 |- ( n e. RR -> n = -u -u n )
49	48	ad2antrl 473	. . . . . . . . 9 |- ( ( A C_ RR /\ ( n e. RR /\ -u n e. A ) ) -> n = -u -u n )
50	41, 44, 49	rspcedvd 2708	. . . . . . . 8 |- ( ( A C_ RR /\ ( n e. RR /\ -u n e. A ) ) -> E. a e. A n = -u a )
51	50	ex 113	. . . . . . 7 |- ( A C_ RR -> ( ( n e. RR /\ -u n e. A ) -> E. a e. A n = -u a ) )
52	40, 51	impbid 127	. . . . . 6 |- ( A C_ RR -> ( E. a e. A n = -u a <-> ( n e. RR /\ -u n e. A ) ) )
53	52	abbidv 2196	. . . . 5 |- ( A C_ RR -> { n | E. a e. A n = -u a } = { n | ( n e. RR /\ -u n e. A ) } )
54	18	rnmpt 4600	. . . . 5 |- ran ( a e. A |-> -u a ) = { n | E. a e. A n = -u a }
55		df-rab 2357	. . . . 5 |- { n e. RR | -u n e. A } = { n | ( n e. RR /\ -u n e. A ) }
56	53, 54, 55	3eqtr4g 2138	. . . 4 |- ( A C_ RR -> ran ( a e. A |-> -u a ) = { n e. RR | -u n e. A } )
57	56	eleq1d 2147	. . 3 |- ( A C_ RR -> ( ran ( a e. A |-> -u a ) e. Fin <-> { n e. RR | -u n e. A } e. Fin ) )
58	13, 23, 57	3bitrd 212	. 2 |- ( A C_ RR -> ( A e. Fin <-> { n e. RR | -u n e. A } e. Fin ) )
59	58	biimpa 290	1 |- ( ( A C_ RR /\ A e. Fin ) -> { n e. RR | -u n e. A } e. Fin )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   = wceq 1284   e. wcel 1433   {cab 2067   A.wral 2348   E.wrex 2349   {crab 2352   _Vcvv 2601   C_ wss 2973   |-> cmpt 3839   dom cdm 4363   ran crn 4364   Fun wfun 4916   -1-1->wf1 4919   -1-1-onto->wf1o 4921   Fincfn 6244   CCcc 6979   RRcr 6980   -ucneg 7280

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-coll 3893  ax-sep 3896  ax-nul 3904  ax-pow 3948  ax-pr 3964  ax-un 4188  ax-setind 4280  ax-iinf 4329  ax-cnex 7067  ax-resscn 7068  ax-1cn 7069  ax-icn 7071  ax-addcl 7072  ax-addrcl 7073  ax-mulcl 7074  ax-addcom 7076  ax-addass 7078  ax-distr 7080  ax-i2m1 7081  ax-0id 7084  ax-rnegex 7085  ax-cnre 7087

This theorem depends on definitions:  df-bi 115  df-dc 776  df-3or 920  df-3an 921  df-tru 1287  df-fal 1290  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ne 2246  df-ral 2353  df-rex 2354  df-reu 2355  df-rab 2357  df-v 2603  df-sbc 2816  df-csb 2909  df-dif 2975  df-un 2977  df-in 2979  df-ss 2986  df-nul 3252  df-if 3352  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-int 3637  df-iun 3680  df-br 3786  df-opab 3840  df-mpt 3841  df-tr 3876  df-id 4048  df-iord 4121  df-on 4123  df-suc 4126  df-iom 4332  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-rn 4374  df-res 4375  df-ima 4376  df-iota 4887  df-fun 4924  df-fn 4925  df-f 4926  df-f1 4927  df-fo 4928  df-f1o 4929  df-fv 4930  df-riota 5488  df-ov 5535  df-oprab 5536  df-mpt2 5537  df-1st 5787  df-2nd 5788  df-1o 6024  df-er 6129  df-en 6245  df-fin 6247  df-sub 7281  df-neg 7282

This theorem is referenced by: (None)