Definition df-mitp

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

	Ref	Expression
Assertion	df-mitp	⊢ mItp = ( 𝑡 ∈ V ↦ ( 𝑎 ∈ ( mSA ‘ 𝑡 ) ↦ ( 𝑔 ∈ X 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } ) ↦ ( ℩ 𝑥 ∃ 𝑚 ∈ ( mVL ‘ 𝑡 ) ( 𝑔 = ( 𝑚 ↾ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ) ∧ 𝑥 = ( 𝑚 ( mEval ‘ 𝑡 ) 𝑎 ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmitp	⊢ mItp
1		vt	⊢ 𝑡
2		cvv	⊢ V
3		va	⊢ 𝑎
4		cmsa	⊢ mSA
5	1	cv	⊢ 𝑡
6	5 4	cfv	⊢ ( mSA ‘ 𝑡 )
7		vg	⊢ 𝑔
8		vi	⊢ 𝑖
9		cmvrs	⊢ mVars
10	5 9	cfv	⊢ ( mVars ‘ 𝑡 )
11	3	cv	⊢ 𝑎
12	11 10	cfv	⊢ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 )
13		cmuv	⊢ mUV
14	5 13	cfv	⊢ ( mUV ‘ 𝑡 )
15		cmty	⊢ mType
16	5 15	cfv	⊢ ( mType ‘ 𝑡 )
17	8	cv	⊢ 𝑖
18	17 16	cfv	⊢ ( ( mType ‘ 𝑡 ) ‘ 𝑖 )
19	18	csn	⊢ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) }
20	14 19	cima	⊢ ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } )
21	8 12 20	cixp	⊢ X 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } )
22		vx	⊢ 𝑥
23		vm	⊢ 𝑚
24		cmvl	⊢ mVL
25	5 24	cfv	⊢ ( mVL ‘ 𝑡 )
26	7	cv	⊢ 𝑔
27	23	cv	⊢ 𝑚
28	27 12	cres	⊢ ( 𝑚 ↾ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) )
29	26 28	wceq	⊢ 𝑔 = ( 𝑚 ↾ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) )
30	22	cv	⊢ 𝑥
31		cmevl	⊢ mEval
32	5 31	cfv	⊢ ( mEval ‘ 𝑡 )
33	27 11 32	co	⊢ ( 𝑚 ( mEval ‘ 𝑡 ) 𝑎 )
34	30 33	wceq	⊢ 𝑥 = ( 𝑚 ( mEval ‘ 𝑡 ) 𝑎 )
35	29 34	wa	⊢ ( 𝑔 = ( 𝑚 ↾ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ) ∧ 𝑥 = ( 𝑚 ( mEval ‘ 𝑡 ) 𝑎 ) )
36	35 23 25	wrex	⊢ ∃ 𝑚 ∈ ( mVL ‘ 𝑡 ) ( 𝑔 = ( 𝑚 ↾ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ) ∧ 𝑥 = ( 𝑚 ( mEval ‘ 𝑡 ) 𝑎 ) )
37	36 22	cio	⊢ ( ℩ 𝑥 ∃ 𝑚 ∈ ( mVL ‘ 𝑡 ) ( 𝑔 = ( 𝑚 ↾ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ) ∧ 𝑥 = ( 𝑚 ( mEval ‘ 𝑡 ) 𝑎 ) ) )
38	7 21 37	cmpt	⊢ ( 𝑔 ∈ X 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } ) ↦ ( ℩ 𝑥 ∃ 𝑚 ∈ ( mVL ‘ 𝑡 ) ( 𝑔 = ( 𝑚 ↾ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ) ∧ 𝑥 = ( 𝑚 ( mEval ‘ 𝑡 ) 𝑎 ) ) ) )
39	3 6 38	cmpt	⊢ ( 𝑎 ∈ ( mSA ‘ 𝑡 ) ↦ ( 𝑔 ∈ X 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } ) ↦ ( ℩ 𝑥 ∃ 𝑚 ∈ ( mVL ‘ 𝑡 ) ( 𝑔 = ( 𝑚 ↾ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ) ∧ 𝑥 = ( 𝑚 ( mEval ‘ 𝑡 ) 𝑎 ) ) ) ) )
40	1 2 39	cmpt	⊢ ( 𝑡 ∈ V ↦ ( 𝑎 ∈ ( mSA ‘ 𝑡 ) ↦ ( 𝑔 ∈ X 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } ) ↦ ( ℩ 𝑥 ∃ 𝑚 ∈ ( mVL ‘ 𝑡 ) ( 𝑔 = ( 𝑚 ↾ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ) ∧ 𝑥 = ( 𝑚 ( mEval ‘ 𝑡 ) 𝑎 ) ) ) ) ) )
41	0 40	wceq	⊢ mItp = ( 𝑡 ∈ V ↦ ( 𝑎 ∈ ( mSA ‘ 𝑡 ) ↦ ( 𝑔 ∈ X 𝑖 ∈ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ( ( mUV ‘ 𝑡 ) “ { ( ( mType ‘ 𝑡 ) ‘ 𝑖 ) } ) ↦ ( ℩ 𝑥 ∃ 𝑚 ∈ ( mVL ‘ 𝑡 ) ( 𝑔 = ( 𝑚 ↾ ( ( mVars ‘ 𝑡 ) ‘ 𝑎 ) ) ∧ 𝑥 = ( 𝑚 ( mEval ‘ 𝑡 ) 𝑎 ) ) ) ) ) )