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

Metamath Proof Explorer

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