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	eqtrid	|- ( -. 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