Definition df-mesyn

Description: Define the syntax typecode function for expressions. (Contributed by Mario Carneiro, 12-Jun-2023)

	Ref	Expression
Assertion	df-mesyn	|- mESyn = ( t e. _V |-> ( c e. ( mTC ` t ) , e e. ( mREx ` t ) |-> ( ( ( mSyn ` t ) ` c ) m0St e ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmesy	|- mESyn
1		vt	|- t
2		cvv	|- _V
3		vc	|- c
4		cmtc	|- mTC
5	1	cv	|- t
6	5 4	cfv	|- ( mTC ` t )
7		ve	|- e
8		cmrex	|- mREx
9	5 8	cfv	|- ( mREx ` t )
10		cmsy	|- mSyn
11	5 10	cfv	|- ( mSyn ` t )
12	3	cv	|- c
13	12 11	cfv	|- ( ( mSyn ` t ) ` c )
14		cm0s	|- m0St
15	7	cv	|- e
16	13 15 14	co	|- ( ( ( mSyn ` t ) ` c ) m0St e )
17	3 7 6 9 16	cmpo	|- ( c e. ( mTC ` t ) , e e. ( mREx ` t ) |-> ( ( ( mSyn ` t ) ` c ) m0St e ) )
18	1 2 17	cmpt	|- ( t e. _V |-> ( c e. ( mTC ` t ) , e e. ( mREx ` t ) |-> ( ( ( mSyn ` t ) ` c ) m0St e ) ) )
19	0 18	wceq	|- mESyn = ( t e. _V |-> ( c e. ( mTC ` t ) , e e. ( mREx ` t ) |-> ( ( ( mSyn ` t ) ` c ) m0St e ) ) )