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 φ S
Assertion seff φ exp S : S S

Proof

Step Hyp Ref Expression
1 seff.s φ S
2 elpri S S = S =
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 S = S = exp : S S exp :
10 9 anidms S = exp : S S exp :
11 8 10 mpbiri S = exp : S S
12 reseq2 S = exp S = exp
13 12 feq1d S = exp S : S S exp : S S
14 11 13 mpbird S = exp S : S S
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 S = S = exp : S S exp :
25 24 anidms S = exp : S S exp :
26 23 25 mpbiri S = exp : S S
27 reseq2 S = exp S = exp
28 27 feq1d S = exp S : S S exp : S S
29 26 28 mpbird S = exp S : S S
30 14 29 jaoi S = S = exp S : S S
31 1 2 30 3syl φ exp S : S S