Metamath Proof Explorer


Theorem mstaval

Description: Value of the set of statements. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mstaval.r
|- R = ( mStRed ` T )
mstaval.s
|- S = ( mStat ` T )
Assertion mstaval
|- S = ran R

Proof

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