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→ ℝ