Theorem reeff1

Description: The exponential function maps real arguments one-to-one to positive reals. (Contributed by Steve Rodriguez, 25-Aug-2007) (Revised by Mario Carneiro, 10-Nov-2013)

	Ref	Expression
Assertion	reeff1	⊢ ( exp ↾ ℝ ) : ℝ –1-1→ ℝ+

Proof

Step	Hyp	Ref	Expression
1		eff	⊢ exp : ℂ ⟶ ℂ
2		ffn	⊢ ( exp : ℂ ⟶ ℂ → exp Fn ℂ )
3	1 2	ax-mp	⊢ exp Fn ℂ
4		ax-resscn	⊢ ℝ ⊆ ℂ
5		fnssres	⊢ ( ( exp Fn ℂ ∧ ℝ ⊆ ℂ ) → ( exp ↾ ℝ ) Fn ℝ )
6	3 4 5	mp2an	⊢ ( exp ↾ ℝ ) Fn ℝ
7		fvres	⊢ ( 𝑥 ∈ ℝ → ( ( exp ↾ ℝ ) ‘ 𝑥 ) = ( exp ‘ 𝑥 ) )
8		rpefcl	⊢ ( 𝑥 ∈ ℝ → ( exp ‘ 𝑥 ) ∈ ℝ+ )
9	7 8	eqeltrd	⊢ ( 𝑥 ∈ ℝ → ( ( exp ↾ ℝ ) ‘ 𝑥 ) ∈ ℝ+ )
10	9	rgen	⊢ ∀ 𝑥 ∈ ℝ ( ( exp ↾ ℝ ) ‘ 𝑥 ) ∈ ℝ+
11		ffnfv	⊢ ( ( exp ↾ ℝ ) : ℝ ⟶ ℝ+ ↔ ( ( exp ↾ ℝ ) Fn ℝ ∧ ∀ 𝑥 ∈ ℝ ( ( exp ↾ ℝ ) ‘ 𝑥 ) ∈ ℝ+ ) )
12	6 10 11	mpbir2an	⊢ ( exp ↾ ℝ ) : ℝ ⟶ ℝ+
13		fvres	⊢ ( 𝑦 ∈ ℝ → ( ( exp ↾ ℝ ) ‘ 𝑦 ) = ( exp ‘ 𝑦 ) )
14	7 13	eqeqan12d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( exp ↾ ℝ ) ‘ 𝑥 ) = ( ( exp ↾ ℝ ) ‘ 𝑦 ) ↔ ( exp ‘ 𝑥 ) = ( exp ‘ 𝑦 ) ) )
15		reef11	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( exp ‘ 𝑥 ) = ( exp ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
16	15	biimpd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( exp ‘ 𝑥 ) = ( exp ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
17	14 16	sylbid	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( exp ↾ ℝ ) ‘ 𝑥 ) = ( ( exp ↾ ℝ ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
18	17	rgen2	⊢ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( ( ( exp ↾ ℝ ) ‘ 𝑥 ) = ( ( exp ↾ ℝ ) ‘ 𝑦 ) → 𝑥 = 𝑦 )
19		dff13	⊢ ( ( exp ↾ ℝ ) : ℝ –1-1→ ℝ+ ↔ ( ( exp ↾ ℝ ) : ℝ ⟶ ℝ+ ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( ( ( exp ↾ ℝ ) ‘ 𝑥 ) = ( ( exp ↾ ℝ ) ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
20	12 18 19	mpbir2an	⊢ ( exp ↾ ℝ ) : ℝ –1-1→ ℝ+