Metamath Proof Explorer

Theorem resinf1o

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

Ref Expression
Assertion resinf1o 
|- ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 )

Proof

Step Hyp Ref Expression
1 recosf1o 
 |-  ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) -1-1-onto-> ( -u 1 [,] 1 )
2 eqid 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) = ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) )
3 halfpire 
 |-  ( _pi / 2 ) e. RR
4 neghalfpire 
 |-  -u ( _pi / 2 ) e. RR
5 iccssre 
 |-  ( ( -u ( _pi / 2 ) e. RR /\ ( _pi / 2 ) e. RR ) -> ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) C_ RR )
6 4 3 5 mp2an 
 |-  ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) C_ RR
7 6 sseli 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> x e. RR )
8 resubcl 
 |-  ( ( ( _pi / 2 ) e. RR /\ x e. RR ) -> ( ( _pi / 2 ) - x ) e. RR )
9 3 7 8 sylancr 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( _pi / 2 ) - x ) e. RR )
10 4 3 elicc2i 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) <-> ( x e. RR /\ -u ( _pi / 2 ) <_ x /\ x <_ ( _pi / 2 ) ) )
11 10 simp3bi 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> x <_ ( _pi / 2 ) )
12 subge0 
 |-  ( ( ( _pi / 2 ) e. RR /\ x e. RR ) -> ( 0 <_ ( ( _pi / 2 ) - x ) <-> x <_ ( _pi / 2 ) ) )
13 3 7 12 sylancr 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( 0 <_ ( ( _pi / 2 ) - x ) <-> x <_ ( _pi / 2 ) ) )
14 11 13 mpbird 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> 0 <_ ( ( _pi / 2 ) - x ) )
15 3 recni 
 |-  ( _pi / 2 ) e. CC
16 picn 
 |-  _pi e. CC
17 15 negcli 
 |-  -u ( _pi / 2 ) e. CC
18 16 15 negsubi 
 |-  ( _pi + -u ( _pi / 2 ) ) = ( _pi - ( _pi / 2 ) )
19 pidiv2halves 
 |-  ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi
20 16 15 15 19 subaddrii 
 |-  ( _pi - ( _pi / 2 ) ) = ( _pi / 2 )
21 18 20 eqtri 
 |-  ( _pi + -u ( _pi / 2 ) ) = ( _pi / 2 )
22 15 16 17 21 subaddrii 
 |-  ( ( _pi / 2 ) - _pi ) = -u ( _pi / 2 )
23 10 simp2bi 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> -u ( _pi / 2 ) <_ x )
24 22 23 eqbrtrid 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( _pi / 2 ) - _pi ) <_ x )
25 pire 
 |-  _pi e. RR
26 suble 
 |-  ( ( ( _pi / 2 ) e. RR /\ _pi e. RR /\ x e. RR ) -> ( ( ( _pi / 2 ) - _pi ) <_ x <-> ( ( _pi / 2 ) - x ) <_ _pi ) )
27 3 25 7 26 mp3an12i 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( ( _pi / 2 ) - _pi ) <_ x <-> ( ( _pi / 2 ) - x ) <_ _pi ) )
28 24 27 mpbid 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( _pi / 2 ) - x ) <_ _pi )
29 0re 
 |-  0 e. RR
30 29 25 elicc2i 
 |-  ( ( ( _pi / 2 ) - x ) e. ( 0 [,] _pi ) <-> ( ( ( _pi / 2 ) - x ) e. RR /\ 0 <_ ( ( _pi / 2 ) - x ) /\ ( ( _pi / 2 ) - x ) <_ _pi ) )
31 9 14 28 30 syl3anbrc 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( _pi / 2 ) - x ) e. ( 0 [,] _pi ) )
32 31 adantl 
 |-  ( ( T. /\ x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) -> ( ( _pi / 2 ) - x ) e. ( 0 [,] _pi ) )
33 29 25 elicc2i 
 |-  ( y e. ( 0 [,] _pi ) <-> ( y e. RR /\ 0 <_ y /\ y <_ _pi ) )
34 33 simp1bi 
 |-  ( y e. ( 0 [,] _pi ) -> y e. RR )
35 resubcl 
 |-  ( ( ( _pi / 2 ) e. RR /\ y e. RR ) -> ( ( _pi / 2 ) - y ) e. RR )
36 3 34 35 sylancr 
 |-  ( y e. ( 0 [,] _pi ) -> ( ( _pi / 2 ) - y ) e. RR )
37 33 simp3bi 
 |-  ( y e. ( 0 [,] _pi ) -> y <_ _pi )
38 15 15 subnegi 
 |-  ( ( _pi / 2 ) - -u ( _pi / 2 ) ) = ( ( _pi / 2 ) + ( _pi / 2 ) )
39 38 19 eqtri 
 |-  ( ( _pi / 2 ) - -u ( _pi / 2 ) ) = _pi
40 37 39 breqtrrdi 
 |-  ( y e. ( 0 [,] _pi ) -> y <_ ( ( _pi / 2 ) - -u ( _pi / 2 ) ) )
41 lesub 
 |-  ( ( y e. RR /\ ( _pi / 2 ) e. RR /\ -u ( _pi / 2 ) e. RR ) -> ( y <_ ( ( _pi / 2 ) - -u ( _pi / 2 ) ) <-> -u ( _pi / 2 ) <_ ( ( _pi / 2 ) - y ) ) )
42 3 4 41 mp3an23 
 |-  ( y e. RR -> ( y <_ ( ( _pi / 2 ) - -u ( _pi / 2 ) ) <-> -u ( _pi / 2 ) <_ ( ( _pi / 2 ) - y ) ) )
43 34 42 syl 
 |-  ( y e. ( 0 [,] _pi ) -> ( y <_ ( ( _pi / 2 ) - -u ( _pi / 2 ) ) <-> -u ( _pi / 2 ) <_ ( ( _pi / 2 ) - y ) ) )
44 40 43 mpbid 
 |-  ( y e. ( 0 [,] _pi ) -> -u ( _pi / 2 ) <_ ( ( _pi / 2 ) - y ) )
45 15 subidi 
 |-  ( ( _pi / 2 ) - ( _pi / 2 ) ) = 0
46 33 simp2bi 
 |-  ( y e. ( 0 [,] _pi ) -> 0 <_ y )
47 45 46 eqbrtrid 
 |-  ( y e. ( 0 [,] _pi ) -> ( ( _pi / 2 ) - ( _pi / 2 ) ) <_ y )
48 suble 
 |-  ( ( ( _pi / 2 ) e. RR /\ ( _pi / 2 ) e. RR /\ y e. RR ) -> ( ( ( _pi / 2 ) - ( _pi / 2 ) ) <_ y <-> ( ( _pi / 2 ) - y ) <_ ( _pi / 2 ) ) )
49 3 3 34 48 mp3an12i 
 |-  ( y e. ( 0 [,] _pi ) -> ( ( ( _pi / 2 ) - ( _pi / 2 ) ) <_ y <-> ( ( _pi / 2 ) - y ) <_ ( _pi / 2 ) ) )
50 47 49 mpbid 
 |-  ( y e. ( 0 [,] _pi ) -> ( ( _pi / 2 ) - y ) <_ ( _pi / 2 ) )
51 4 3 elicc2i 
 |-  ( ( ( _pi / 2 ) - y ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) <-> ( ( ( _pi / 2 ) - y ) e. RR /\ -u ( _pi / 2 ) <_ ( ( _pi / 2 ) - y ) /\ ( ( _pi / 2 ) - y ) <_ ( _pi / 2 ) ) )
52 36 44 50 51 syl3anbrc 
 |-  ( y e. ( 0 [,] _pi ) -> ( ( _pi / 2 ) - y ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
53 52 adantl 
 |-  ( ( T. /\ y e. ( 0 [,] _pi ) ) -> ( ( _pi / 2 ) - y ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
54 iccssre 
 |-  ( ( 0 e. RR /\ _pi e. RR ) -> ( 0 [,] _pi ) C_ RR )
55 29 25 54 mp2an 
 |-  ( 0 [,] _pi ) C_ RR
56 ax-resscn 
 |-  RR C_ CC
57 55 56 sstri 
 |-  ( 0 [,] _pi ) C_ CC
58 57 sseli 
 |-  ( y e. ( 0 [,] _pi ) -> y e. CC )
59 6 56 sstri 
 |-  ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) C_ CC
60 59 sseli 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> x e. CC )
61 subsub23 
 |-  ( ( ( _pi / 2 ) e. CC /\ y e. CC /\ x e. CC ) -> ( ( ( _pi / 2 ) - y ) = x <-> ( ( _pi / 2 ) - x ) = y ) )
62 15 61 mp3an1 
 |-  ( ( y e. CC /\ x e. CC ) -> ( ( ( _pi / 2 ) - y ) = x <-> ( ( _pi / 2 ) - x ) = y ) )
63 58 60 62 syl2anr 
 |-  ( ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) /\ y e. ( 0 [,] _pi ) ) -> ( ( ( _pi / 2 ) - y ) = x <-> ( ( _pi / 2 ) - x ) = y ) )
64 63 adantl 
 |-  ( ( T. /\ ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) /\ y e. ( 0 [,] _pi ) ) ) -> ( ( ( _pi / 2 ) - y ) = x <-> ( ( _pi / 2 ) - x ) = y ) )
65 eqcom 
 |-  ( x = ( ( _pi / 2 ) - y ) <-> ( ( _pi / 2 ) - y ) = x )
66 eqcom 
 |-  ( y = ( ( _pi / 2 ) - x ) <-> ( ( _pi / 2 ) - x ) = y )
67 64 65 66 3bitr4g 
 |-  ( ( T. /\ ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) /\ y e. ( 0 [,] _pi ) ) ) -> ( x = ( ( _pi / 2 ) - y ) <-> y = ( ( _pi / 2 ) - x ) ) )
68 2 32 53 67 f1o2d 
 |-  ( T. -> ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( 0 [,] _pi ) )
69 68 mptru 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( 0 [,] _pi )
70 f1oco 
 |-  ( ( ( cos |` ( 0 [,] _pi ) ) : ( 0 [,] _pi ) -1-1-onto-> ( -u 1 [,] 1 ) /\ ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( 0 [,] _pi ) ) -> ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 ) )
71 1 69 70 mp2an 
 |-  ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 )
72 cosf 
 |-  cos : CC --> CC
73 ffn 
 |-  ( cos : CC --> CC -> cos Fn CC )
74 72 73 ax-mp 
 |-  cos Fn CC
75 fnssres 
 |-  ( ( cos Fn CC /\ ( 0 [,] _pi ) C_ CC ) -> ( cos |` ( 0 [,] _pi ) ) Fn ( 0 [,] _pi ) )
76 74 57 75 mp2an 
 |-  ( cos |` ( 0 [,] _pi ) ) Fn ( 0 [,] _pi )
77 2 31 fmpti 
 |-  ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) --> ( 0 [,] _pi )
78 fnfco 
 |-  ( ( ( cos |` ( 0 [,] _pi ) ) Fn ( 0 [,] _pi ) /\ ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) --> ( 0 [,] _pi ) ) -> ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) Fn ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
79 76 77 78 mp2an 
 |-  ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) Fn ( -u ( _pi / 2 ) [,] ( _pi / 2 ) )
80 sinf 
 |-  sin : CC --> CC
81 ffn 
 |-  ( sin : CC --> CC -> sin Fn CC )
82 80 81 ax-mp 
 |-  sin Fn CC
83 fnssres 
 |-  ( ( sin Fn CC /\ ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) C_ CC ) -> ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) Fn ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
84 82 59 83 mp2an 
 |-  ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) Fn ( -u ( _pi / 2 ) [,] ( _pi / 2 ) )
85 eqfnfv 
 |-  ( ( ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) Fn ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) /\ ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) Fn ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) -> ( ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) = ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) <-> A. y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ( ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) ` y ) = ( ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` y ) ) )
86 79 84 85 mp2an 
 |-  ( ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) = ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) <-> A. y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ( ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) ` y ) = ( ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` y ) )
87 77 ffvelcdmi 
 |-  ( y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ` y ) e. ( 0 [,] _pi ) )
88 87 fvresd 
 |-  ( y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( cos |` ( 0 [,] _pi ) ) ` ( ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ` y ) ) = ( cos ` ( ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ` y ) ) )
89 oveq2 
 |-  ( x = y -> ( ( _pi / 2 ) - x ) = ( ( _pi / 2 ) - y ) )
90 ovex 
 |-  ( ( _pi / 2 ) - y ) e. _V
91 89 2 90 fvmpt 
 |-  ( y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ` y ) = ( ( _pi / 2 ) - y ) )
92 91 fveq2d 
 |-  ( y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( cos ` ( ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ` y ) ) = ( cos ` ( ( _pi / 2 ) - y ) ) )
93 59 sseli 
 |-  ( y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> y e. CC )
94 coshalfpim 
 |-  ( y e. CC -> ( cos ` ( ( _pi / 2 ) - y ) ) = ( sin ` y ) )
95 93 94 syl 
 |-  ( y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( cos ` ( ( _pi / 2 ) - y ) ) = ( sin ` y ) )
96 88 92 95 3eqtrd 
 |-  ( y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( cos |` ( 0 [,] _pi ) ) ` ( ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ` y ) ) = ( sin ` y ) )
97 fvco3 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) --> ( 0 [,] _pi ) /\ y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) -> ( ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) ` y ) = ( ( cos |` ( 0 [,] _pi ) ) ` ( ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ` y ) ) )
98 77 97 mpan 
 |-  ( y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) ` y ) = ( ( cos |` ( 0 [,] _pi ) ) ` ( ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ` y ) ) )
99 fvres 
 |-  ( y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` y ) = ( sin ` y ) )
100 96 98 99 3eqtr4d 
 |-  ( y e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) ` y ) = ( ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` y ) )
101 86 100 mprgbir 
 |-  ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) = ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
102 f1oeq1 
 |-  ( ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) = ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) -> ( ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 ) <-> ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 ) ) )
103 101 102 ax-mp 
 |-  ( ( ( cos |` ( 0 [,] _pi ) ) o. ( x e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) |-> ( ( _pi / 2 ) - x ) ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 ) <-> ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 ) )
104 71 103 mpbi 
 |-  ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 )