Theorem reefiso

Description: The exponential function on the reals determines an isomorphism from reals onto positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007) (Revised by Mario Carneiro, 11-Mar-2014)

	Ref	Expression
Assertion	reefiso	|- ( exp |` RR ) Isom < , < ( RR , RR+ )

Proof

Step	Hyp	Ref	Expression
1		reeff1o	|- ( exp |` RR ) : RR -1-1-onto-> RR+
2		eflt	|- ( ( x e. RR /\ y e. RR ) -> ( x < y <-> ( exp ` x ) < ( exp ` y ) ) )
3		fvres	|- ( x e. RR -> ( ( exp |` RR ) ` x ) = ( exp ` x ) )
4		fvres	|- ( y e. RR -> ( ( exp |` RR ) ` y ) = ( exp ` y ) )
5	3 4	breqan12d	|- ( ( x e. RR /\ y e. RR ) -> ( ( ( exp |` RR ) ` x ) < ( ( exp |` RR ) ` y ) <-> ( exp ` x ) < ( exp ` y ) ) )
6	2 5	bitr4d	|- ( ( x e. RR /\ y e. RR ) -> ( x < y <-> ( ( exp |` RR ) ` x ) < ( ( exp |` RR ) ` y ) ) )
7	6	rgen2	|- A. x e. RR A. y e. RR ( x < y <-> ( ( exp |` RR ) ` x ) < ( ( exp |` RR ) ` y ) )
8		df-isom	|- ( ( exp |` RR ) Isom < , < ( RR , RR+ ) <-> ( ( exp |` RR ) : RR -1-1-onto-> RR+ /\ A. x e. RR A. y e. RR ( x < y <-> ( ( exp |` RR ) ` x ) < ( ( exp |` RR ) ` y ) ) ) )
9	1 7 8	mpbir2an	|- ( exp |` RR ) Isom < , < ( RR , RR+ )