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 V ran mStRed t
7 1 fvexi R V
8 7 rnex ran R V
9 5 6 8 fvmpt T V mStat T = ran R
10 rn0 ran =
11 10 eqcomi = ran
12 fvprc ¬ T V mStat T =
13 fvprc ¬ T V mStRed T =
14 1 13 syl5eq ¬ T V R =
15 14 rneqd ¬ T V ran R = ran
16 11 12 15 3eqtr4a ¬ T V mStat T = ran R
17 9 16 pm2.61i mStat T = ran R
18 2 17 eqtri S = ran R