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 ⁡ c m0St e

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmesy class mESyn
1 vt setvar t
2 cvv class V
3 vc setvar c
4 cmtc class mTC
5 1 cv setvar t
6 5 4 cfv class mTC ⁡ t
7 ve setvar e
8 cmrex class mREx
9 5 8 cfv class mREx ⁡ t
10 cmsy class mSyn
11 5 10 cfv class mSyn ⁡ t
12 3 cv setvar c
13 12 11 cfv class mSyn ⁡ t ⁡ c
14 cm0s class m0St
15 7 cv setvar e
16 13 15 14 co class mSyn ⁡ t ⁡ c m0St e
17 3 7 6 9 16 cmpo class c ∈ mTC ⁡ t , e ∈ mREx ⁡ t ⟼ mSyn ⁡ t ⁡ c m0St e
18 1 2 17 cmpt class t ∈ V ⟼ c ∈ mTC ⁡ t , e ∈ mREx ⁡ t ⟼ mSyn ⁡ t ⁡ c m0St e
19 0 18 wceq wff mESyn = t ∈ V ⟼ c ∈ mTC ⁡ t , e ∈ mREx ⁡ t ⟼ mSyn ⁡ t ⁡ c m0St e