Definition df-musyn

Description: Define the syntax typecode function for the model universe. (Contributed by Mario Carneiro, 14-Jul-2016)

	Ref	Expression
Assertion	df-musyn	$$⊢\mathrm{mUSyn}=\left(t\in \mathrm{V}⟼\left(v\in \mathrm{mUV}\left(t\right)⟼⟨\mathrm{mSyn}\left(t\right)\left(1^{st}\left(v\right)\right),2^{nd}\left(v\right)⟩\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cusyn	$$class\mathrm{mUSyn}$$
1		vt	$$setvart$$
2		cvv	$$class\mathrm{V}$$
3		vv	$$setvarv$$
4		cmuv	$$class\mathrm{mUV}$$
5	1	cv	$$setvart$$
6	5 4	cfv	$$class\mathrm{mUV}\left(t\right)$$
7		cmsy	$$class\mathrm{mSyn}$$
8	5 7	cfv	$$class\mathrm{mSyn}\left(t\right)$$
9		c1st	$$class{1}^{st}$$
10	3	cv	$$setvarv$$
11	10 9	cfv	$$class{1}^{st}\left(v\right)$$
12	11 8	cfv	$$class\mathrm{mSyn}\left(t\right)\left(1^{st}\left(v\right)\right)$$
13		c2nd	$$class{2}^{nd}$$
14	10 13	cfv	$$class{2}^{nd}\left(v\right)$$
15	12 14	cop	$$class⟨\mathrm{mSyn}\left(t\right)\left(1^{st}\left(v\right)\right),2^{nd}\left(v\right)⟩$$
16	3 6 15	cmpt	$$class\left(v\in \mathrm{mUV}\left(t\right)⟼⟨\mathrm{mSyn}\left(t\right)\left(1^{st}\left(v\right)\right),2^{nd}\left(v\right)⟩\right)$$
17	1 2 16	cmpt	$$class\left(t\in \mathrm{V}⟼\left(v\in \mathrm{mUV}\left(t\right)⟼⟨\mathrm{mSyn}\left(t\right)\left(1^{st}\left(v\right)\right),2^{nd}\left(v\right)⟩\right)\right)$$
18	0 17	wceq	$$wff\mathrm{mUSyn}=\left(t\in \mathrm{V}⟼\left(v\in \mathrm{mUV}\left(t\right)⟼⟨\mathrm{mSyn}\left(t\right)\left(1^{st}\left(v\right)\right),2^{nd}\left(v\right)⟩\right)\right)$$