Theorem mstaval

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

	Ref	Expression
Hypotheses	mstaval.r	$$⊢R=\mathrm{mStRed}\left(T\right)$$
	mstaval.s	$$⊢S=\mathrm{mStat}\left(T\right)$$
Assertion	mstaval	$$⊢S=\mathrm{ran}R$$

Proof

Step	Hyp	Ref	Expression
1		mstaval.r	$$⊢R=\mathrm{mStRed}\left(T\right)$$
2		mstaval.s	$$⊢S=\mathrm{mStat}\left(T\right)$$
3		fveq2	$$⊢t=T\to \mathrm{mStRed}\left(t\right)=\mathrm{mStRed}\left(T\right)$$
4	3 1	eqtr4di	$$⊢t=T\to \mathrm{mStRed}\left(t\right)=R$$
5	4	rneqd	$$⊢t=T\to \mathrm{ran}\mathrm{mStRed}\left(t\right)=\mathrm{ran}R$$
6		df-msta	$$⊢\mathrm{mStat}=\left(t\in \mathrm{V}⟼\mathrm{ran}\mathrm{mStRed}\left(t\right)\right)$$
7	1	fvexi	$$⊢R\in \mathrm{V}$$
8	7	rnex	$$⊢\mathrm{ran}R\in \mathrm{V}$$
9	5 6 8	fvmpt	$$⊢T\in \mathrm{V}\to \mathrm{mStat}\left(T\right)=\mathrm{ran}R$$
10		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
11	10	eqcomi	$$⊢\varnothing =\mathrm{ran}\varnothing$$
12		fvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{mStat}\left(T\right)=\varnothing$$
13		fvprc	$$⊢\neg T\in \mathrm{V}\to \mathrm{mStRed}\left(T\right)=\varnothing$$
14	1 13	syl5eq	$$⊢\neg T\in \mathrm{V}\to R=\varnothing$$
15	14	rneqd	$$⊢\neg T\in \mathrm{V}\to \mathrm{ran}R=\mathrm{ran}\varnothing$$
16	11 12 15	3eqtr4a	$$⊢\neg T\in \mathrm{V}\to \mathrm{mStat}\left(T\right)=\mathrm{ran}R$$
17	9 16	pm2.61i	$$⊢\mathrm{mStat}\left(T\right)=\mathrm{ran}R$$
18	2 17	eqtri	$$⊢S=\mathrm{ran}R$$