Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mesyn Structured version   Visualization version   GIF version

Definition df-mesyn 34585
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
StepHypRef Expression
1 cmesy 34575 . 2 class mESyn
2 vt . . 3 setvar 𝑑
3 cvv 3474 . . 3 class V
4 vc . . . 4 setvar 𝑐
5 ve . . . 4 setvar 𝑒
62cv 1540 . . . . 5 class 𝑑
7 cmtc 34450 . . . . 5 class mTC
86, 7cfv 6543 . . . 4 class (mTCβ€˜π‘‘)
9 cmrex 34452 . . . . 5 class mREx
106, 9cfv 6543 . . . 4 class (mRExβ€˜π‘‘)
114cv 1540 . . . . . 6 class 𝑐
12 cmsy 34574 . . . . . . 7 class mSyn
136, 12cfv 6543 . . . . . 6 class (mSynβ€˜π‘‘)
1411, 13cfv 6543 . . . . 5 class ((mSynβ€˜π‘‘)β€˜π‘)
155cv 1540 . . . . 5 class 𝑒
16 cm0s 34571 . . . . 5 class m0St
1714, 15, 16co 7408 . . . 4 class (((mSynβ€˜π‘‘)β€˜π‘)m0St𝑒)
184, 5, 8, 10, 17cmpo 7410 . . 3 class (𝑐 ∈ (mTCβ€˜π‘‘), 𝑒 ∈ (mRExβ€˜π‘‘) ↦ (((mSynβ€˜π‘‘)β€˜π‘)m0St𝑒))
192, 3, 18cmpt 5231 . 2 class (𝑑 ∈ V ↦ (𝑐 ∈ (mTCβ€˜π‘‘), 𝑒 ∈ (mRExβ€˜π‘‘) ↦ (((mSynβ€˜π‘‘)β€˜π‘)m0St𝑒)))
201, 19wceq 1541 1 wff mESyn = (𝑑 ∈ V ↦ (𝑐 ∈ (mTCβ€˜π‘‘), 𝑒 ∈ (mRExβ€˜π‘‘) ↦ (((mSynβ€˜π‘‘)β€˜π‘)m0St𝑒)))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator