Metamath Proof Explorer

Theorem relogf1o

Description: The natural logarithm function maps the positive reals one-to-one onto the real numbers. (Contributed by Paul Chapman, 21-Apr-2008)

Ref Expression
Assertion relogf1o 
|- ( log |` RR+ ) : RR+ -1-1-onto-> RR

Proof

Step Hyp Ref Expression
1 eff1o2 
 |-  ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } )
2 dff1o3 
 |-  ( ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } ) <-> ( ( exp |` ran log ) : ran log -onto-> ( CC \ { 0 } ) /\ Fun `' ( exp |` ran log ) ) )
3 2 simprbi 
 |-  ( ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } ) -> Fun `' ( exp |` ran log ) )
4 1 3 ax-mp 
 |-  Fun `' ( exp |` ran log )
5 reeff1o 
 |-  ( exp |` RR ) : RR -1-1-onto-> RR+
6 relogrn 
 |-  ( x e. RR -> x e. ran log )
7 6 ssriv 
 |-  RR C_ ran log
8 resabs1 
 |-  ( RR C_ ran log -> ( ( exp |` ran log ) |` RR ) = ( exp |` RR ) )
9 f1oeq1 
 |-  ( ( ( exp |` ran log ) |` RR ) = ( exp |` RR ) -> ( ( ( exp |` ran log ) |` RR ) : RR -1-1-onto-> RR+ <-> ( exp |` RR ) : RR -1-1-onto-> RR+ ) )
10 7 8 9 mp2b 
 |-  ( ( ( exp |` ran log ) |` RR ) : RR -1-1-onto-> RR+ <-> ( exp |` RR ) : RR -1-1-onto-> RR+ )
11 5 10 mpbir 
 |-  ( ( exp |` ran log ) |` RR ) : RR -1-1-onto-> RR+
12 f1orescnv 
 |-  ( ( Fun `' ( exp |` ran log ) /\ ( ( exp |` ran log ) |` RR ) : RR -1-1-onto-> RR+ ) -> ( `' ( exp |` ran log ) |` RR+ ) : RR+ -1-1-onto-> RR )
13 4 11 12 mp2an 
 |-  ( `' ( exp |` ran log ) |` RR+ ) : RR+ -1-1-onto-> RR
14 dflog2 
 |-  log = `' ( exp |` ran log )
15 reseq1 
 |-  ( log = `' ( exp |` ran log ) -> ( log |` RR+ ) = ( `' ( exp |` ran log ) |` RR+ ) )
16 f1oeq1 
 |-  ( ( log |` RR+ ) = ( `' ( exp |` ran log ) |` RR+ ) -> ( ( log |` RR+ ) : RR+ -1-1-onto-> RR <-> ( `' ( exp |` ran log ) |` RR+ ) : RR+ -1-1-onto-> RR ) )
17 14 15 16 mp2b 
 |-  ( ( log |` RR+ ) : RR+ -1-1-onto-> RR <-> ( `' ( exp |` ran log ) |` RR+ ) : RR+ -1-1-onto-> RR )
18 13 17 mpbir 
 |-  ( log |` RR+ ) : RR+ -1-1-onto-> RR