reeff1

Description: The exponential function maps real arguments one-to-one to positive reals. (Contributed by Steve Rodriguez, 25-Aug-2007) (Revised by Mario Carneiro, 10-Nov-2013)

		Ref	Expression
	Assertion	reeff1	$⊢ ({\exp ↾}_{ℝ}) : ℝ \underset{1-1}{⟶} ℝ^{+}$

Proof

Step	Hyp	Ref	Expression
1		eff	$⊢ \exp : ℂ ⟶ ℂ$
2		ffn	$⊢ \exp : ℂ ⟶ ℂ \to \exp Fn ℂ$
3	1 2	ax-mp	$⊢ \exp Fn ℂ$
4		ax-resscn	$⊢ ℝ \subseteq ℂ$
5		fnssres	$⊢ (\exp Fn ℂ \land ℝ \subseteq ℂ) \to ({\exp ↾}_{ℝ}) Fn ℝ$
6	3 4 5	mp2an	$⊢ ({\exp ↾}_{ℝ}) Fn ℝ$
7		fvres	$⊢ x \in ℝ \to ({\exp ↾}_{ℝ}) (x) = e^{x}$
8		rpefcl	$⊢ x \in ℝ \to e^{x} \in ℝ^{+}$
9	7 8	eqeltrd	$⊢ x \in ℝ \to ({\exp ↾}_{ℝ}) (x) \in ℝ^{+}$
10	9	rgen	$⊢ \forall x \in ℝ ({\exp ↾}_{ℝ}) (x) \in ℝ^{+}$
11		ffnfv	$⊢ ({\exp ↾}_{ℝ}) : ℝ ⟶ ℝ^{+} \leftrightarrow (({\exp ↾}_{ℝ}) Fn ℝ \land \forall x \in ℝ ({\exp ↾}_{ℝ}) (x) \in ℝ^{+})$
12	6 10 11	mpbir2an	$⊢ ({\exp ↾}_{ℝ}) : ℝ ⟶ ℝ^{+}$
13		fvres	$⊢ y \in ℝ \to ({\exp ↾}_{ℝ}) (y) = e^{y}$
14	7 13	eqeqan12d	$⊢ (x \in ℝ \land y \in ℝ) \to (({\exp ↾}_{ℝ}) (x) = ({\exp ↾}_{ℝ}) (y) \leftrightarrow e^{x} = e^{y})$
15		reef11	$⊢ (x \in ℝ \land y \in ℝ) \to (e^{x} = e^{y} \leftrightarrow x = y)$
16	15	biimpd	$⊢ (x \in ℝ \land y \in ℝ) \to (e^{x} = e^{y} \to x = y)$
17	14 16	sylbid	$⊢ (x \in ℝ \land y \in ℝ) \to (({\exp ↾}_{ℝ}) (x) = ({\exp ↾}_{ℝ}) (y) \to x = y)$
18	17	rgen2	$⊢ \forall x \in ℝ \forall y \in ℝ (({\exp ↾}_{ℝ}) (x) = ({\exp ↾}_{ℝ}) (y) \to x = y)$
19		dff13	$⊢ ({\exp ↾}_{ℝ}) : ℝ \underset{1-1}{⟶} ℝ^{+} \leftrightarrow (({\exp ↾}_{ℝ}) : ℝ ⟶ ℝ^{+} \land \forall x \in ℝ \forall y \in ℝ (({\exp ↾}_{ℝ}) (x) = ({\exp ↾}_{ℝ}) (y) \to x = y))$
20	12 18 19	mpbir2an	$⊢ ({\exp ↾}_{ℝ}) : ℝ \underset{1-1}{⟶} ℝ^{+}$

Metamath Proof Explorer

Theorem reeff1

Proof