Metamath Proof Explorer

Theorem recosf1o

Description: The cosine function is a bijection when restricted to its principal domain. (Contributed by Mario Carneiro, 12-May-2014)

Ref Expression
Assertion recosf1o 
|- ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) -1-1-onto-> ( -u 1 [,] 1 )

Proof

Step Hyp Ref Expression
1 cosf 
 |-  cos : CC --> CC
2 ffn 
 |-  ( cos : CC --> CC -> cos Fn CC )
3 1 2 ax-mp 
 |-  cos Fn CC
4 0re 
 |-  0 e. RR
5 pire 
 |-  _pi e. RR
6 iccssre 
 |-  ( ( 0 e. RR /\ _pi e. RR ) -> ( 0 [,] _pi ) C_ RR )
7 4 5 6 mp2an 
 |-  ( 0 [,] _pi ) C_ RR
8 ax-resscn 
 |-  RR C_ CC
9 7 8 sstri 
 |-  ( 0 [,] _pi ) C_ CC
10 fnssres 
 |-  ( ( cos Fn CC /\ ( 0 [,] _pi ) C_ CC ) -> ( cos |` ( 0 [,] _pi ) ) Fn ( 0 [,] _pi ) )
11 3 9 10 mp2an 
 |-  ( cos |` ( 0 [,] _pi ) ) Fn ( 0 [,] _pi )
12 fvres 
 |-  ( x e. ( 0 [,] _pi ) -> ( ( cos |` ( 0 [,] _pi ) ) ` x ) = ( cos ` x ) )
13 7 sseli 
 |-  ( x e. ( 0 [,] _pi ) -> x e. RR )
14 cosbnd2 
 |-  ( x e. RR -> ( cos ` x ) e. ( -u 1 [,] 1 ) )
15 13 14 syl 
 |-  ( x e. ( 0 [,] _pi ) -> ( cos ` x ) e. ( -u 1 [,] 1 ) )
16 12 15 eqeltrd 
 |-  ( x e. ( 0 [,] _pi ) -> ( ( cos |` ( 0 [,] _pi ) ) ` x ) e. ( -u 1 [,] 1 ) )
17 16 rgen 
 |-  A. x e. ( 0 [,] _pi ) ( ( cos |` ( 0 [,] _pi ) ) ` x ) e. ( -u 1 [,] 1 )
18 ffnfv 
 |-  ( ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) --> ( -u 1 [,] 1 ) <-> ( ( cos |` ( 0 [,] _pi ) ) Fn ( 0 [,] _pi ) /\ A. x e. ( 0 [,] _pi ) ( ( cos |` ( 0 [,] _pi ) ) ` x ) e. ( -u 1 [,] 1 ) ) )
19 11 17 18 mpbir2an 
 |-  ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) --> ( -u 1 [,] 1 )
20 fvres 
 |-  ( y e. ( 0 [,] _pi ) -> ( ( cos |` ( 0 [,] _pi ) ) ` y ) = ( cos ` y ) )
21 12 20 eqeqan12d 
 |-  ( ( x e. ( 0 [,] _pi ) /\ y e. ( 0 [,] _pi ) ) -> ( ( ( cos |` ( 0 [,] _pi ) ) ` x ) = ( ( cos |` ( 0 [,] _pi ) ) ` y ) <-> ( cos ` x ) = ( cos ` y ) ) )
22 cos11 
 |-  ( ( x e. ( 0 [,] _pi ) /\ y e. ( 0 [,] _pi ) ) -> ( x = y <-> ( cos ` x ) = ( cos ` y ) ) )
23 22 biimprd 
 |-  ( ( x e. ( 0 [,] _pi ) /\ y e. ( 0 [,] _pi ) ) -> ( ( cos ` x ) = ( cos ` y ) -> x = y ) )
24 21 23 sylbid 
 |-  ( ( x e. ( 0 [,] _pi ) /\ y e. ( 0 [,] _pi ) ) -> ( ( ( cos |` ( 0 [,] _pi ) ) ` x ) = ( ( cos |` ( 0 [,] _pi ) ) ` y ) -> x = y ) )
25 24 rgen2 
 |-  A. x e. ( 0 [,] _pi ) A. y e. ( 0 [,] _pi ) ( ( ( cos |` ( 0 [,] _pi ) ) ` x ) = ( ( cos |` ( 0 [,] _pi ) ) ` y ) -> x = y )
26 dff13 
 |-  ( ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) -1-1-> ( -u 1 [,] 1 ) <-> ( ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) --> ( -u 1 [,] 1 ) /\ A. x e. ( 0 [,] _pi ) A. y e. ( 0 [,] _pi ) ( ( ( cos |` ( 0 [,] _pi ) ) ` x ) = ( ( cos |` ( 0 [,] _pi ) ) ` y ) -> x = y ) ) )
27 19 25 26 mpbir2an 
 |-  ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) -1-1-> ( -u 1 [,] 1 )
28 4 a1i 
 |-  ( x e. ( -u 1 [,] 1 ) -> 0 e. RR )
29 5 a1i 
 |-  ( x e. ( -u 1 [,] 1 ) -> _pi e. RR )
30 neg1rr 
 |-  -u 1 e. RR
31 1re 
 |-  1 e. RR
32 30 31 elicc2i 
 |-  ( x e. ( -u 1 [,] 1 ) <-> ( x e. RR /\ -u 1 <_ x /\ x <_ 1 ) )
33 32 simp1bi 
 |-  ( x e. ( -u 1 [,] 1 ) -> x e. RR )
34 pipos 
 |-  0 < _pi
35 34 a1i 
 |-  ( x e. ( -u 1 [,] 1 ) -> 0 < _pi )
36 9 a1i 
 |-  ( x e. ( -u 1 [,] 1 ) -> ( 0 [,] _pi ) C_ CC )
37 coscn 
 |-  cos e. ( CC -cn-> CC )
38 37 a1i 
 |-  ( x e. ( -u 1 [,] 1 ) -> cos e. ( CC -cn-> CC ) )
39 7 sseli 
 |-  ( z e. ( 0 [,] _pi ) -> z e. RR )
40 39 recoscld 
 |-  ( z e. ( 0 [,] _pi ) -> ( cos ` z ) e. RR )
41 40 adantl 
 |-  ( ( x e. ( -u 1 [,] 1 ) /\ z e. ( 0 [,] _pi ) ) -> ( cos ` z ) e. RR )
42 cospi 
 |-  ( cos ` _pi ) = -u 1
43 32 simp2bi 
 |-  ( x e. ( -u 1 [,] 1 ) -> -u 1 <_ x )
44 42 43 eqbrtrid 
 |-  ( x e. ( -u 1 [,] 1 ) -> ( cos ` _pi ) <_ x )
45 32 simp3bi 
 |-  ( x e. ( -u 1 [,] 1 ) -> x <_ 1 )
46 cos0 
 |-  ( cos ` 0 ) = 1
47 45 46 breqtrrdi 
 |-  ( x e. ( -u 1 [,] 1 ) -> x <_ ( cos ` 0 ) )
48 44 47 jca 
 |-  ( x e. ( -u 1 [,] 1 ) -> ( ( cos ` _pi ) <_ x /\ x <_ ( cos ` 0 ) ) )
49 28 29 33 35 36 38 41 48 ivthle2 
 |-  ( x e. ( -u 1 [,] 1 ) -> E. y e. ( 0 [,] _pi ) ( cos ` y ) = x )
50 eqcom 
 |-  ( x = ( ( cos |` ( 0 [,] _pi ) ) ` y ) <-> ( ( cos |` ( 0 [,] _pi ) ) ` y ) = x )
51 20 eqeq1d 
 |-  ( y e. ( 0 [,] _pi ) -> ( ( ( cos |` ( 0 [,] _pi ) ) ` y ) = x <-> ( cos ` y ) = x ) )
52 50 51 syl5bb 
 |-  ( y e. ( 0 [,] _pi ) -> ( x = ( ( cos |` ( 0 [,] _pi ) ) ` y ) <-> ( cos ` y ) = x ) )
53 52 rexbiia 
 |-  ( E. y e. ( 0 [,] _pi ) x = ( ( cos |` ( 0 [,] _pi ) ) ` y ) <-> E. y e. ( 0 [,] _pi ) ( cos ` y ) = x )
54 49 53 sylibr 
 |-  ( x e. ( -u 1 [,] 1 ) -> E. y e. ( 0 [,] _pi ) x = ( ( cos |` ( 0 [,] _pi ) ) ` y ) )
55 54 rgen 
 |-  A. x e. ( -u 1 [,] 1 ) E. y e. ( 0 [,] _pi ) x = ( ( cos |` ( 0 [,] _pi ) ) ` y )
56 dffo3 
 |-  ( ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) -onto-> ( -u 1 [,] 1 ) <-> ( ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) --> ( -u 1 [,] 1 ) /\ A. x e. ( -u 1 [,] 1 ) E. y e. ( 0 [,] _pi ) x = ( ( cos |` ( 0 [,] _pi ) ) ` y ) ) )
57 19 55 56 mpbir2an 
 |-  ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) -onto-> ( -u 1 [,] 1 )
58 df-f1o 
 |-  ( ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) -1-1-onto-> ( -u 1 [,] 1 ) <-> ( ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) -1-1-> ( -u 1 [,] 1 ) /\ ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) -onto-> ( -u 1 [,] 1 ) ) )
59 27 57 58 mpbir2an 
 |-  ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) -1-1-onto-> ( -u 1 [,] 1 )