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

Definition df-msax 32747
Description: Define the indexing set for a syntax axiom's representation in a tree. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-msax mSAX = (𝑡 ∈ V ↦ (𝑝 ∈ (mSA‘𝑡) ↦ ((mVH‘𝑡) “ ((mVars‘𝑡)‘𝑝))))
Distinct variable group:   𝑡,𝑝

Detailed syntax breakdown of Definition df-msax
StepHypRef Expression
1 cmsax 32737 . 2 class mSAX
2 vt . . 3 setvar 𝑡
3 cvv 3492 . . 3 class V
4 vp . . . 4 setvar 𝑝
52cv 1527 . . . . 5 class 𝑡
6 cmsa 32730 . . . . 5 class mSA
75, 6cfv 6348 . . . 4 class (mSA‘𝑡)
8 cmvh 32616 . . . . . 6 class mVH
95, 8cfv 6348 . . . . 5 class (mVH‘𝑡)
104cv 1527 . . . . . 6 class 𝑝
11 cmvrs 32613 . . . . . . 7 class mVars
125, 11cfv 6348 . . . . . 6 class (mVars‘𝑡)
1310, 12cfv 6348 . . . . 5 class ((mVars‘𝑡)‘𝑝)
149, 13cima 5551 . . . 4 class ((mVH‘𝑡) “ ((mVars‘𝑡)‘𝑝))
154, 7, 14cmpt 5137 . . 3 class (𝑝 ∈ (mSA‘𝑡) ↦ ((mVH‘𝑡) “ ((mVars‘𝑡)‘𝑝)))
162, 3, 15cmpt 5137 . 2 class (𝑡 ∈ V ↦ (𝑝 ∈ (mSA‘𝑡) ↦ ((mVH‘𝑡) “ ((mVars‘𝑡)‘𝑝))))
171, 16wceq 1528 1 wff mSAX = (𝑡 ∈ V ↦ (𝑝 ∈ (mSA‘𝑡) ↦ ((mVH‘𝑡) “ ((mVars‘𝑡)‘𝑝))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator