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

Metamath Proof Explorer

Theorem dvne0f1

Description: A function on a closed interval with nonzero derivative is one-to-one. (Contributed by Mario Carneiro, 19-Feb-2015)

Ref Expression
Hypotheses dvne0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dvne0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
dvne0.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
dvne0.d ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
dvne0.z ⊢ ( 𝜑 → ¬ 0 ∈ ran ( ℝ D 𝐹 ) )
Assertion dvne0f1 ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) –1-1→ ℝ )

Proof

Step Hyp Ref Expression
1 dvne0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 dvne0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 dvne0.f ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
4 dvne0.d ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
5 dvne0.z ⊢ ( 𝜑 → ¬ 0 ∈ ran ( ℝ D 𝐹 ) )
6 1 2 3 4 5 dvne0 ⊢ ( 𝜑 → ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) )
7 isof1o ⊢ ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) → 𝐹 : ( 𝐴 [,] 𝐵 ) –1-1-onto→ ran 𝐹 )
8 isof1o ⊢ ( 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) → 𝐹 : ( 𝐴 [,] 𝐵 ) –1-1-onto→ ran 𝐹 )
9 7 8 jaoi ⊢ ( ( 𝐹 Isom < , < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ∨ 𝐹 Isom < , ◡ < ( ( 𝐴 [,] 𝐵 ) , ran 𝐹 ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) –1-1-onto→ ran 𝐹 )
10 f1of1 ⊢ ( 𝐹 : ( 𝐴 [,] 𝐵 ) –1-1-onto→ ran 𝐹 → 𝐹 : ( 𝐴 [,] 𝐵 ) –1-1→ ran 𝐹 )
11 6 9 10 3syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) –1-1→ ran 𝐹 )
12 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ )
13 frn ⊢ ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℝ → ran 𝐹 ⊆ ℝ )
14 3 12 13 3syl ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
15 f1ss ⊢ ( ( 𝐹 : ( 𝐴 [,] 𝐵 ) –1-1→ ran 𝐹 ∧ ran 𝐹 ⊆ ℝ ) → 𝐹 : ( 𝐴 [,] 𝐵 ) –1-1→ ℝ )
16 11 14 15 syl2anc ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) –1-1→ ℝ )