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 expIsom<,<+

Proof

Step Hyp Ref Expression
1 reeff1o exp:1-1 onto+
2 eflt xyx<yex<ey
3 fvres xexpx=ex
4 fvres yexpy=ey
5 3 4 breqan12d xyexpx<expyex<ey
6 2 5 bitr4d xyx<yexpx<expy
7 6 rgen2 xyx<yexpx<expy
8 df-isom expIsom<,<+exp:1-1 onto+xyx<yexpx<expy
9 1 7 8 mpbir2an expIsom<,<+