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 37 rexlimdva
 |-  ( A C_ RR -> ( E. a e. A n = -u a -> ( n e. RR /\ -u n e. A ) ) )
39 simprr
 |-  ( ( A C_ RR /\ ( n e. RR /\ -u n e. A ) ) -> -u n e. A )
40 negeq
 |-  ( a = -u n -> -u a = -u -u n )
41 40 eqeq2d
 |-  ( a = -u n -> ( n = -u a <-> n = -u -u n ) )
42 41 adantl
 |-  ( ( ( A C_ RR /\ ( n e. RR /\ -u n e. A ) ) /\ a = -u n ) -> ( n = -u a <-> n = -u -u n ) )
43 recn
 |-  ( n e. RR -> n e. CC )
44 negneg
 |-  ( n e. CC -> -u -u n = n )
45 44 eqcomd
 |-  ( n e. CC -> n = -u -u n )
46 43 45 syl
 |-  ( n e. RR -> n = -u -u n )
47 46 ad2antrl
 |-  ( ( A C_ RR /\ ( n e. RR /\ -u n e. A ) ) -> n = -u -u n )
48 39 42 47 rspcedvd
 |-  ( ( A C_ RR /\ ( n e. RR /\ -u n e. A ) ) -> E. a e. A n = -u a )
49 48 ex
 |-  ( A C_ RR -> ( ( n e. RR /\ -u n e. A ) -> E. a e. A n = -u a ) )
50 38 49 impbid
 |-  ( A C_ RR -> ( E. a e. A n = -u a <-> ( n e. RR /\ -u n e. A ) ) )
51 50 abbidv
 |-  ( A C_ RR -> { n | E. a e. A n = -u a } = { n | ( n e. RR /\ -u n e. A ) } )
52 16 rnmpt
 |-  ran ( a e. A |-> -u a ) = { n | E. a e. A n = -u a }
53 df-rab
 |-  { n e. RR | -u n e. A } = { n | ( n e. RR /\ -u n e. A ) }
54 51 52 53 3eqtr4g
 |-  ( A C_ RR -> ran ( a e. A |-> -u a ) = { n e. RR | -u n e. A } )
55 54 eleq1d
 |-  ( A C_ RR -> ( ran ( a e. A |-> -u a ) e. Fin <-> { n e. RR | -u n e. A } e. Fin ) )
56 12 21 55 3bitrd
 |-  ( A C_ RR -> ( A e. Fin <-> { n e. RR | -u n e. A } e. Fin ) )
57 56 biimpa
 |-  ( ( A C_ RR /\ A e. Fin ) -> { n e. RR | -u n e. A } e. Fin )