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 = ( t e. _V |-> ( p e. ( mSA ` t ) |-> ( ( mVH ` t ) " ( ( mVars ` t ) ` p ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmsax	|- mSAX
1		vt	|- t
2		cvv	|- _V
3		vp	|- p
4		cmsa	|- mSA
5	1	cv	|- t
6	5 4	cfv	|- ( mSA ` t )
7		cmvh	|- mVH
8	5 7	cfv	|- ( mVH ` t )
9		cmvrs	|- mVars
10	5 9	cfv	|- ( mVars ` t )
11	3	cv	|- p
12	11 10	cfv	|- ( ( mVars ` t ) ` p )
13	8 12	cima	|- ( ( mVH ` t ) " ( ( mVars ` t ) ` p ) )
14	3 6 13	cmpt	|- ( p e. ( mSA ` t ) |-> ( ( mVH ` t ) " ( ( mVars ` t ) ` p ) ) )
15	1 2 14	cmpt	|- ( t e. _V |-> ( p e. ( mSA ` t ) |-> ( ( mVH ` t ) " ( ( mVars ` t ) ` p ) ) ) )
16	0 15	wceq	|- mSAX = ( t e. _V |-> ( p e. ( mSA ` t ) |-> ( ( mVH ` t ) " ( ( mVars ` t ) ` p ) ) ) )