Theorem mstaval

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

	Ref	Expression
Hypotheses	mstaval.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
	mstaval.s	⊢ 𝑆 = ( mStat ‘ 𝑇 )
Assertion	mstaval	⊢ 𝑆 = ran 𝑅

Proof

Step	Hyp	Ref	Expression
1		mstaval.r	⊢ 𝑅 = ( mStRed ‘ 𝑇 )
2		mstaval.s	⊢ 𝑆 = ( mStat ‘ 𝑇 )
3		fveq2	⊢ ( 𝑡 = 𝑇 → ( mStRed ‘ 𝑡 ) = ( mStRed ‘ 𝑇 ) )
4	3 1	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mStRed ‘ 𝑡 ) = 𝑅 )
5	4	rneqd	⊢ ( 𝑡 = 𝑇 → ran ( mStRed ‘ 𝑡 ) = ran 𝑅 )
6		df-msta	⊢ mStat = ( 𝑡 ∈ V ↦ ran ( mStRed ‘ 𝑡 ) )
7	1	fvexi	⊢ 𝑅 ∈ V
8	7	rnex	⊢ ran 𝑅 ∈ V
9	5 6 8	fvmpt	⊢ ( 𝑇 ∈ V → ( mStat ‘ 𝑇 ) = ran 𝑅 )
10		rn0	⊢ ran ∅ = ∅
11	10	eqcomi	⊢ ∅ = ran ∅
12		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mStat ‘ 𝑇 ) = ∅ )
13		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mStRed ‘ 𝑇 ) = ∅ )
14	1 13	syl5eq	⊢ ( ¬ 𝑇 ∈ V → 𝑅 = ∅ )
15	14	rneqd	⊢ ( ¬ 𝑇 ∈ V → ran 𝑅 = ran ∅ )
16	11 12 15	3eqtr4a	⊢ ( ¬ 𝑇 ∈ V → ( mStat ‘ 𝑇 ) = ran 𝑅 )
17	9 16	pm2.61i	⊢ ( mStat ‘ 𝑇 ) = ran 𝑅
18	2 17	eqtri	⊢ 𝑆 = ran 𝑅