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	$$⊢\mathrm{mSAX}=\left(t\in \mathrm{V}⟼\left(p\in \mathrm{mSA}\left(t\right)⟼\mathrm{mVH}\left(t\right)\left[\mathrm{mVars}\left(t\right)\left(p\right)\right]\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmsax	$$class\mathrm{mSAX}$$
1		vt	$$setvart$$
2		cvv	$$class\mathrm{V}$$
3		vp	$$setvarp$$
4		cmsa	$$class\mathrm{mSA}$$
5	1	cv	$$setvart$$
6	5 4	cfv	$$class\mathrm{mSA}\left(t\right)$$
7		cmvh	$$class\mathrm{mVH}$$
8	5 7	cfv	$$class\mathrm{mVH}\left(t\right)$$
9		cmvrs	$$class\mathrm{mVars}$$
10	5 9	cfv	$$class\mathrm{mVars}\left(t\right)$$
11	3	cv	$$setvarp$$
12	11 10	cfv	$$class\mathrm{mVars}\left(t\right)\left(p\right)$$
13	8 12	cima	$$class\mathrm{mVH}\left(t\right)\left[\mathrm{mVars}\left(t\right)\left(p\right)\right]$$
14	3 6 13	cmpt	$$class\left(p\in \mathrm{mSA}\left(t\right)⟼\mathrm{mVH}\left(t\right)\left[\mathrm{mVars}\left(t\right)\left(p\right)\right]\right)$$
15	1 2 14	cmpt	$$class\left(t\in \mathrm{V}⟼\left(p\in \mathrm{mSA}\left(t\right)⟼\mathrm{mVH}\left(t\right)\left[\mathrm{mVars}\left(t\right)\left(p\right)\right]\right)\right)$$
16	0 15	wceq	$$wff\mathrm{mSAX}=\left(t\in \mathrm{V}⟼\left(p\in \mathrm{mSA}\left(t\right)⟼\mathrm{mVH}\left(t\right)\left[\mathrm{mVars}\left(t\right)\left(p\right)\right]\right)\right)$$