Metamath Proof Explorer

Definition df-gmdl

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

Ref Expression
Assertion df-gmdl ⊢ mGMdl = t ∈ mGFS ∩ mMdl | ∀ c ∈ mTC ⁡ t mUV ⁡ t c ⊆ mUV ⁡ t mSyn ⁡ t ⁡ c ∧ ∀ v ∈ mUV ⁡ c ∀ w ∈ mUV ⁡ c v mFresh ⁡ t w ↔ v mFresh ⁡ t mUSyn ⁡ t ⁡ w ∧ ∀ m ∈ mVL ⁡ t ∀ e ∈ mEx ⁡ t mEval ⁡ t m e = mEval ⁡ t m mESyn ⁡ t ⁡ e ∩ mUV ⁡ t 1 st ⁡ e

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgmdl class mGMdl
1 vt setvar t
2 cmgfs class mGFS
3 cmdl class mMdl
4 2 3 cin class mGFS ∩ mMdl
5 vc setvar c
6 cmtc class mTC
7 1 cv setvar t
8 7 6 cfv class mTC ⁡ t
9 cmuv class mUV
10 7 9 cfv class mUV ⁡ t
11 5 cv setvar c
12 11 csn class c
13 10 12 cima class mUV ⁡ t c
14 cmsy class mSyn
15 7 14 cfv class mSyn ⁡ t
16 11 15 cfv class mSyn ⁡ t ⁡ c
17 16 csn class mSyn ⁡ t ⁡ c
18 10 17 cima class mUV ⁡ t mSyn ⁡ t ⁡ c
19 13 18 wss wff mUV ⁡ t c ⊆ mUV ⁡ t mSyn ⁡ t ⁡ c
20 19 5 8 wral wff ∀ c ∈ mTC ⁡ t mUV ⁡ t c ⊆ mUV ⁡ t mSyn ⁡ t ⁡ c
21 vv setvar v
22 11 9 cfv class mUV ⁡ c
23 vw setvar w
24 21 cv setvar v
25 cmfsh class mFresh
26 7 25 cfv class mFresh ⁡ t
27 23 cv setvar w
28 24 27 26 wbr wff v mFresh ⁡ t w
29 cusyn class mUSyn
30 7 29 cfv class mUSyn ⁡ t
31 27 30 cfv class mUSyn ⁡ t ⁡ w
32 24 31 26 wbr wff v mFresh ⁡ t mUSyn ⁡ t ⁡ w
33 28 32 wb wff v mFresh ⁡ t w ↔ v mFresh ⁡ t mUSyn ⁡ t ⁡ w
34 33 23 22 wral wff ∀ w ∈ mUV ⁡ c v mFresh ⁡ t w ↔ v mFresh ⁡ t mUSyn ⁡ t ⁡ w
35 34 21 22 wral wff ∀ v ∈ mUV ⁡ c ∀ w ∈ mUV ⁡ c v mFresh ⁡ t w ↔ v mFresh ⁡ t mUSyn ⁡ t ⁡ w
36 vm setvar m
37 cmvl class mVL
38 7 37 cfv class mVL ⁡ t
39 ve setvar e
40 cmex class mEx
41 7 40 cfv class mEx ⁡ t
42 cmevl class mEval
43 7 42 cfv class mEval ⁡ t
44 36 cv setvar m
45 39 cv setvar e
46 44 45 cop class m e
47 46 csn class m e
48 43 47 cima class mEval ⁡ t m e
49 cmesy class mESyn
50 7 49 cfv class mESyn ⁡ t
51 45 50 cfv class mESyn ⁡ t ⁡ e
52 44 51 cop class m mESyn ⁡ t ⁡ e
53 52 csn class m mESyn ⁡ t ⁡ e
54 43 53 cima class mEval ⁡ t m mESyn ⁡ t ⁡ e
55 c1st class 1 st
56 45 55 cfv class 1 st ⁡ e
57 56 csn class 1 st ⁡ e
58 10 57 cima class mUV ⁡ t 1 st ⁡ e
59 54 58 cin class mEval ⁡ t m mESyn ⁡ t ⁡ e ∩ mUV ⁡ t 1 st ⁡ e
60 48 59 wceq wff mEval ⁡ t m e = mEval ⁡ t m mESyn ⁡ t ⁡ e ∩ mUV ⁡ t 1 st ⁡ e
61 60 39 41 wral wff ∀ e ∈ mEx ⁡ t mEval ⁡ t m e = mEval ⁡ t m mESyn ⁡ t ⁡ e ∩ mUV ⁡ t 1 st ⁡ e
62 61 36 38 wral wff ∀ m ∈ mVL ⁡ t ∀ e ∈ mEx ⁡ t mEval ⁡ t m e = mEval ⁡ t m mESyn ⁡ t ⁡ e ∩ mUV ⁡ t 1 st ⁡ e
63 20 35 62 w3a wff ∀ c ∈ mTC ⁡ t mUV ⁡ t c ⊆ mUV ⁡ t mSyn ⁡ t ⁡ c ∧ ∀ v ∈ mUV ⁡ c ∀ w ∈ mUV ⁡ c v mFresh ⁡ t w ↔ v mFresh ⁡ t mUSyn ⁡ t ⁡ w ∧ ∀ m ∈ mVL ⁡ t ∀ e ∈ mEx ⁡ t mEval ⁡ t m e = mEval ⁡ t m mESyn ⁡ t ⁡ e ∩ mUV ⁡ t 1 st ⁡ e
64 63 1 4 crab class t ∈ mGFS ∩ mMdl | ∀ c ∈ mTC ⁡ t mUV ⁡ t c ⊆ mUV ⁡ t mSyn ⁡ t ⁡ c ∧ ∀ v ∈ mUV ⁡ c ∀ w ∈ mUV ⁡ c v mFresh ⁡ t w ↔ v mFresh ⁡ t mUSyn ⁡ t ⁡ w ∧ ∀ m ∈ mVL ⁡ t ∀ e ∈ mEx ⁡ t mEval ⁡ t m e = mEval ⁡ t m mESyn ⁡ t ⁡ e ∩ mUV ⁡ t 1 st ⁡ e
65 0 64 wceq wff mGMdl = t ∈ mGFS ∩ mMdl | ∀ c ∈ mTC ⁡ t mUV ⁡ t c ⊆ mUV ⁡ t mSyn ⁡ t ⁡ c ∧ ∀ v ∈ mUV ⁡ c ∀ w ∈ mUV ⁡ c v mFresh ⁡ t w ↔ v mFresh ⁡ t mUSyn ⁡ t ⁡ w ∧ ∀ m ∈ mVL ⁡ t ∀ e ∈ mEx ⁡ t mEval ⁡ t m e = mEval ⁡ t m mESyn ⁡ t ⁡ e ∩ mUV ⁡ t 1 st ⁡ e