Definition df-mesyn 33540

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

Assertion

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

Distinct variable group:   𝑒,𝑐,𝑡

Detailed syntax breakdown of Definition df-mesyn

Step	Hyp	Ref	Expression
1		cmesy 33530	. 2 class mESyn
2		vt	. . 3 setvar 𝑡
3		cvv 3430	. . 3 class V
4		vc	. . . 4 setvar 𝑐
5		ve	. . . 4 setvar 𝑒
6	2	cv 1540	. . . . 5 class 𝑡
7		cmtc 33405	. . . . 5 class mTC
8	6, 7	cfv 6430	. . . 4 class (mTC‘𝑡)
9		cmrex 33407	. . . . 5 class mREx
10	6, 9	cfv 6430	. . . 4 class (mREx‘𝑡)
11	4	cv 1540	. . . . . 6 class 𝑐
12		cmsy 33529	. . . . . . 7 class mSyn
13	6, 12	cfv 6430	. . . . . 6 class (mSyn‘𝑡)
14	11, 13	cfv 6430	. . . . 5 class ((mSyn‘𝑡)‘𝑐)
15	5	cv 1540	. . . . 5 class 𝑒
16		cm0s 33526	. . . . 5 class m0St
17	14, 15, 16	co 7268	. . . 4 class (((mSyn‘𝑡)‘𝑐)m0St𝑒)
18	4, 5, 8, 10, 17	cmpo 7270	. . 3 class (𝑐 ∈ (mTC‘𝑡), 𝑒 ∈ (mREx‘𝑡) ↦ (((mSyn‘𝑡)‘𝑐)m0St𝑒))
19	2, 3, 18	cmpt 5161	. 2 class (𝑡 ∈ V ↦ (𝑐 ∈ (mTC‘𝑡), 𝑒 ∈ (mREx‘𝑡) ↦ (((mSyn‘𝑡)‘𝑐)m0St𝑒)))
20	1, 19	wceq 1541	1 wff mESyn = (𝑡 ∈ V ↦ (𝑐 ∈ (mTC‘𝑡), 𝑒 ∈ (mREx‘𝑡) ↦ (((mSyn‘𝑡)‘𝑐)m0St𝑒)))

This definition is referenced by: (None)