Definition df-musyn 31518

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

Assertion

Ref	Expression
df-musyn	|- mUSyn = ( t e. _V |-> ( v e. (mUV ` t ) |-> <. ( (mSyn ` t ) ` ( 1st ` v ) ) , ( 2nd ` v ) >. ) )

Distinct variable group:   v, t

Detailed syntax breakdown of Definition df-musyn

Step	Hyp	Ref	Expression
1		cusyn 31507	. 2 class mUSyn
2		vt	. . 3 setvar t
3		cvv 3200	. . 3 class _V
4		vv	. . . 4 setvar v
5	2	cv 1482	. . . . 5 class t
6		cmuv 31500	. . . . 5 class mUV
7	5, 6	cfv 5888	. . . 4 class (mUV ` t )
8	4	cv 1482	. . . . . . 7 class v
9		c1st 7166	. . . . . . 7 class 1st
10	8, 9	cfv 5888	. . . . . 6 class ( 1st ` v )
11		cmsy 31485	. . . . . . 7 class mSyn
12	5, 11	cfv 5888	. . . . . 6 class (mSyn ` t )
13	10, 12	cfv 5888	. . . . 5 class ( (mSyn ` t ) ` ( 1st ` v ) )
14		c2nd 7167	. . . . . 6 class 2nd
15	8, 14	cfv 5888	. . . . 5 class ( 2nd ` v )
16	13, 15	cop 4183	. . . 4 class <. ( (mSyn ` t ) ` ( 1st ` v ) ) , ( 2nd ` v ) >.
17	4, 7, 16	cmpt 4729	. . 3 class ( v e. (mUV ` t ) |-> <. ( (mSyn ` t ) ` ( 1st ` v ) ) , ( 2nd ` v ) >. )
18	2, 3, 17	cmpt 4729	. 2 class ( t e. _V |-> ( v e. (mUV ` t ) |-> <. ( (mSyn ` t ) ` ( 1st ` v ) ) , ( 2nd ` v ) >. ) )
19	1, 18	wceq 1483	1 wff mUSyn = ( t e. _V |-> ( v e. (mUV ` t ) |-> <. ( (mSyn ` t ) ` ( 1st ` v ) ) , ( 2nd ` v ) >. ) )

This definition is referenced by: (None)