This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) : ( - ( π / 2 ) [,] ( π / 2 ) ) –1-1-onto→ ( - 1 [,] 1 )

Proof

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