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 
|- ( ph -> S e. { RR , CC } )
Assertion seff 
|- ( ph -> ( exp |` S ) : S --> S )

Proof

Step Hyp Ref Expression
1 seff.s 
 |-  ( ph -> S e. { RR , CC } )
2 elpri 
 |-  ( S e. { RR , CC } -> ( S = RR \/ S = CC ) )
3 reeff1 
 |-  ( exp |` RR ) : RR -1-1-> RR+
4 f1f 
 |-  ( ( exp |` RR ) : RR -1-1-> RR+ -> ( exp |` RR ) : RR --> RR+ )
5 rpssre 
 |-  RR+ C_ RR
6 fss 
 |-  ( ( ( exp |` RR ) : RR --> RR+ /\ RR+ C_ RR ) -> ( exp |` RR ) : RR --> RR )
7 5 6 mpan2 
 |-  ( ( exp |` RR ) : RR --> RR+ -> ( exp |` RR ) : RR --> RR )
8 3 4 7 mp2b 
 |-  ( exp |` RR ) : RR --> RR
9 feq23 
 |-  ( ( S = RR /\ S = RR ) -> ( ( exp |` RR ) : S --> S <-> ( exp |` RR ) : RR --> RR ) )
10 9 anidms 
 |-  ( S = RR -> ( ( exp |` RR ) : S --> S <-> ( exp |` RR ) : RR --> RR ) )
11 8 10 mpbiri 
 |-  ( S = RR -> ( exp |` RR ) : S --> S )
12 reseq2 
 |-  ( S = RR -> ( exp |` S ) = ( exp |` RR ) )
13 12 feq1d 
 |-  ( S = RR -> ( ( exp |` S ) : S --> S <-> ( exp |` RR ) : S --> S ) )
14 11 13 mpbird 
 |-  ( S = RR -> ( exp |` S ) : S --> S )
15 eff 
 |-  exp : CC --> CC
16 frel 
 |-  ( exp : CC --> CC -> Rel exp )
17 resdm 
 |-  ( Rel exp -> ( exp |` dom exp ) = exp )
18 15 16 17 mp2b 
 |-  ( exp |` dom exp ) = exp
19 15 fdmi 
 |-  dom exp = CC
20 19 reseq2i 
 |-  ( exp |` dom exp ) = ( exp |` CC )
21 18 20 eqtr3i 
 |-  exp = ( exp |` CC )
22 21 feq1i 
 |-  ( exp : CC --> CC <-> ( exp |` CC ) : CC --> CC )
23 15 22 mpbi 
 |-  ( exp |` CC ) : CC --> CC
24 feq23 
 |-  ( ( S = CC /\ S = CC ) -> ( ( exp |` CC ) : S --> S <-> ( exp |` CC ) : CC --> CC ) )
25 24 anidms 
 |-  ( S = CC -> ( ( exp |` CC ) : S --> S <-> ( exp |` CC ) : CC --> CC ) )
26 23 25 mpbiri 
 |-  ( S = CC -> ( exp |` CC ) : S --> S )
27 reseq2 
 |-  ( S = CC -> ( exp |` S ) = ( exp |` CC ) )
28 27 feq1d 
 |-  ( S = CC -> ( ( exp |` S ) : S --> S <-> ( exp |` CC ) : S --> S ) )
29 26 28 mpbird 
 |-  ( S = CC -> ( exp |` S ) : S --> S )
30 14 29 jaoi 
 |-  ( ( S = RR \/ S = CC ) -> ( exp |` S ) : S --> S )
31 1 2 30 3syl 
 |-  ( ph -> ( exp |` S ) : S --> S )