Metamath Proof Explorer


Theorem seff

Description: Let set S be the real or complex numbers. Then the exponential function restricted to S is a mapping from S to S . (Contributed by Steve Rodriguez, 6-Nov-2015)

Ref Expression
Hypothesis seff.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
Assertion seff ( 𝜑 → ( exp ↾ 𝑆 ) : 𝑆𝑆 )

Proof

Step Hyp Ref Expression
1 seff.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
2 elpri ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) )
3 reeff1 ( exp ↾ ℝ ) : ℝ –1-1→ ℝ+
4 f1f ( ( exp ↾ ℝ ) : ℝ –1-1→ ℝ+ → ( exp ↾ ℝ ) : ℝ ⟶ ℝ+ )
5 rpssre + ⊆ ℝ
6 fss ( ( ( exp ↾ ℝ ) : ℝ ⟶ ℝ+ ∧ ℝ+ ⊆ ℝ ) → ( exp ↾ ℝ ) : ℝ ⟶ ℝ )
7 5 6 mpan2 ( ( exp ↾ ℝ ) : ℝ ⟶ ℝ+ → ( exp ↾ ℝ ) : ℝ ⟶ ℝ )
8 3 4 7 mp2b ( exp ↾ ℝ ) : ℝ ⟶ ℝ
9 feq23 ( ( 𝑆 = ℝ ∧ 𝑆 = ℝ ) → ( ( exp ↾ ℝ ) : 𝑆𝑆 ↔ ( exp ↾ ℝ ) : ℝ ⟶ ℝ ) )
10 9 anidms ( 𝑆 = ℝ → ( ( exp ↾ ℝ ) : 𝑆𝑆 ↔ ( exp ↾ ℝ ) : ℝ ⟶ ℝ ) )
11 8 10 mpbiri ( 𝑆 = ℝ → ( exp ↾ ℝ ) : 𝑆𝑆 )
12 reseq2 ( 𝑆 = ℝ → ( exp ↾ 𝑆 ) = ( exp ↾ ℝ ) )
13 12 feq1d ( 𝑆 = ℝ → ( ( exp ↾ 𝑆 ) : 𝑆𝑆 ↔ ( exp ↾ ℝ ) : 𝑆𝑆 ) )
14 11 13 mpbird ( 𝑆 = ℝ → ( exp ↾ 𝑆 ) : 𝑆𝑆 )
15 eff exp : ℂ ⟶ ℂ
16 frel ( exp : ℂ ⟶ ℂ → Rel exp )
17 resdm ( Rel exp → ( exp ↾ dom exp ) = exp )
18 15 16 17 mp2b ( exp ↾ dom exp ) = exp
19 15 fdmi dom exp = ℂ
20 19 reseq2i ( exp ↾ dom exp ) = ( exp ↾ ℂ )
21 18 20 eqtr3i exp = ( exp ↾ ℂ )
22 21 feq1i ( exp : ℂ ⟶ ℂ ↔ ( exp ↾ ℂ ) : ℂ ⟶ ℂ )
23 15 22 mpbi ( exp ↾ ℂ ) : ℂ ⟶ ℂ
24 feq23 ( ( 𝑆 = ℂ ∧ 𝑆 = ℂ ) → ( ( exp ↾ ℂ ) : 𝑆𝑆 ↔ ( exp ↾ ℂ ) : ℂ ⟶ ℂ ) )
25 24 anidms ( 𝑆 = ℂ → ( ( exp ↾ ℂ ) : 𝑆𝑆 ↔ ( exp ↾ ℂ ) : ℂ ⟶ ℂ ) )
26 23 25 mpbiri ( 𝑆 = ℂ → ( exp ↾ ℂ ) : 𝑆𝑆 )
27 reseq2 ( 𝑆 = ℂ → ( exp ↾ 𝑆 ) = ( exp ↾ ℂ ) )
28 27 feq1d ( 𝑆 = ℂ → ( ( exp ↾ 𝑆 ) : 𝑆𝑆 ↔ ( exp ↾ ℂ ) : 𝑆𝑆 ) )
29 26 28 mpbird ( 𝑆 = ℂ → ( exp ↾ 𝑆 ) : 𝑆𝑆 )
30 14 29 jaoi ( ( 𝑆 = ℝ ∨ 𝑆 = ℂ ) → ( exp ↾ 𝑆 ) : 𝑆𝑆 )
31 1 2 30 3syl ( 𝜑 → ( exp ↾ 𝑆 ) : 𝑆𝑆 )