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 ⁡ a mUV ⁡ t mType ⁡ t ⁡ i ⟼ ι x | ∃ m ∈ mVL ⁡ t g = m ↾ mVars ⁡ t ⁡ a ∧ x = m mEval ⁡ t a

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmitp class mItp
1 vt setvar t
2 cvv class V
3 va setvar a
4 cmsa class mSA
5 1 cv setvar t
6 5 4 cfv class mSA ⁡ t
7 vg setvar g
8 vi setvar i
9 cmvrs class mVars
10 5 9 cfv class mVars ⁡ t
11 3 cv setvar a
12 11 10 cfv class mVars ⁡ t ⁡ a
13 cmuv class mUV
14 5 13 cfv class mUV ⁡ t
15 cmty class mType
16 5 15 cfv class mType ⁡ t
17 8 cv setvar i
18 17 16 cfv class mType ⁡ t ⁡ i
19 18 csn class mType ⁡ t ⁡ i
20 14 19 cima class mUV ⁡ t mType ⁡ t ⁡ i
21 8 12 20 cixp class ⨉ i ∈ mVars ⁡ t ⁡ a mUV ⁡ t mType ⁡ t ⁡ i
22 vx setvar x
23 vm setvar m
24 cmvl class mVL
25 5 24 cfv class mVL ⁡ t
26 7 cv setvar g
27 23 cv setvar m
28 27 12 cres class m ↾ mVars ⁡ t ⁡ a
29 26 28 wceq wff g = m ↾ mVars ⁡ t ⁡ a
30 22 cv setvar x
31 cmevl class mEval
32 5 31 cfv class mEval ⁡ t
33 27 11 32 co class m mEval ⁡ t a
34 30 33 wceq wff x = m mEval ⁡ t a
35 29 34 wa wff g = m ↾ mVars ⁡ t ⁡ a ∧ x = m mEval ⁡ t a
36 35 23 25 wrex wff ∃ m ∈ mVL ⁡ t g = m ↾ mVars ⁡ t ⁡ a ∧ x = m mEval ⁡ t a
37 36 22 cio class ι x | ∃ m ∈ mVL ⁡ t g = m ↾ mVars ⁡ t ⁡ a ∧ x = m mEval ⁡ t a
38 7 21 37 cmpt class g ∈ ⨉ i ∈ mVars ⁡ t ⁡ a mUV ⁡ t mType ⁡ t ⁡ i ⟼ ι x | ∃ m ∈ mVL ⁡ t g = m ↾ mVars ⁡ t ⁡ a ∧ x = m mEval ⁡ t a
39 3 6 38 cmpt class a ∈ mSA ⁡ t ⟼ g ∈ ⨉ i ∈ mVars ⁡ t ⁡ a mUV ⁡ t mType ⁡ t ⁡ i ⟼ ι x | ∃ m ∈ mVL ⁡ t g = m ↾ mVars ⁡ t ⁡ a ∧ x = m mEval ⁡ t a
40 1 2 39 cmpt class t ∈ V ⟼ a ∈ mSA ⁡ t ⟼ g ∈ ⨉ i ∈ mVars ⁡ t ⁡ a mUV ⁡ t mType ⁡ t ⁡ i ⟼ ι x | ∃ m ∈ mVL ⁡ t g = m ↾ mVars ⁡ t ⁡ a ∧ x = m mEval ⁡ t a
41 0 40 wceq wff mItp = t ∈ V ⟼ a ∈ mSA ⁡ t ⟼ g ∈ ⨉ i ∈ mVars ⁡ t ⁡ a mUV ⁡ t mType ⁡ t ⁡ i ⟼ ι x | ∃ m ∈ mVL ⁡ t g = m ↾ mVars ⁡ t ⁡ a ∧ x = m mEval ⁡ t a