This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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+ )