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 |` RR+ ) Isom < , < ( RR+ , RR )

Proof

Step Hyp Ref Expression
1 reefiso
 |-  ( exp |` RR ) Isom < , < ( RR , RR+ )
2 isocnv
 |-  ( ( exp |` RR ) Isom < , < ( RR , RR+ ) -> `' ( exp |` RR ) Isom < , < ( RR+ , RR ) )
3 1 2 ax-mp
 |-  `' ( exp |` RR ) Isom < , < ( RR+ , RR )
4 dfrelog
 |-  ( log |` RR+ ) = `' ( exp |` RR )
5 isoeq1
 |-  ( ( log |` RR+ ) = `' ( exp |` RR ) -> ( ( log |` RR+ ) Isom < , < ( RR+ , RR ) <-> `' ( exp |` RR ) Isom < , < ( RR+ , RR ) ) )
6 4 5 ax-mp
 |-  ( ( log |` RR+ ) Isom < , < ( RR+ , RR ) <-> `' ( exp |` RR ) Isom < , < ( RR+ , RR ) )
7 3 6 mpbir
 |-  ( log |` RR+ ) Isom < , < ( RR+ , RR )