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	|- ( ph -> A e. RR )
	dvne0.b	|- ( ph -> B e. RR )
	dvne0.f	|- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
	dvne0.d	|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
	dvne0.z	|- ( ph -> -. 0 e. ran ( RR _D F ) )
Assertion	dvne0f1	|- ( ph -> F : ( A [,] B ) -1-1-> RR )

Proof

Step	Hyp	Ref	Expression
1		dvne0.a	|- ( ph -> A e. RR )
2		dvne0.b	|- ( ph -> B e. RR )
3		dvne0.f	|- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
4		dvne0.d	|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
5		dvne0.z	|- ( ph -> -. 0 e. ran ( RR _D F ) )
6	1 2 3 4 5	dvne0	|- ( ph -> ( F Isom < , < ( ( A [,] B ) , ran F ) \/ F Isom < , `' < ( ( A [,] B ) , ran F ) ) )
7		isof1o	|- ( F Isom < , < ( ( A [,] B ) , ran F ) -> F : ( A [,] B ) -1-1-onto-> ran F )
8		isof1o	|- ( F Isom < , `' < ( ( A [,] B ) , ran F ) -> F : ( A [,] B ) -1-1-onto-> ran F )
9	7 8	jaoi	|- ( ( F Isom < , < ( ( A [,] B ) , ran F ) \/ F Isom < , `' < ( ( A [,] B ) , ran F ) ) -> F : ( A [,] B ) -1-1-onto-> ran F )
10		f1of1	|- ( F : ( A [,] B ) -1-1-onto-> ran F -> F : ( A [,] B ) -1-1-> ran F )
11	6 9 10	3syl	|- ( ph -> F : ( A [,] B ) -1-1-> ran F )
12		cncff	|- ( F e. ( ( A [,] B ) -cn-> RR ) -> F : ( A [,] B ) --> RR )
13		frn	|- ( F : ( A [,] B ) --> RR -> ran F C_ RR )
14	3 12 13	3syl	|- ( ph -> ran F C_ RR )
15		f1ss	|- ( ( F : ( A [,] B ) -1-1-> ran F /\ ran F C_ RR ) -> F : ( A [,] B ) -1-1-> RR )
16	11 14 15	syl2anc	|- ( ph -> F : ( A [,] B ) -1-1-> RR )