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	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right){Isom}_{<,<}\left({ℝ}^{+},ℝ\right)$$

Proof

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