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

Metamath Proof Explorer

Theorem reefiso

Description: The exponential function on the reals determines an isomorphism from reals onto positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007) (Revised by Mario Carneiro, 11-Mar-2014)

Ref Expression
Assertion reefiso ( exp ↾ ℝ ) Isom < , < ( ℝ , ℝ+ )

Proof

Step Hyp Ref Expression
1 reeff1o ⊢ ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+
2 eflt ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 < 𝑦 ↔ ( exp ‘ 𝑥 ) < ( exp ‘ 𝑦 ) ) )
3 fvres ⊢ ( 𝑥 ∈ ℝ → ( ( exp ↾ ℝ ) ‘ 𝑥 ) = ( exp ‘ 𝑥 ) )
4 fvres ⊢ ( 𝑦 ∈ ℝ → ( ( exp ↾ ℝ ) ‘ 𝑦 ) = ( exp ‘ 𝑦 ) )
5 3 4 breqan12d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( exp ↾ ℝ ) ‘ 𝑥 ) < ( ( exp ↾ ℝ ) ‘ 𝑦 ) ↔ ( exp ‘ 𝑥 ) < ( exp ‘ 𝑦 ) ) )
6 2 5 bitr4d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 < 𝑦 ↔ ( ( exp ↾ ℝ ) ‘ 𝑥 ) < ( ( exp ↾ ℝ ) ‘ 𝑦 ) ) )
7 6 rgen2 ⊢ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 ↔ ( ( exp ↾ ℝ ) ‘ 𝑥 ) < ( ( exp ↾ ℝ ) ‘ 𝑦 ) )
8 df-isom ⊢ ( ( exp ↾ ℝ ) Isom < , < ( ℝ , ℝ+ ) ↔ ( ( exp ↾ ℝ ) : ℝ –1-1-onto→ ℝ+ ∧ ∀ 𝑥 ∈ ℝ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 ↔ ( ( exp ↾ ℝ ) ‘ 𝑥 ) < ( ( exp ↾ ℝ ) ‘ 𝑦 ) ) ) )
9 1 7 8 mpbir2an ⊢ ( exp ↾ ℝ ) Isom < , < ( ℝ , ℝ+ )