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→ ℝ )