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 ↾ 𝑆 ) : 𝑆 ⟶ 𝑆 )