Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mst Structured version   Visualization version   Unicode version
Definition df-mst 31497
Description: Define the function mapping syntax expressions to syntax trees. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mst |- mST = ( t e. _V |-> ( ( (/) (mTree ` t ) (/) ) |` ( (mEx ` t ) |` (mVT ` t ) ) ) )
Detailed syntax breakdown of Definition df-mst
StepHypRef Expression
1 cmst 31489 . 2 class mST
2 vt . . 3 setvar t
3 cvv 3200 . . 3 class _V
4 c0 3915 . . . . 5 class (/)
52cv 1482 . . . . . 6 class t
6 cmtree 31488 . . . . . 6 class mTree
75, 6cfv 5888 . . . . 5 class (mTree ` t )
84, 4, 7co 6650 . . . 4 class ( (/) (mTree ` t ) (/) )
9 cmex 31364 . . . . . 6 class mEx
105, 9cfv 5888 . . . . 5 class (mEx ` t )
11 cmvt 31360 . . . . . 6 class mVT
125, 11cfv 5888 . . . . 5 class (mVT ` t )
1310, 12cres 5116 . . . 4 class ( (mEx ` t ) |` (mVT ` t ) )
148, 13cres 5116 . . 3 class ( ( (/) (mTree ` t ) (/) ) |` ( (mEx ` t ) |` (mVT ` t ) ) )
152, 3, 14cmpt 4729 . 2 class ( t e. _V |-> ( ( (/) (mTree ` t ) (/) ) |` ( (mEx ` t ) |` (mVT ` t ) ) ) )
161, 15wceq 1483 1 wff mST = ( t e. _V |-> ( ( (/) (mTree ` t ) (/) ) |` ( (mEx ` t ) |` (mVT ` t ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator