Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mitp Structured version   Visualization version   GIF version

Definition df-mitp 33158
Description: Define the interpretation function for a model. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mitp mItp = (𝑡 ∈ V ↦ (𝑎 ∈ (mSA‘𝑡) ↦ (𝑔X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) ↦ (℩𝑥𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎))))))
Distinct variable group:   𝑔,𝑎,𝑖,𝑚,𝑡,𝑥

Detailed syntax breakdown of Definition df-mitp
StepHypRef Expression
1 cmitp 33147 . 2 class mItp
2 vt . . 3 setvar 𝑡
3 cvv 3398 . . 3 class V
4 va . . . 4 setvar 𝑎
52cv 1541 . . . . 5 class 𝑡
6 cmsa 33119 . . . . 5 class mSA
75, 6cfv 6339 . . . 4 class (mSA‘𝑡)
8 vg . . . . 5 setvar 𝑔
9 vi . . . . . 6 setvar 𝑖
104cv 1541 . . . . . . 7 class 𝑎
11 cmvrs 33002 . . . . . . . 8 class mVars
125, 11cfv 6339 . . . . . . 7 class (mVars‘𝑡)
1310, 12cfv 6339 . . . . . 6 class ((mVars‘𝑡)‘𝑎)
14 cmuv 33138 . . . . . . . 8 class mUV
155, 14cfv 6339 . . . . . . 7 class (mUV‘𝑡)
169cv 1541 . . . . . . . . 9 class 𝑖
17 cmty 32995 . . . . . . . . . 10 class mType
185, 17cfv 6339 . . . . . . . . 9 class (mType‘𝑡)
1916, 18cfv 6339 . . . . . . . 8 class ((mType‘𝑡)‘𝑖)
2019csn 4516 . . . . . . 7 class {((mType‘𝑡)‘𝑖)}
2115, 20cima 5528 . . . . . 6 class ((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)})
229, 13, 21cixp 8507 . . . . 5 class X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)})
238cv 1541 . . . . . . . . 9 class 𝑔
24 vm . . . . . . . . . . 11 setvar 𝑚
2524cv 1541 . . . . . . . . . 10 class 𝑚
2625, 13cres 5527 . . . . . . . . 9 class (𝑚 ↾ ((mVars‘𝑡)‘𝑎))
2723, 26wceq 1542 . . . . . . . 8 wff 𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎))
28 vx . . . . . . . . . 10 setvar 𝑥
2928cv 1541 . . . . . . . . 9 class 𝑥
30 cmevl 33143 . . . . . . . . . . 11 class mEval
315, 30cfv 6339 . . . . . . . . . 10 class (mEval‘𝑡)
3225, 10, 31co 7170 . . . . . . . . 9 class (𝑚(mEval‘𝑡)𝑎)
3329, 32wceq 1542 . . . . . . . 8 wff 𝑥 = (𝑚(mEval‘𝑡)𝑎)
3427, 33wa 399 . . . . . . 7 wff (𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎))
35 cmvl 33139 . . . . . . . 8 class mVL
365, 35cfv 6339 . . . . . . 7 class (mVL‘𝑡)
3734, 24, 36wrex 3054 . . . . . 6 wff 𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎))
3837, 28cio 6295 . . . . 5 class (℩𝑥𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎)))
398, 22, 38cmpt 5110 . . . 4 class (𝑔X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) ↦ (℩𝑥𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎))))
404, 7, 39cmpt 5110 . . 3 class (𝑎 ∈ (mSA‘𝑡) ↦ (𝑔X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) ↦ (℩𝑥𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎)))))
412, 3, 40cmpt 5110 . 2 class (𝑡 ∈ V ↦ (𝑎 ∈ (mSA‘𝑡) ↦ (𝑔X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) ↦ (℩𝑥𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎))))))
421, 41wceq 1542 1 wff mItp = (𝑡 ∈ V ↦ (𝑎 ∈ (mSA‘𝑡) ↦ (𝑔X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) ↦ (℩𝑥𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎))))))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator