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 < , < ( ℝ , ℝ+ ) → ◡ ( exp ↾ ℝ ) Isom < , < ( ℝ+ , ℝ ) )
3	1 2	ax-mp	⊢ ◡ ( exp ↾ ℝ ) Isom < , < ( ℝ+ , ℝ )
4		dfrelog	⊢ ( log ↾ ℝ+ ) = ◡ ( exp ↾ ℝ )
5		isoeq1	⊢ ( ( log ↾ ℝ+ ) = ◡ ( exp ↾ ℝ ) → ( ( log ↾ ℝ+ ) Isom < , < ( ℝ+ , ℝ ) ↔ ◡ ( exp ↾ ℝ ) Isom < , < ( ℝ+ , ℝ ) ) )
6	4 5	ax-mp	⊢ ( ( log ↾ ℝ+ ) Isom < , < ( ℝ+ , ℝ ) ↔ ◡ ( exp ↾ ℝ ) Isom < , < ( ℝ+ , ℝ ) )
7	3 6	mpbir	⊢ ( log ↾ ℝ+ ) Isom < , < ( ℝ+ , ℝ )