Metamath Proof Explorer

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∈V⟼c∈mTC⁡t,e∈mREx⁡t⟼mSyn⁡t⁡cm0Ste

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmesy classmESyn
1 vt setvart
2 cvv classV
3 vc setvarc
4 cmtc classmTC
5 1 cv setvart
6 5 4 cfv classmTC⁡t
7 ve setvare
8 cmrex classmREx
9 5 8 cfv classmREx⁡t
10 cmsy classmSyn
11 5 10 cfv classmSyn⁡t
12 3 cv setvarc
13 12 11 cfv classmSyn⁡t⁡c
14 cm0s classm0St
15 7 cv setvare
16 13 15 14 co classmSyn⁡t⁡cm0Ste
17 3 7 6 9 16 cmpo classc∈mTC⁡t,e∈mREx⁡t⟼mSyn⁡t⁡cm0Ste
18 1 2 17 cmpt classt∈V⟼c∈mTC⁡t,e∈mREx⁡t⟼mSyn⁡t⁡cm0Ste
19 0 18 wceq wffmESyn=t∈V⟼c∈mTC⁡t,e∈mREx⁡t⟼mSyn⁡t⁡cm0Ste