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⁡tmUV⁡tc⊆mUV⁡tmSyn⁡t⁡c∧∀v∈mUV⁡c∀w∈mUV⁡cvmFresh⁡tw↔vmFresh⁡tmUSyn⁡t⁡w∧∀m∈mVL⁡t∀e∈mEx⁡tmEval⁡tme=mEval⁡tmmESyn⁡t⁡e∩mUV⁡t1st⁡e

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgmdl classmGMdl
1 vt setvart
2 cmgfs classmGFS
3 cmdl classmMdl
4 2 3 cin classmGFS∩mMdl
5 vc setvarc
6 cmtc classmTC
7 1 cv setvart
8 7 6 cfv classmTC⁡t
9 cmuv classmUV
10 7 9 cfv classmUV⁡t
11 5 cv setvarc
12 11 csn classc
13 10 12 cima classmUV⁡tc
14 cmsy classmSyn
15 7 14 cfv classmSyn⁡t
16 11 15 cfv classmSyn⁡t⁡c
17 16 csn classmSyn⁡t⁡c
18 10 17 cima classmUV⁡tmSyn⁡t⁡c
19 13 18 wss wffmUV⁡tc⊆mUV⁡tmSyn⁡t⁡c
20 19 5 8 wral wff∀c∈mTC⁡tmUV⁡tc⊆mUV⁡tmSyn⁡t⁡c
21 vv setvarv
22 11 9 cfv classmUV⁡c
23 vw setvarw
24 21 cv setvarv
25 cmfsh classmFresh
26 7 25 cfv classmFresh⁡t
27 23 cv setvarw
28 24 27 26 wbr wffvmFresh⁡tw
29 cusyn classmUSyn
30 7 29 cfv classmUSyn⁡t
31 27 30 cfv classmUSyn⁡t⁡w
32 24 31 26 wbr wffvmFresh⁡tmUSyn⁡t⁡w
33 28 32 wb wffvmFresh⁡tw↔vmFresh⁡tmUSyn⁡t⁡w
34 33 23 22 wral wff∀w∈mUV⁡cvmFresh⁡tw↔vmFresh⁡tmUSyn⁡t⁡w
35 34 21 22 wral wff∀v∈mUV⁡c∀w∈mUV⁡cvmFresh⁡tw↔vmFresh⁡tmUSyn⁡t⁡w
36 vm setvarm
37 cmvl classmVL
38 7 37 cfv classmVL⁡t
39 ve setvare
40 cmex classmEx
41 7 40 cfv classmEx⁡t
42 cmevl classmEval
43 7 42 cfv classmEval⁡t
44 36 cv setvarm
45 39 cv setvare
46 44 45 cop classme
47 46 csn classme
48 43 47 cima classmEval⁡tme
49 cmesy classmESyn
50 7 49 cfv classmESyn⁡t
51 45 50 cfv classmESyn⁡t⁡e
52 44 51 cop classmmESyn⁡t⁡e
53 52 csn classmmESyn⁡t⁡e
54 43 53 cima classmEval⁡tmmESyn⁡t⁡e
55 c1st class1st
56 45 55 cfv class1st⁡e
57 56 csn class1st⁡e
58 10 57 cima classmUV⁡t1st⁡e
59 54 58 cin classmEval⁡tmmESyn⁡t⁡e∩mUV⁡t1st⁡e
60 48 59 wceq wffmEval⁡tme=mEval⁡tmmESyn⁡t⁡e∩mUV⁡t1st⁡e
61 60 39 41 wral wff∀e∈mEx⁡tmEval⁡tme=mEval⁡tmmESyn⁡t⁡e∩mUV⁡t1st⁡e
62 61 36 38 wral wff∀m∈mVL⁡t∀e∈mEx⁡tmEval⁡tme=mEval⁡tmmESyn⁡t⁡e∩mUV⁡t1st⁡e
63 20 35 62 w3a wff∀c∈mTC⁡tmUV⁡tc⊆mUV⁡tmSyn⁡t⁡c∧∀v∈mUV⁡c∀w∈mUV⁡cvmFresh⁡tw↔vmFresh⁡tmUSyn⁡t⁡w∧∀m∈mVL⁡t∀e∈mEx⁡tmEval⁡tme=mEval⁡tmmESyn⁡t⁡e∩mUV⁡t1st⁡e
64 63 1 4 crab classt∈mGFS∩mMdl|∀c∈mTC⁡tmUV⁡tc⊆mUV⁡tmSyn⁡t⁡c∧∀v∈mUV⁡c∀w∈mUV⁡cvmFresh⁡tw↔vmFresh⁡tmUSyn⁡t⁡w∧∀m∈mVL⁡t∀e∈mEx⁡tmEval⁡tme=mEval⁡tmmESyn⁡t⁡e∩mUV⁡t1st⁡e
65 0 64 wceq wffmGMdl=t∈mGFS∩mMdl|∀c∈mTC⁡tmUV⁡tc⊆mUV⁡tmSyn⁡t⁡c∧∀v∈mUV⁡c∀w∈mUV⁡cvmFresh⁡tw↔vmFresh⁡tmUSyn⁡t⁡w∧∀m∈mVL⁡t∀e∈mEx⁡tmEval⁡tme=mEval⁡tmmESyn⁡t⁡e∩mUV⁡t1st⁡e