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 
|- ( ( A C_ RR /\ A e. Fin ) -> { n e. RR | -u n e. A } e. Fin )

Proof

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