Metamath Proof Explorer


Theorem negf1o

Description: Negation is an isomorphism of a subset of the real numbers to the negated elements of the subset. (Contributed by AV, 9-Aug-2020)

Ref Expression
Hypothesis negf1o.1
|- F = ( x e. A |-> -u x )
Assertion negf1o
|- ( A C_ RR -> F : A -1-1-onto-> { n e. RR | -u n e. A } )

Proof

Step Hyp Ref Expression
1 negf1o.1
 |-  F = ( x e. A |-> -u x )
2 negeq
 |-  ( n = -u x -> -u n = -u -u x )
3 2 eleq1d
 |-  ( n = -u x -> ( -u n e. A <-> -u -u x e. A ) )
4 ssel
 |-  ( A C_ RR -> ( x e. A -> x e. RR ) )
5 renegcl
 |-  ( x e. RR -> -u x e. RR )
6 4 5 syl6
 |-  ( A C_ RR -> ( x e. A -> -u x e. RR ) )
7 6 imp
 |-  ( ( A C_ RR /\ x e. A ) -> -u x e. RR )
8 4 imp
 |-  ( ( A C_ RR /\ x e. A ) -> x e. RR )
9 recn
 |-  ( x e. RR -> x e. CC )
10 negneg
 |-  ( x e. CC -> -u -u x = x )
11 10 eqcomd
 |-  ( x e. CC -> x = -u -u x )
12 9 11 syl
 |-  ( x e. RR -> x = -u -u x )
13 12 eleq1d
 |-  ( x e. RR -> ( x e. A <-> -u -u x e. A ) )
14 13 biimpcd
 |-  ( x e. A -> ( x e. RR -> -u -u x e. A ) )
15 14 adantl
 |-  ( ( A C_ RR /\ x e. A ) -> ( x e. RR -> -u -u x e. A ) )
16 8 15 mpd
 |-  ( ( A C_ RR /\ x e. A ) -> -u -u x e. A )
17 3 7 16 elrabd
 |-  ( ( A C_ RR /\ x e. A ) -> -u x e. { n e. RR | -u n e. A } )
18 negeq
 |-  ( n = y -> -u n = -u y )
19 18 eleq1d
 |-  ( n = y -> ( -u n e. A <-> -u y e. A ) )
20 19 elrab
 |-  ( y e. { n e. RR | -u n e. A } <-> ( y e. RR /\ -u y e. A ) )
21 simpr
 |-  ( ( y e. RR /\ -u y e. A ) -> -u y e. A )
22 21 a1i
 |-  ( A C_ RR -> ( ( y e. RR /\ -u y e. A ) -> -u y e. A ) )
23 20 22 syl5bi
 |-  ( A C_ RR -> ( y e. { n e. RR | -u n e. A } -> -u y e. A ) )
24 23 imp
 |-  ( ( A C_ RR /\ y e. { n e. RR | -u n e. A } ) -> -u y e. A )
25 4 9 syl6com
 |-  ( x e. A -> ( A C_ RR -> x e. CC ) )
26 25 adantl
 |-  ( ( ( y e. RR /\ -u y e. A ) /\ x e. A ) -> ( A C_ RR -> x e. CC ) )
27 26 imp
 |-  ( ( ( ( y e. RR /\ -u y e. A ) /\ x e. A ) /\ A C_ RR ) -> x e. CC )
28 recn
 |-  ( y e. RR -> y e. CC )
29 28 ad3antrrr
 |-  ( ( ( ( y e. RR /\ -u y e. A ) /\ x e. A ) /\ A C_ RR ) -> y e. CC )
30 negcon2
 |-  ( ( x e. CC /\ y e. CC ) -> ( x = -u y <-> y = -u x ) )
31 27 29 30 syl2anc
 |-  ( ( ( ( y e. RR /\ -u y e. A ) /\ x e. A ) /\ A C_ RR ) -> ( x = -u y <-> y = -u x ) )
32 31 exp31
 |-  ( ( y e. RR /\ -u y e. A ) -> ( x e. A -> ( A C_ RR -> ( x = -u y <-> y = -u x ) ) ) )
33 20 32 sylbi
 |-  ( y e. { n e. RR | -u n e. A } -> ( x e. A -> ( A C_ RR -> ( x = -u y <-> y = -u x ) ) ) )
34 33 impcom
 |-  ( ( x e. A /\ y e. { n e. RR | -u n e. A } ) -> ( A C_ RR -> ( x = -u y <-> y = -u x ) ) )
35 34 impcom
 |-  ( ( A C_ RR /\ ( x e. A /\ y e. { n e. RR | -u n e. A } ) ) -> ( x = -u y <-> y = -u x ) )
36 1 17 24 35 f1o2d
 |-  ( A C_ RR -> F : A -1-1-onto-> { n e. RR | -u n e. A } )