Metamath Proof Explorer

Theorem i1f0

Description: The zero function is simple. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion i1f0 
|- ( RR X. { 0 } ) e. dom S.1

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 1 fconst6 
 |-  ( RR X. { 0 } ) : RR --> RR
3 2 a1i 
 |-  ( T. -> ( RR X. { 0 } ) : RR --> RR )
4 snfi 
 |-  { 0 } e. Fin
5 rnxpss 
 |-  ran ( RR X. { 0 } ) C_ { 0 }
6 ssfi 
 |-  ( ( { 0 } e. Fin /\ ran ( RR X. { 0 } ) C_ { 0 } ) -> ran ( RR X. { 0 } ) e. Fin )
7 4 5 6 mp2an 
 |-  ran ( RR X. { 0 } ) e. Fin
8 7 a1i 
 |-  ( T. -> ran ( RR X. { 0 } ) e. Fin )
9 difss 
 |-  ( ran ( RR X. { 0 } ) \ { 0 } ) C_ ran ( RR X. { 0 } )
10 9 5 sstri 
 |-  ( ran ( RR X. { 0 } ) \ { 0 } ) C_ { 0 }
11 10 sseli 
 |-  ( x e. ( ran ( RR X. { 0 } ) \ { 0 } ) -> x e. { 0 } )
12 11 adantl 
 |-  ( ( T. /\ x e. ( ran ( RR X. { 0 } ) \ { 0 } ) ) -> x e. { 0 } )
13 eldifn 
 |-  ( x e. ( ran ( RR X. { 0 } ) \ { 0 } ) -> -. x e. { 0 } )
14 13 adantl 
 |-  ( ( T. /\ x e. ( ran ( RR X. { 0 } ) \ { 0 } ) ) -> -. x e. { 0 } )
15 12 14 pm2.21dd 
 |-  ( ( T. /\ x e. ( ran ( RR X. { 0 } ) \ { 0 } ) ) -> ( `' ( RR X. { 0 } ) " { x } ) e. dom vol )
16 12 14 pm2.21dd 
 |-  ( ( T. /\ x e. ( ran ( RR X. { 0 } ) \ { 0 } ) ) -> ( vol ` ( `' ( RR X. { 0 } ) " { x } ) ) e. RR )
17 3 8 15 16 i1fd 
 |-  ( T. -> ( RR X. { 0 } ) e. dom S.1 )
18 17 mptru 
 |-  ( RR X. { 0 } ) e. dom S.1