Step |
Hyp |
Ref |
Expression |
1 |
|
mstaval.r |
|- R = ( mStRed ` T ) |
2 |
|
mstaval.s |
|- S = ( mStat ` T ) |
3 |
|
fveq2 |
|- ( t = T -> ( mStRed ` t ) = ( mStRed ` T ) ) |
4 |
3 1
|
eqtr4di |
|- ( t = T -> ( mStRed ` t ) = R ) |
5 |
4
|
rneqd |
|- ( t = T -> ran ( mStRed ` t ) = ran R ) |
6 |
|
df-msta |
|- mStat = ( t e. _V |-> ran ( mStRed ` t ) ) |
7 |
1
|
fvexi |
|- R e. _V |
8 |
7
|
rnex |
|- ran R e. _V |
9 |
5 6 8
|
fvmpt |
|- ( T e. _V -> ( mStat ` T ) = ran R ) |
10 |
|
rn0 |
|- ran (/) = (/) |
11 |
10
|
eqcomi |
|- (/) = ran (/) |
12 |
|
fvprc |
|- ( -. T e. _V -> ( mStat ` T ) = (/) ) |
13 |
|
fvprc |
|- ( -. T e. _V -> ( mStRed ` T ) = (/) ) |
14 |
1 13
|
syl5eq |
|- ( -. T e. _V -> R = (/) ) |
15 |
14
|
rneqd |
|- ( -. T e. _V -> ran R = ran (/) ) |
16 |
11 12 15
|
3eqtr4a |
|- ( -. T e. _V -> ( mStat ` T ) = ran R ) |
17 |
9 16
|
pm2.61i |
|- ( mStat ` T ) = ran R |
18 |
2 17
|
eqtri |
|- S = ran R |