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 < , < ( ℝ , ℝ+ )