Metamath Proof Explorer

Definition df-mitp

Description: Define the interpretation function for a model. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mitp ⊢mItp=t∈V⟼a∈mSA⁡t⟼g∈⨉i∈mVars⁡t⁡amUV⁡tmType⁡t⁡i⟼ιx|∃m∈mVL⁡tg=m↾mVars⁡t⁡a∧x=mmEval⁡ta

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmitp classmItp
1 vt setvart
2 cvv classV
3 va setvara
4 cmsa classmSA
5 1 cv setvart
6 5 4 cfv classmSA⁡t
7 vg setvarg
8 vi setvari
9 cmvrs classmVars
10 5 9 cfv classmVars⁡t
11 3 cv setvara
12 11 10 cfv classmVars⁡t⁡a
13 cmuv classmUV
14 5 13 cfv classmUV⁡t
15 cmty classmType
16 5 15 cfv classmType⁡t
17 8 cv setvari
18 17 16 cfv classmType⁡t⁡i
19 18 csn classmType⁡t⁡i
20 14 19 cima classmUV⁡tmType⁡t⁡i
21 8 12 20 cixp class⨉i∈mVars⁡t⁡amUV⁡tmType⁡t⁡i
22 vx setvarx
23 vm setvarm
24 cmvl classmVL
25 5 24 cfv classmVL⁡t
26 7 cv setvarg
27 23 cv setvarm
28 27 12 cres classm↾mVars⁡t⁡a
29 26 28 wceq wffg=m↾mVars⁡t⁡a
30 22 cv setvarx
31 cmevl classmEval
32 5 31 cfv classmEval⁡t
33 27 11 32 co classmmEval⁡ta
34 30 33 wceq wffx=mmEval⁡ta
35 29 34 wa wffg=m↾mVars⁡t⁡a∧x=mmEval⁡ta
36 35 23 25 wrex wff∃m∈mVL⁡tg=m↾mVars⁡t⁡a∧x=mmEval⁡ta
37 36 22 cio classιx|∃m∈mVL⁡tg=m↾mVars⁡t⁡a∧x=mmEval⁡ta
38 7 21 37 cmpt classg∈⨉i∈mVars⁡t⁡amUV⁡tmType⁡t⁡i⟼ιx|∃m∈mVL⁡tg=m↾mVars⁡t⁡a∧x=mmEval⁡ta
39 3 6 38 cmpt classa∈mSA⁡t⟼g∈⨉i∈mVars⁡t⁡amUV⁡tmType⁡t⁡i⟼ιx|∃m∈mVL⁡tg=m↾mVars⁡t⁡a∧x=mmEval⁡ta
40 1 2 39 cmpt classt∈V⟼a∈mSA⁡t⟼g∈⨉i∈mVars⁡t⁡amUV⁡tmType⁡t⁡i⟼ιx|∃m∈mVL⁡tg=m↾mVars⁡t⁡a∧x=mmEval⁡ta
41 0 40 wceq wffmItp=t∈V⟼a∈mSA⁡t⟼g∈⨉i∈mVars⁡t⁡amUV⁡tmType⁡t⁡i⟼ιx|∃m∈mVL⁡tg=m↾mVars⁡t⁡a∧x=mmEval⁡ta