dvne0f1

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

Step	Hyp	Ref	Expression
1		dvne0.a	$⊢ φ \to A \in ℝ$
2		dvne0.b	$⊢ φ \to B \in ℝ$
3		dvne0.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
4		dvne0.d	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
5		dvne0.z	$⊢ φ \to \neg 0 \in ran F_{ℝ}^{'}$
6	1 2 3 4 5	dvne0	$⊢ φ \to (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F))$
7		isof1o	$⊢ F {Isom}_{<, <} ([A, B], ran F) \to F : [A, B] \underset{1-1 onto}{⟶} ran F$
8		isof1o	$⊢ F {Isom}_{<, <^{-1}} ([A, B], ran F) \to F : [A, B] \underset{1-1 onto}{⟶} ran F$
9	7 8	jaoi	$⊢ (F {Isom}_{<, <} ([A, B], ran F) \lor F {Isom}_{<, <^{-1}} ([A, B], ran F)) \to F : [A, B] \underset{1-1 onto}{⟶} ran F$
10		f1of1	$⊢ F : [A, B] \underset{1-1 onto}{⟶} ran F \to F : [A, B] \underset{1-1}{⟶} ran F$
11	6 9 10	3syl	$⊢ φ \to F : [A, B] \underset{1-1}{⟶} ran F$
12		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℝ \to F : [A, B] ⟶ ℝ$
13		frn	$⊢ F : [A, B] ⟶ ℝ \to ran F \subseteq ℝ$
14	3 12 13	3syl	$⊢ φ \to ran F \subseteq ℝ$
15		f1ss	$⊢ (F : [A, B] \underset{1-1}{⟶} ran F \land ran F \subseteq ℝ) \to F : [A, B] \underset{1-1}{⟶} ℝ$
16	11 14 15	syl2anc	$⊢ φ \to F : [A, B] \underset{1-1}{⟶} ℝ$

Metamath Proof Explorer