Definition df-mst

Description: Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-mst	⊢ mST = ( 𝑡 ∈ V ↦ ( ( ∅ ( mTree ‘ 𝑡 ) ∅ ) ↾ ( ( mEx ‘ 𝑡 ) ↾ ( mVT ‘ 𝑡 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmst	⊢ mST
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		c0	⊢ ∅
4		cmtree	⊢ mTree
5	1	cv	⊢ 𝑡
6	5 4	cfv	⊢ ( mTree ‘ 𝑡 )
7	3 3 6	co	⊢ ( ∅ ( mTree ‘ 𝑡 ) ∅ )
8		cmex	⊢ mEx
9	5 8	cfv	⊢ ( mEx ‘ 𝑡 )
10		cmvt	⊢ mVT
11	5 10	cfv	⊢ ( mVT ‘ 𝑡 )
12	9 11	cres	⊢ ( ( mEx ‘ 𝑡 ) ↾ ( mVT ‘ 𝑡 ) )
13	7 12	cres	⊢ ( ( ∅ ( mTree ‘ 𝑡 ) ∅ ) ↾ ( ( mEx ‘ 𝑡 ) ↾ ( mVT ‘ 𝑡 ) ) )
14	1 2 13	cmpt	⊢ ( 𝑡 ∈ V ↦ ( ( ∅ ( mTree ‘ 𝑡 ) ∅ ) ↾ ( ( mEx ‘ 𝑡 ) ↾ ( mVT ‘ 𝑡 ) ) ) )
15	0 14	wceq	⊢ mST = ( 𝑡 ∈ V ↦ ( ( ∅ ( mTree ‘ 𝑡 ) ∅ ) ↾ ( ( mEx ‘ 𝑡 ) ↾ ( mVT ‘ 𝑡 ) ) ) )