Metamath Proof Explorer

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 
|- mUSyn = ( t e. _V |-> ( v e. ( mUV ` t ) |-> <. ( ( mSyn ` t ) ` ( 1st ` v ) ) , ( 2nd ` v ) >. ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cusyn 
 |-  mUSyn
1 vt 
 |-  t
2 cvv 
 |-  _V
3 vv 
 |-  v
4 cmuv 
 |-  mUV
5 1 cv 
 |-  t
6 5 4 cfv 
 |-  ( mUV ` t )
7 cmsy 
 |-  mSyn
8 5 7 cfv 
 |-  ( mSyn ` t )
9 c1st 
 |-  1st
10 3 cv 
 |-  v
11 10 9 cfv 
 |-  ( 1st ` v )
12 11 8 cfv 
 |-  ( ( mSyn ` t ) ` ( 1st ` v ) )
13 c2nd 
 |-  2nd
14 10 13 cfv 
 |-  ( 2nd ` v )
15 12 14 cop 
 |-  <. ( ( mSyn ` t ) ` ( 1st ` v ) ) , ( 2nd ` v ) >.
16 3 6 15 cmpt 
 |-  ( v e. ( mUV ` t ) |-> <. ( ( mSyn ` t ) ` ( 1st ` v ) ) , ( 2nd ` v ) >. )
17 1 2 16 cmpt 
 |-  ( t e. _V |-> ( v e. ( mUV ` t ) |-> <. ( ( mSyn ` t ) ` ( 1st ` v ) ) , ( 2nd ` v ) >. ) )
18 0 17 wceq 
 |-  mUSyn = ( t e. _V |-> ( v e. ( mUV ` t ) |-> <. ( ( mSyn ` t ) ` ( 1st ` v ) ) , ( 2nd ` v ) >. ) )