Theorem relogf1o

Description: The natural logarithm function maps the positive reals one-to-one onto the real numbers. (Contributed by Paul Chapman, 21-Apr-2008)

	Ref	Expression
Assertion	relogf1o	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ$$

Proof

Step	Hyp	Ref	Expression
1		eff1o2	$$⊢\left({\exp \upharpoonright }_{\mathrm{ran}log}\right):\mathrm{ran}log\underset{1-1\; onto}{⟶}ℂ\setminus \left\{0\right\}$$
2		dff1o3	$$⊢\left({\exp \upharpoonright }_{\mathrm{ran}log}\right):\mathrm{ran}log\underset{1-1\; onto}{⟶}ℂ\setminus \left\{0\right\}\leftrightarrow \left(\left({\exp \upharpoonright }_{\mathrm{ran}log}\right):\mathrm{ran}log\underset{onto}{⟶}ℂ\setminus \left\{0\right\}\wedge \mathrm{Fun}{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\right)$$
3	2	simprbi	$$⊢\left({\exp \upharpoonright }_{\mathrm{ran}log}\right):\mathrm{ran}log\underset{1-1\; onto}{⟶}ℂ\setminus \left\{0\right\}\to \mathrm{Fun}{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}$$
4	1 3	ax-mp	$$⊢\mathrm{Fun}{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}$$
5		reeff1o	$$⊢\left({\exp \upharpoonright }_{ℝ}\right):ℝ\underset{1-1\; onto}{⟶}{ℝ}^{+}$$
6		relogrn	$$⊢x\in ℝ\to x\in \mathrm{ran}log$$
7	6	ssriv	$$⊢ℝ\subseteq \mathrm{ran}log$$
8		resabs1	$$⊢ℝ\subseteq \mathrm{ran}log\to {\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\upharpoonright }_{ℝ}={\exp \upharpoonright }_{ℝ}$$
9		f1oeq1	$$⊢{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\upharpoonright }_{ℝ}={\exp \upharpoonright }_{ℝ}\to \left(\left({\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\upharpoonright }_{ℝ}\right):ℝ\underset{1-1\; onto}{⟶}{ℝ}^{+}\leftrightarrow \left({\exp \upharpoonright }_{ℝ}\right):ℝ\underset{1-1\; onto}{⟶}{ℝ}^{+}\right)$$
10	7 8 9	mp2b	$$⊢\left({\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\upharpoonright }_{ℝ}\right):ℝ\underset{1-1\; onto}{⟶}{ℝ}^{+}\leftrightarrow \left({\exp \upharpoonright }_{ℝ}\right):ℝ\underset{1-1\; onto}{⟶}{ℝ}^{+}$$
11	5 10	mpbir	$$⊢\left({\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\upharpoonright }_{ℝ}\right):ℝ\underset{1-1\; onto}{⟶}{ℝ}^{+}$$
12		f1orescnv	$$⊢\left(\mathrm{Fun}{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\wedge \left({\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)\upharpoonright }_{ℝ}\right):ℝ\underset{1-1\; onto}{⟶}{ℝ}^{+}\right)\to \left({{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ$$
13	4 11 12	mp2an	$$⊢\left({{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ$$
14		dflog2	$$⊢log={\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}$$
15		reseq1	$$⊢log={\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\to {log\upharpoonright }_{{ℝ}^{+}}={{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\upharpoonright }_{{ℝ}^{+}}$$
16		f1oeq1	$$⊢{log\upharpoonright }_{{ℝ}^{+}}={{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\upharpoonright }_{{ℝ}^{+}}\to \left(\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ\leftrightarrow \left({{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ\right)$$
17	14 15 16	mp2b	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ\leftrightarrow \left({{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ$$
18	13 17	mpbir	$$⊢\left({log\upharpoonright }_{{ℝ}^{+}}\right):{ℝ}^{+}\underset{1-1\; onto}{⟶}ℝ$$