Definition df-gmdl 30773

Description: Define the set of models of a grammatical formal system. (Contributed by Mario Carneiro, 14-Jul-2016.)

Assertion

Ref	Expression
df-gmdl	⊢ mGMdl = {𝑡 ∈ (mGFS ∩ mMdl) ∣ (∀𝑐 ∈ (mTC‘𝑡)((mUV‘𝑡) “ {𝑐}) ⊆ ((mUV‘𝑡) “ {((mSyn‘𝑡)‘𝑐)}) ∧ ∀𝑣 ∈ (mUV‘𝑐)∀𝑤 ∈ (mUV‘𝑐)(𝑣(mFresh‘𝑡)𝑤 ↔ 𝑣(mFresh‘𝑡)((mUSyn‘𝑡)‘𝑤)) ∧ ∀𝑚 ∈ (mVL‘𝑡)∀𝑒 ∈ (mEx‘𝑡)((mEval‘𝑡) “ {⟨𝑚, 𝑒⟩}) = (((mEval‘𝑡) “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st ‘𝑒)})))}

Distinct variable group:   𝑒,𝑐,𝑚,𝑡,𝑣,𝑤

Detailed syntax breakdown of Definition df-gmdl

Step	Hyp	Ref	Expression
1		cgmdl 30762	. 2 class mGMdl
2		vt	. . . . . . . . 9 setvar 𝑡
3	2	cv 1474	. . . . . . . 8 class 𝑡
4		cmuv 30754	. . . . . . . 8 class mUV
5	3, 4	cfv 5804	. . . . . . 7 class (mUV‘𝑡)
6		vc	. . . . . . . . 9 setvar 𝑐
7	6	cv 1474	. . . . . . . 8 class 𝑐
8	7	csn 4125	. . . . . . 7 class {𝑐}
9	5, 8	cima 5041	. . . . . 6 class ((mUV‘𝑡) “ {𝑐})
10		cmsy 30739	. . . . . . . . . 10 class mSyn
11	3, 10	cfv 5804	. . . . . . . . 9 class (mSyn‘𝑡)
12	7, 11	cfv 5804	. . . . . . . 8 class ((mSyn‘𝑡)‘𝑐)
13	12	csn 4125	. . . . . . 7 class {((mSyn‘𝑡)‘𝑐)}
14	5, 13	cima 5041	. . . . . 6 class ((mUV‘𝑡) “ {((mSyn‘𝑡)‘𝑐)})
15	9, 14	wss 3540	. . . . 5 wff ((mUV‘𝑡) “ {𝑐}) ⊆ ((mUV‘𝑡) “ {((mSyn‘𝑡)‘𝑐)})
16		cmtc 30615	. . . . . 6 class mTC
17	3, 16	cfv 5804	. . . . 5 class (mTC‘𝑡)
18	15, 6, 17	wral 2896	. . . 4 wff ∀𝑐 ∈ (mTC‘𝑡)((mUV‘𝑡) “ {𝑐}) ⊆ ((mUV‘𝑡) “ {((mSyn‘𝑡)‘𝑐)})
19		vv	. . . . . . . . 9 setvar 𝑣
20	19	cv 1474	. . . . . . . 8 class 𝑣
21		vw	. . . . . . . . 9 setvar 𝑤
22	21	cv 1474	. . . . . . . 8 class 𝑤
23		cmfsh 30757	. . . . . . . . 9 class mFresh
24	3, 23	cfv 5804	. . . . . . . 8 class (mFresh‘𝑡)
25	20, 22, 24	wbr 4583	. . . . . . 7 wff 𝑣(mFresh‘𝑡)𝑤
26		cusyn 30761	. . . . . . . . . 10 class mUSyn
27	3, 26	cfv 5804	. . . . . . . . 9 class (mUSyn‘𝑡)
28	22, 27	cfv 5804	. . . . . . . 8 class ((mUSyn‘𝑡)‘𝑤)
29	20, 28, 24	wbr 4583	. . . . . . 7 wff 𝑣(mFresh‘𝑡)((mUSyn‘𝑡)‘𝑤)
30	25, 29	wb 195	. . . . . 6 wff (𝑣(mFresh‘𝑡)𝑤 ↔ 𝑣(mFresh‘𝑡)((mUSyn‘𝑡)‘𝑤))
31	7, 4	cfv 5804	. . . . . 6 class (mUV‘𝑐)
32	30, 21, 31	wral 2896	. . . . 5 wff ∀𝑤 ∈ (mUV‘𝑐)(𝑣(mFresh‘𝑡)𝑤 ↔ 𝑣(mFresh‘𝑡)((mUSyn‘𝑡)‘𝑤))
33	32, 19, 31	wral 2896	. . . 4 wff ∀𝑣 ∈ (mUV‘𝑐)∀𝑤 ∈ (mUV‘𝑐)(𝑣(mFresh‘𝑡)𝑤 ↔ 𝑣(mFresh‘𝑡)((mUSyn‘𝑡)‘𝑤))
34		cmevl 30759	. . . . . . . . 9 class mEval
35	3, 34	cfv 5804	. . . . . . . 8 class (mEval‘𝑡)
36		vm	. . . . . . . . . . 11 setvar 𝑚
37	36	cv 1474	. . . . . . . . . 10 class 𝑚
38		ve	. . . . . . . . . . 11 setvar 𝑒
39	38	cv 1474	. . . . . . . . . 10 class 𝑒
40	37, 39	cop 4131	. . . . . . . . 9 class ⟨𝑚, 𝑒⟩
41	40	csn 4125	. . . . . . . 8 class {⟨𝑚, 𝑒⟩}
42	35, 41	cima 5041	. . . . . . 7 class ((mEval‘𝑡) “ {⟨𝑚, 𝑒⟩})
43		cmesy 30740	. . . . . . . . . . . . 13 class mESyn
44	3, 43	cfv 5804	. . . . . . . . . . . 12 class (mESyn‘𝑡)
45	39, 44	cfv 5804	. . . . . . . . . . 11 class ((mESyn‘𝑡)‘𝑒)
46	37, 45	cop 4131	. . . . . . . . . 10 class ⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩
47	46	csn 4125	. . . . . . . . 9 class {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}
48	35, 47	cima 5041	. . . . . . . 8 class ((mEval‘𝑡) “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩})
49		c1st 7057	. . . . . . . . . . 11 class 1st
50	39, 49	cfv 5804	. . . . . . . . . 10 class (1st ‘𝑒)
51	50	csn 4125	. . . . . . . . 9 class {(1st ‘𝑒)}
52	5, 51	cima 5041	. . . . . . . 8 class ((mUV‘𝑡) “ {(1st ‘𝑒)})
53	48, 52	cin 3539	. . . . . . 7 class (((mEval‘𝑡) “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st ‘𝑒)}))
54	42, 53	wceq 1475	. . . . . 6 wff ((mEval‘𝑡) “ {⟨𝑚, 𝑒⟩}) = (((mEval‘𝑡) “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st ‘𝑒)}))
55		cmex 30618	. . . . . . 7 class mEx
56	3, 55	cfv 5804	. . . . . 6 class (mEx‘𝑡)
57	54, 38, 56	wral 2896	. . . . 5 wff ∀𝑒 ∈ (mEx‘𝑡)((mEval‘𝑡) “ {⟨𝑚, 𝑒⟩}) = (((mEval‘𝑡) “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st ‘𝑒)}))
58		cmvl 30755	. . . . . 6 class mVL
59	3, 58	cfv 5804	. . . . 5 class (mVL‘𝑡)
60	57, 36, 59	wral 2896	. . . 4 wff ∀𝑚 ∈ (mVL‘𝑡)∀𝑒 ∈ (mEx‘𝑡)((mEval‘𝑡) “ {⟨𝑚, 𝑒⟩}) = (((mEval‘𝑡) “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st ‘𝑒)}))
61	18, 33, 60	w3a 1031	. . 3 wff (∀𝑐 ∈ (mTC‘𝑡)((mUV‘𝑡) “ {𝑐}) ⊆ ((mUV‘𝑡) “ {((mSyn‘𝑡)‘𝑐)}) ∧ ∀𝑣 ∈ (mUV‘𝑐)∀𝑤 ∈ (mUV‘𝑐)(𝑣(mFresh‘𝑡)𝑤 ↔ 𝑣(mFresh‘𝑡)((mUSyn‘𝑡)‘𝑤)) ∧ ∀𝑚 ∈ (mVL‘𝑡)∀𝑒 ∈ (mEx‘𝑡)((mEval‘𝑡) “ {⟨𝑚, 𝑒⟩}) = (((mEval‘𝑡) “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st ‘𝑒)})))
62		cmgfs 30741	. . . 4 class mGFS
63		cmdl 30760	. . . 4 class mMdl
64	62, 63	cin 3539	. . 3 class (mGFS ∩ mMdl)
65	61, 2, 64	crab 2900	. 2 class {𝑡 ∈ (mGFS ∩ mMdl) ∣ (∀𝑐 ∈ (mTC‘𝑡)((mUV‘𝑡) “ {𝑐}) ⊆ ((mUV‘𝑡) “ {((mSyn‘𝑡)‘𝑐)}) ∧ ∀𝑣 ∈ (mUV‘𝑐)∀𝑤 ∈ (mUV‘𝑐)(𝑣(mFresh‘𝑡)𝑤 ↔ 𝑣(mFresh‘𝑡)((mUSyn‘𝑡)‘𝑤)) ∧ ∀𝑚 ∈ (mVL‘𝑡)∀𝑒 ∈ (mEx‘𝑡)((mEval‘𝑡) “ {⟨𝑚, 𝑒⟩}) = (((mEval‘𝑡) “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st ‘𝑒)})))}
66	1, 65	wceq 1475	1 wff mGMdl = {𝑡 ∈ (mGFS ∩ mMdl) ∣ (∀𝑐 ∈ (mTC‘𝑡)((mUV‘𝑡) “ {𝑐}) ⊆ ((mUV‘𝑡) “ {((mSyn‘𝑡)‘𝑐)}) ∧ ∀𝑣 ∈ (mUV‘𝑐)∀𝑤 ∈ (mUV‘𝑐)(𝑣(mFresh‘𝑡)𝑤 ↔ 𝑣(mFresh‘𝑡)((mUSyn‘𝑡)‘𝑤)) ∧ ∀𝑚 ∈ (mVL‘𝑡)∀𝑒 ∈ (mEx‘𝑡)((mEval‘𝑡) “ {⟨𝑚, 𝑒⟩}) = (((mEval‘𝑡) “ {⟨𝑚, ((mESyn‘𝑡)‘𝑒)⟩}) ∩ ((mUV‘𝑡) “ {(1st ‘𝑒)})))}

This definition is referenced by: (None)