Definition df-msax

Description: Define the indexing set for a syntax axiom's representation in a tree. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-msax	⊢ mSAX = ( 𝑡 ∈ V ↦ ( 𝑝 ∈ ( mSA ‘ 𝑡 ) ↦ ( ( mVH ‘ 𝑡 ) “ ( ( mVars ‘ 𝑡 ) ‘ 𝑝 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmsax	⊢ mSAX
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		vp	⊢ 𝑝
4		cmsa	⊢ mSA
5	1	cv	⊢ 𝑡
6	5 4	cfv	⊢ ( mSA ‘ 𝑡 )
7		cmvh	⊢ mVH
8	5 7	cfv	⊢ ( mVH ‘ 𝑡 )
9		cmvrs	⊢ mVars
10	5 9	cfv	⊢ ( mVars ‘ 𝑡 )
11	3	cv	⊢ 𝑝
12	11 10	cfv	⊢ ( ( mVars ‘ 𝑡 ) ‘ 𝑝 )
13	8 12	cima	⊢ ( ( mVH ‘ 𝑡 ) “ ( ( mVars ‘ 𝑡 ) ‘ 𝑝 ) )
14	3 6 13	cmpt	⊢ ( 𝑝 ∈ ( mSA ‘ 𝑡 ) ↦ ( ( mVH ‘ 𝑡 ) “ ( ( mVars ‘ 𝑡 ) ‘ 𝑝 ) ) )
15	1 2 14	cmpt	⊢ ( 𝑡 ∈ V ↦ ( 𝑝 ∈ ( mSA ‘ 𝑡 ) ↦ ( ( mVH ‘ 𝑡 ) “ ( ( mVars ‘ 𝑡 ) ‘ 𝑝 ) ) ) )
16	0 15	wceq	⊢ mSAX = ( 𝑡 ∈ V ↦ ( 𝑝 ∈ ( mSA ‘ 𝑡 ) ↦ ( ( mVH ‘ 𝑡 ) “ ( ( mVars ‘ 𝑡 ) ‘ 𝑝 ) ) ) )