Definition df-msta

Description: Define the set of all statements. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-msta	⊢ mStat = ( 𝑡 ∈ V ↦ ran ( mStRed ‘ 𝑡 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmsta	⊢ mStat
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		cmsr	⊢ mStRed
4	1	cv	⊢ 𝑡
5	4 3	cfv	⊢ ( mStRed ‘ 𝑡 )
6	5	crn	⊢ ran ( mStRed ‘ 𝑡 )
7	1 2 6	cmpt	⊢ ( 𝑡 ∈ V ↦ ran ( mStRed ‘ 𝑡 ) )
8	0 7	wceq	⊢ mStat = ( 𝑡 ∈ V ↦ ran ( mStRed ‘ 𝑡 ) )