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	$$⊢\mathrm{mST}=\left(t\in \mathrm{V}⟼{\left(\varnothing \mathrm{mTree}\left(t\right)\varnothing \right)\upharpoonright }_{\left({\mathrm{mEx}\left(t\right)\upharpoonright }_{\mathrm{mVT}\left(t\right)}\right)}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmst	$$class\mathrm{mST}$$
1		vt	$$setvart$$
2		cvv	$$class\mathrm{V}$$
3		c0	$$class\varnothing$$
4		cmtree	$$class\mathrm{mTree}$$
5	1	cv	$$setvart$$
6	5 4	cfv	$$class\mathrm{mTree}\left(t\right)$$
7	3 3 6	co	$$class\left(\varnothing \mathrm{mTree}\left(t\right)\varnothing \right)$$
8		cmex	$$class\mathrm{mEx}$$
9	5 8	cfv	$$class\mathrm{mEx}\left(t\right)$$
10		cmvt	$$class\mathrm{mVT}$$
11	5 10	cfv	$$class\mathrm{mVT}\left(t\right)$$
12	9 11	cres	$$class\left({\mathrm{mEx}\left(t\right)\upharpoonright }_{\mathrm{mVT}\left(t\right)}\right)$$
13	7 12	cres	$$class\left({\left(\varnothing \mathrm{mTree}\left(t\right)\varnothing \right)\upharpoonright }_{\left({\mathrm{mEx}\left(t\right)\upharpoonright }_{\mathrm{mVT}\left(t\right)}\right)}\right)$$
14	1 2 13	cmpt	$$class\left(t\in \mathrm{V}⟼{\left(\varnothing \mathrm{mTree}\left(t\right)\varnothing \right)\upharpoonright }_{\left({\mathrm{mEx}\left(t\right)\upharpoonright }_{\mathrm{mVT}\left(t\right)}\right)}\right)$$
15	0 14	wceq	$$wff\mathrm{mST}=\left(t\in \mathrm{V}⟼{\left(\varnothing \mathrm{mTree}\left(t\right)\varnothing \right)\upharpoonright }_{\left({\mathrm{mEx}\left(t\right)\upharpoonright }_{\mathrm{mVT}\left(t\right)}\right)}\right)$$