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

Metamath Proof Explorer

Theorem reefiso

Description: The exponential function on the reals determines an isomorphism from reals onto positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007) (Revised by Mario Carneiro, 11-Mar-2014)

		Ref	Expression
	Assertion	reefiso	$⊢ ({\exp ↾}_{ℝ}) {Isom}_{<, <} (ℝ, ℝ^{+})$

Proof

Step	Hyp	Ref	Expression
1		reeff1o	$⊢ ({\exp ↾}_{ℝ}) : ℝ \underset{1-1 onto}{⟶} ℝ^{+}$
2		eflt	$⊢ (x \in ℝ \land y \in ℝ) \to (x < y \leftrightarrow e^{x} < e^{y})$
3		fvres	$⊢ x \in ℝ \to ({\exp ↾}_{ℝ}) (x) = e^{x}$
4		fvres	$⊢ y \in ℝ \to ({\exp ↾}_{ℝ}) (y) = e^{y}$
5	3 4	breqan12d	$⊢ (x \in ℝ \land y \in ℝ) \to (({\exp ↾}_{ℝ}) (x) < ({\exp ↾}_{ℝ}) (y) \leftrightarrow e^{x} < e^{y})$
6	2 5	bitr4d	$⊢ (x \in ℝ \land y \in ℝ) \to (x < y \leftrightarrow ({\exp ↾}_{ℝ}) (x) < ({\exp ↾}_{ℝ}) (y))$
7	6	rgen2	$⊢ \forall x \in ℝ \forall y \in ℝ (x < y \leftrightarrow ({\exp ↾}_{ℝ}) (x) < ({\exp ↾}_{ℝ}) (y))$
8		df-isom	$⊢ ({\exp ↾}_{ℝ}) {Isom}_{<, <} (ℝ, ℝ^{+}) \leftrightarrow (({\exp ↾}_{ℝ}) : ℝ \underset{1-1 onto}{⟶} ℝ^{+} \land \forall x \in ℝ \forall y \in ℝ (x < y \leftrightarrow ({\exp ↾}_{ℝ}) (x) < ({\exp ↾}_{ℝ}) (y)))$
9	1 7 8	mpbir2an	$⊢ ({\exp ↾}_{ℝ}) {Isom}_{<, <} (ℝ, ℝ^{+})$