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

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 ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ

Proof

Step Hyp Ref Expression
1 eff1o2 ⊢ ( exp ↾ ran log ) : ran log –1-1-onto→ ( ℂ ∖ { 0 } )
2 dff1o3 ⊢ ( ( exp ↾ ran log ) : ran log –1-1-onto→ ( ℂ ∖ { 0 } ) ↔ ( ( exp ↾ ran log ) : ran log –onto→ ( ℂ ∖ { 0 } ) ∧ Fun ◡ ( exp ↾ ran log ) ) )
3 2 simprbi ⊢ ( ( exp ↾ ran log ) : ran log –1-1-onto→ ( ℂ ∖ { 0 } ) → Fun ◡ ( exp ↾ ran log ) )
4 1 3 ax-mp ⊢ Fun ◡ ( exp ↾ ran log )
5 reeff1o ⊢ ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+
6 relogrn ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ran log )
7 6 ssriv ⊢ ℝ ⊆ ran log
8 resabs1 ⊢ ( ℝ ⊆ ran log → ( ( exp ↾ ran log ) ↾ ℝ ) = ( exp ↾ ℝ ) )
9 f1oeq1 ⊢ ( ( ( exp ↾ ran log ) ↾ ℝ ) = ( exp ↾ ℝ ) → ( ( ( exp ↾ ran log ) ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ ↔ ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ ) )
10 7 8 9 mp2b ⊢ ( ( ( exp ↾ ran log ) ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ ↔ ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ )
11 5 10 mpbir ⊢ ( ( exp ↾ ran log ) ↾ ℝ ) : ℝ –1-1-onto→ ℝ+
12 f1orescnv ⊢ ( ( Fun ◡ ( exp ↾ ran log ) ∧ ( ( exp ↾ ran log ) ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ ) → ( ◡ ( exp ↾ ran log ) ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ )
13 4 11 12 mp2an ⊢ ( ◡ ( exp ↾ ran log ) ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ
14 dflog2 ⊢ log = ◡ ( exp ↾ ran log )
15 reseq1 ⊢ ( log = ◡ ( exp ↾ ran log ) → ( log ↾ ℝ+ ) = ( ◡ ( exp ↾ ran log ) ↾ ℝ+ ) )
16 f1oeq1 ⊢ ( ( log ↾ ℝ+ ) = ( ◡ ( exp ↾ ran log ) ↾ ℝ+ ) → ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ ↔ ( ◡ ( exp ↾ ran log ) ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ ) )
17 14 15 16 mp2b ⊢ ( ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ ↔ ( ◡ ( exp ↾ ran log ) ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ )
18 13 17 mpbir ⊢ ( log ↾ ℝ+ ) : ℝ+ –1-1-onto→ ℝ