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 < , < ( ℝ , ℝ+ ) → ◡ ( 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 < , < ( ℝ+ , ℝ )