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

Metamath Proof Explorer

Theorem relogiso

Description: The natural logarithm function on positive reals determines an isomorphism from the positive reals onto the reals. (Contributed by Steve Rodriguez, 25-Nov-2007)

		Ref	Expression
	Assertion	relogiso	$⊢ ({log ↾}_{ℝ^{+}}) {Isom}_{<, <} (ℝ^{+}, ℝ)$

Proof

Step	Hyp	Ref	Expression
1		reefiso	$⊢ ({\exp ↾}_{ℝ}) {Isom}_{<, <} (ℝ, ℝ^{+})$
2		isocnv	$⊢ ({\exp ↾}_{ℝ}) {Isom}_{<, <} (ℝ, ℝ^{+}) \to {({\exp ↾}_{ℝ})}^{-1} {Isom}_{<, <} (ℝ^{+}, ℝ)$
3	1 2	ax-mp	$⊢ {({\exp ↾}_{ℝ})}^{-1} {Isom}_{<, <} (ℝ^{+}, ℝ)$
4		dfrelog	$⊢ {log ↾}_{ℝ^{+}} = {({\exp ↾}_{ℝ})}^{-1}$
5		isoeq1	$⊢ {log ↾}_{ℝ^{+}} = {({\exp ↾}_{ℝ})}^{-1} \to (({log ↾}_{ℝ^{+}}) {Isom}_{<, <} (ℝ^{+}, ℝ) \leftrightarrow {({\exp ↾}_{ℝ})}^{-1} {Isom}_{<, <} (ℝ^{+}, ℝ))$
6	4 5	ax-mp	$⊢ ({log ↾}_{ℝ^{+}}) {Isom}_{<, <} (ℝ^{+}, ℝ) \leftrightarrow {({\exp ↾}_{ℝ})}^{-1} {Isom}_{<, <} (ℝ^{+}, ℝ)$
7	3 6	mpbir	$⊢ ({log ↾}_{ℝ^{+}}) {Isom}_{<, <} (ℝ^{+}, ℝ)$