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 = ( t e. _V |-> ( ( (/) ( mTree ` t ) (/) ) |` ( ( mEx ` t ) |` ( mVT ` t ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmst	|- mST
1		vt	|- t
2		cvv	|- _V
3		c0	|- (/)
4		cmtree	|- mTree
5	1	cv	|- t
6	5 4	cfv	|- ( mTree ` t )
7	3 3 6	co	|- ( (/) ( mTree ` t ) (/) )
8		cmex	|- mEx
9	5 8	cfv	|- ( mEx ` t )
10		cmvt	|- mVT
11	5 10	cfv	|- ( mVT ` t )
12	9 11	cres	|- ( ( mEx ` t ) |` ( mVT ` t ) )
13	7 12	cres	|- ( ( (/) ( mTree ` t ) (/) ) |` ( ( mEx ` t ) |` ( mVT ` t ) ) )
14	1 2 13	cmpt	|- ( t e. _V |-> ( ( (/) ( mTree ` t ) (/) ) |` ( ( mEx ` t ) |` ( mVT ` t ) ) ) )
15	0 14	wceq	|- mST = ( t e. _V |-> ( ( (/) ( mTree ` t ) (/) ) |` ( ( mEx ` t ) |` ( mVT ` t ) ) ) )