Definition df-mesyn

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

	Ref	Expression
Assertion	df-mesyn	⊢ mESyn = ( 𝑡 ∈ V ↦ ( 𝑐 ∈ ( mTC ‘ 𝑡 ) , 𝑒 ∈ ( mREx ‘ 𝑡 ) ↦ ( ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) m0St 𝑒 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmesy	⊢ mESyn
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		vc	⊢ 𝑐
4		cmtc	⊢ mTC
5	1	cv	⊢ 𝑡
6	5 4	cfv	⊢ ( mTC ‘ 𝑡 )
7		ve	⊢ 𝑒
8		cmrex	⊢ mREx
9	5 8	cfv	⊢ ( mREx ‘ 𝑡 )
10		cmsy	⊢ mSyn
11	5 10	cfv	⊢ ( mSyn ‘ 𝑡 )
12	3	cv	⊢ 𝑐
13	12 11	cfv	⊢ ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 )
14		cm0s	⊢ m0St
15	7	cv	⊢ 𝑒
16	13 15 14	co	⊢ ( ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) m0St 𝑒 )
17	3 7 6 9 16	cmpo	⊢ ( 𝑐 ∈ ( mTC ‘ 𝑡 ) , 𝑒 ∈ ( mREx ‘ 𝑡 ) ↦ ( ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) m0St 𝑒 ) )
18	1 2 17	cmpt	⊢ ( 𝑡 ∈ V ↦ ( 𝑐 ∈ ( mTC ‘ 𝑡 ) , 𝑒 ∈ ( mREx ‘ 𝑡 ) ↦ ( ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) m0St 𝑒 ) ) )
19	0 18	wceq	⊢ mESyn = ( 𝑡 ∈ V ↦ ( 𝑐 ∈ ( mTC ‘ 𝑡 ) , 𝑒 ∈ ( mREx ‘ 𝑡 ) ↦ ( ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) m0St 𝑒 ) ) )