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 ∈ V ⟼ v ∈ mUV ⁡ t ⟼ mSyn ⁡ t ⁡ 1 st ⁡ v 2 nd ⁡ v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cusyn class mUSyn
1 vt setvar t
2 cvv class V
3 vv setvar v
4 cmuv class mUV
5 1 cv setvar t
6 5 4 cfv class mUV ⁡ t
7 cmsy class mSyn
8 5 7 cfv class mSyn ⁡ t
9 c1st class 1 st
10 3 cv setvar v
11 10 9 cfv class 1 st ⁡ v
12 11 8 cfv class mSyn ⁡ t ⁡ 1 st ⁡ v
13 c2nd class 2 nd
14 10 13 cfv class 2 nd ⁡ v
15 12 14 cop class mSyn ⁡ t ⁡ 1 st ⁡ v 2 nd ⁡ v
16 3 6 15 cmpt class v ∈ mUV ⁡ t ⟼ mSyn ⁡ t ⁡ 1 st ⁡ v 2 nd ⁡ v
17 1 2 16 cmpt class t ∈ V ⟼ v ∈ mUV ⁡ t ⟼ mSyn ⁡ t ⁡ 1 st ⁡ v 2 nd ⁡ v
18 0 17 wceq wff mUSyn = t ∈ V ⟼ v ∈ mUV ⁡ t ⟼ mSyn ⁡ t ⁡ 1 st ⁡ v 2 nd ⁡ v