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 = ( 𝑡 ∈ V ↦ ( 𝑣 ∈ ( mUV ‘ 𝑡 ) ↦ ⟨ ( ( mSyn ‘ 𝑡 ) ‘ ( 1st ‘ 𝑣 ) ) , ( 2nd ‘ 𝑣 ) ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cusyn	⊢ mUSyn
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		vv	⊢ 𝑣
4		cmuv	⊢ mUV
5	1	cv	⊢ 𝑡
6	5 4	cfv	⊢ ( mUV ‘ 𝑡 )
7		cmsy	⊢ mSyn
8	5 7	cfv	⊢ ( mSyn ‘ 𝑡 )
9		c1st	⊢ 1st
10	3	cv	⊢ 𝑣
11	10 9	cfv	⊢ ( 1st ‘ 𝑣 )
12	11 8	cfv	⊢ ( ( mSyn ‘ 𝑡 ) ‘ ( 1st ‘ 𝑣 ) )
13		c2nd	⊢ 2nd
14	10 13	cfv	⊢ ( 2nd ‘ 𝑣 )
15	12 14	cop	⊢ ⟨ ( ( mSyn ‘ 𝑡 ) ‘ ( 1st ‘ 𝑣 ) ) , ( 2nd ‘ 𝑣 ) ⟩
16	3 6 15	cmpt	⊢ ( 𝑣 ∈ ( mUV ‘ 𝑡 ) ↦ ⟨ ( ( mSyn ‘ 𝑡 ) ‘ ( 1st ‘ 𝑣 ) ) , ( 2nd ‘ 𝑣 ) ⟩ )
17	1 2 16	cmpt	⊢ ( 𝑡 ∈ V ↦ ( 𝑣 ∈ ( mUV ‘ 𝑡 ) ↦ ⟨ ( ( mSyn ‘ 𝑡 ) ‘ ( 1st ‘ 𝑣 ) ) , ( 2nd ‘ 𝑣 ) ⟩ ) )
18	0 17	wceq	⊢ mUSyn = ( 𝑡 ∈ V ↦ ( 𝑣 ∈ ( mUV ‘ 𝑡 ) ↦ ⟨ ( ( mSyn ‘ 𝑡 ) ‘ ( 1st ‘ 𝑣 ) ) , ( 2nd ‘ 𝑣 ) ⟩ ) )