Definition df-mitp 32876

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

Step	Hyp	Ref	Expression
1		cmitp 32865	. 2 class mItp
2		vt	. . 3 setvar 𝑡
3		cvv 3497	. . 3 class V
4		va	. . . 4 setvar 𝑎
5	2	cv 1535	. . . . 5 class 𝑡
6		cmsa 32837	. . . . 5 class mSA
7	5, 6	cfv 6358	. . . 4 class (mSA‘𝑡)
8		vg	. . . . 5 setvar 𝑔
9		vi	. . . . . 6 setvar 𝑖
10	4	cv 1535	. . . . . . 7 class 𝑎
11		cmvrs 32720	. . . . . . . 8 class mVars
12	5, 11	cfv 6358	. . . . . . 7 class (mVars‘𝑡)
13	10, 12	cfv 6358	. . . . . 6 class ((mVars‘𝑡)‘𝑎)
14		cmuv 32856	. . . . . . . 8 class mUV
15	5, 14	cfv 6358	. . . . . . 7 class (mUV‘𝑡)
16	9	cv 1535	. . . . . . . . 9 class 𝑖
17		cmty 32713	. . . . . . . . . 10 class mType
18	5, 17	cfv 6358	. . . . . . . . 9 class (mType‘𝑡)
19	16, 18	cfv 6358	. . . . . . . 8 class ((mType‘𝑡)‘𝑖)
20	19	csn 4570	. . . . . . 7 class {((mType‘𝑡)‘𝑖)}
21	15, 20	cima 5561	. . . . . 6 class ((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)})
22	9, 13, 21	cixp 8464	. . . . 5 class X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)})
23	8	cv 1535	. . . . . . . . 9 class 𝑔
24		vm	. . . . . . . . . . 11 setvar 𝑚
25	24	cv 1535	. . . . . . . . . 10 class 𝑚
26	25, 13	cres 5560	. . . . . . . . 9 class (𝑚 ↾ ((mVars‘𝑡)‘𝑎))
27	23, 26	wceq 1536	. . . . . . . 8 wff 𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎))
28		vx	. . . . . . . . . 10 setvar 𝑥
29	28	cv 1535	. . . . . . . . 9 class 𝑥
30		cmevl 32861	. . . . . . . . . . 11 class mEval
31	5, 30	cfv 6358	. . . . . . . . . 10 class (mEval‘𝑡)
32	25, 10, 31	co 7159	. . . . . . . . 9 class (𝑚(mEval‘𝑡)𝑎)
33	29, 32	wceq 1536	. . . . . . . 8 wff 𝑥 = (𝑚(mEval‘𝑡)𝑎)
34	27, 33	wa 398	. . . . . . 7 wff (𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎))
35		cmvl 32857	. . . . . . . 8 class mVL
36	5, 35	cfv 6358	. . . . . . 7 class (mVL‘𝑡)
37	34, 24, 36	wrex 3142	. . . . . 6 wff ∃𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎))
38	37, 28	cio 6315	. . . . 5 class (℩𝑥∃𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎)))
39	8, 22, 38	cmpt 5149	. . . 4 class (𝑔 ∈ X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) ↦ (℩𝑥∃𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎))))
40	4, 7, 39	cmpt 5149	. . 3 class (𝑎 ∈ (mSA‘𝑡) ↦ (𝑔 ∈ X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) ↦ (℩𝑥∃𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎)))))
41	2, 3, 40	cmpt 5149	. 2 class (𝑡 ∈ V ↦ (𝑎 ∈ (mSA‘𝑡) ↦ (𝑔 ∈ X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) ↦ (℩𝑥∃𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎))))))
42	1, 41	wceq 1536	1 wff mItp = (𝑡 ∈ V ↦ (𝑎 ∈ (mSA‘𝑡) ↦ (𝑔 ∈ X𝑖 ∈ ((mVars‘𝑡)‘𝑎)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑖)}) ↦ (℩𝑥∃𝑚 ∈ (mVL‘𝑡)(𝑔 = (𝑚 ↾ ((mVars‘𝑡)‘𝑎)) ∧ 𝑥 = (𝑚(mEval‘𝑡)𝑎))))))

This definition is referenced by: (None)