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 biimtrid 
 |-  ( 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 } )