Definition df-msax 32850

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

Step	Hyp	Ref	Expression
1		cmsax 32840	. 2 class mSAX
2		vt	. . 3 setvar 𝑡
3		cvv 3494	. . 3 class V
4		vp	. . . 4 setvar 𝑝
5	2	cv 1536	. . . . 5 class 𝑡
6		cmsa 32833	. . . . 5 class mSA
7	5, 6	cfv 6355	. . . 4 class (mSA‘𝑡)
8		cmvh 32719	. . . . . 6 class mVH
9	5, 8	cfv 6355	. . . . 5 class (mVH‘𝑡)
10	4	cv 1536	. . . . . 6 class 𝑝
11		cmvrs 32716	. . . . . . 7 class mVars
12	5, 11	cfv 6355	. . . . . 6 class (mVars‘𝑡)
13	10, 12	cfv 6355	. . . . 5 class ((mVars‘𝑡)‘𝑝)
14	9, 13	cima 5558	. . . 4 class ((mVH‘𝑡) “ ((mVars‘𝑡)‘𝑝))
15	4, 7, 14	cmpt 5146	. . 3 class (𝑝 ∈ (mSA‘𝑡) ↦ ((mVH‘𝑡) “ ((mVars‘𝑡)‘𝑝)))
16	2, 3, 15	cmpt 5146	. 2 class (𝑡 ∈ V ↦ (𝑝 ∈ (mSA‘𝑡) ↦ ((mVH‘𝑡) “ ((mVars‘𝑡)‘𝑝))))
17	1, 16	wceq 1537	1 wff mSAX = (𝑡 ∈ V ↦ (𝑝 ∈ (mSA‘𝑡) ↦ ((mVH‘𝑡) “ ((mVars‘𝑡)‘𝑝))))

This definition is referenced by: (None)