Step |
Hyp |
Ref |
Expression |
1 |
|
i1f0 |
|- ( RR X. { 0 } ) e. dom S.1 |
2 |
|
reex |
|- RR e. _V |
3 |
2
|
a1i |
|- ( T. -> RR e. _V ) |
4 |
|
i1ff |
|- ( ( RR X. { 0 } ) e. dom S.1 -> ( RR X. { 0 } ) : RR --> RR ) |
5 |
1 4
|
mp1i |
|- ( T. -> ( RR X. { 0 } ) : RR --> RR ) |
6 |
|
leid |
|- ( x e. RR -> x <_ x ) |
7 |
6
|
adantl |
|- ( ( T. /\ x e. RR ) -> x <_ x ) |
8 |
3 5 7
|
caofref |
|- ( T. -> ( RR X. { 0 } ) oR <_ ( RR X. { 0 } ) ) |
9 |
|
ax-resscn |
|- RR C_ CC |
10 |
9
|
a1i |
|- ( T. -> RR C_ CC ) |
11 |
5
|
ffnd |
|- ( T. -> ( RR X. { 0 } ) Fn RR ) |
12 |
10 11
|
0pledm |
|- ( T. -> ( 0p oR <_ ( RR X. { 0 } ) <-> ( RR X. { 0 } ) oR <_ ( RR X. { 0 } ) ) ) |
13 |
8 12
|
mpbird |
|- ( T. -> 0p oR <_ ( RR X. { 0 } ) ) |
14 |
13
|
mptru |
|- 0p oR <_ ( RR X. { 0 } ) |
15 |
|
itg2itg1 |
|- ( ( ( RR X. { 0 } ) e. dom S.1 /\ 0p oR <_ ( RR X. { 0 } ) ) -> ( S.2 ` ( RR X. { 0 } ) ) = ( S.1 ` ( RR X. { 0 } ) ) ) |
16 |
1 14 15
|
mp2an |
|- ( S.2 ` ( RR X. { 0 } ) ) = ( S.1 ` ( RR X. { 0 } ) ) |
17 |
|
itg10 |
|- ( S.1 ` ( RR X. { 0 } ) ) = 0 |
18 |
16 17
|
eqtri |
|- ( S.2 ` ( RR X. { 0 } ) ) = 0 |