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 )