Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gmdl Structured version   Visualization version   GIF version

Definition df-gmdl 34901
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
StepHypRef Expression
1 cgmdl 34890 . 2 class mGMdl
2 vt . . . . . . . . 9 setvar 𝑑
32cv 1540 . . . . . . . 8 class 𝑑
4 cmuv 34882 . . . . . . . 8 class mUV
53, 4cfv 6543 . . . . . . 7 class (mUVβ€˜π‘‘)
6 vc . . . . . . . . 9 setvar 𝑐
76cv 1540 . . . . . . . 8 class 𝑐
87csn 4628 . . . . . . 7 class {𝑐}
95, 8cima 5679 . . . . . 6 class ((mUVβ€˜π‘‘) β€œ {𝑐})
10 cmsy 34865 . . . . . . . . . 10 class mSyn
113, 10cfv 6543 . . . . . . . . 9 class (mSynβ€˜π‘‘)
127, 11cfv 6543 . . . . . . . 8 class ((mSynβ€˜π‘‘)β€˜π‘)
1312csn 4628 . . . . . . 7 class {((mSynβ€˜π‘‘)β€˜π‘)}
145, 13cima 5679 . . . . . 6 class ((mUVβ€˜π‘‘) β€œ {((mSynβ€˜π‘‘)β€˜π‘)})
159, 14wss 3948 . . . . 5 wff ((mUVβ€˜π‘‘) β€œ {𝑐}) βŠ† ((mUVβ€˜π‘‘) β€œ {((mSynβ€˜π‘‘)β€˜π‘)})
16 cmtc 34741 . . . . . 6 class mTC
173, 16cfv 6543 . . . . 5 class (mTCβ€˜π‘‘)
1815, 6, 17wral 3061 . . . 4 wff βˆ€π‘ ∈ (mTCβ€˜π‘‘)((mUVβ€˜π‘‘) β€œ {𝑐}) βŠ† ((mUVβ€˜π‘‘) β€œ {((mSynβ€˜π‘‘)β€˜π‘)})
19 vv . . . . . . . . 9 setvar 𝑣
2019cv 1540 . . . . . . . 8 class 𝑣
21 vw . . . . . . . . 9 setvar 𝑀
2221cv 1540 . . . . . . . 8 class 𝑀
23 cmfsh 34885 . . . . . . . . 9 class mFresh
243, 23cfv 6543 . . . . . . . 8 class (mFreshβ€˜π‘‘)
2520, 22, 24wbr 5148 . . . . . . 7 wff 𝑣(mFreshβ€˜π‘‘)𝑀
26 cusyn 34889 . . . . . . . . . 10 class mUSyn
273, 26cfv 6543 . . . . . . . . 9 class (mUSynβ€˜π‘‘)
2822, 27cfv 6543 . . . . . . . 8 class ((mUSynβ€˜π‘‘)β€˜π‘€)
2920, 28, 24wbr 5148 . . . . . . 7 wff 𝑣(mFreshβ€˜π‘‘)((mUSynβ€˜π‘‘)β€˜π‘€)
3025, 29wb 205 . . . . . 6 wff (𝑣(mFreshβ€˜π‘‘)𝑀 ↔ 𝑣(mFreshβ€˜π‘‘)((mUSynβ€˜π‘‘)β€˜π‘€))
317, 4cfv 6543 . . . . . 6 class (mUVβ€˜π‘)
3230, 21, 31wral 3061 . . . . 5 wff βˆ€π‘€ ∈ (mUVβ€˜π‘)(𝑣(mFreshβ€˜π‘‘)𝑀 ↔ 𝑣(mFreshβ€˜π‘‘)((mUSynβ€˜π‘‘)β€˜π‘€))
3332, 19, 31wral 3061 . . . 4 wff βˆ€π‘£ ∈ (mUVβ€˜π‘)βˆ€π‘€ ∈ (mUVβ€˜π‘)(𝑣(mFreshβ€˜π‘‘)𝑀 ↔ 𝑣(mFreshβ€˜π‘‘)((mUSynβ€˜π‘‘)β€˜π‘€))
34 cmevl 34887 . . . . . . . . 9 class mEval
353, 34cfv 6543 . . . . . . . 8 class (mEvalβ€˜π‘‘)
36 vm . . . . . . . . . . 11 setvar π‘š
3736cv 1540 . . . . . . . . . 10 class π‘š
38 ve . . . . . . . . . . 11 setvar 𝑒
3938cv 1540 . . . . . . . . . 10 class 𝑒
4037, 39cop 4634 . . . . . . . . 9 class βŸ¨π‘š, π‘’βŸ©
4140csn 4628 . . . . . . . 8 class {βŸ¨π‘š, π‘’βŸ©}
4235, 41cima 5679 . . . . . . 7 class ((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, π‘’βŸ©})
43 cmesy 34866 . . . . . . . . . . . . 13 class mESyn
443, 43cfv 6543 . . . . . . . . . . . 12 class (mESynβ€˜π‘‘)
4539, 44cfv 6543 . . . . . . . . . . 11 class ((mESynβ€˜π‘‘)β€˜π‘’)
4637, 45cop 4634 . . . . . . . . . 10 class βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩
4746csn 4628 . . . . . . . . 9 class {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}
4835, 47cima 5679 . . . . . . . 8 class ((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩})
49 c1st 7975 . . . . . . . . . . 11 class 1st
5039, 49cfv 6543 . . . . . . . . . 10 class (1st β€˜π‘’)
5150csn 4628 . . . . . . . . 9 class {(1st β€˜π‘’)}
525, 51cima 5679 . . . . . . . 8 class ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)})
5348, 52cin 3947 . . . . . . 7 class (((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}) ∩ ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)}))
5442, 53wceq 1541 . . . . . 6 wff ((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, π‘’βŸ©}) = (((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}) ∩ ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)}))
55 cmex 34744 . . . . . . 7 class mEx
563, 55cfv 6543 . . . . . 6 class (mExβ€˜π‘‘)
5754, 38, 56wral 3061 . . . . 5 wff βˆ€π‘’ ∈ (mExβ€˜π‘‘)((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, π‘’βŸ©}) = (((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}) ∩ ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)}))
58 cmvl 34883 . . . . . 6 class mVL
593, 58cfv 6543 . . . . 5 class (mVLβ€˜π‘‘)
6057, 36, 59wral 3061 . . . 4 wff βˆ€π‘š ∈ (mVLβ€˜π‘‘)βˆ€π‘’ ∈ (mExβ€˜π‘‘)((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, π‘’βŸ©}) = (((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}) ∩ ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)}))
6118, 33, 60w3a 1087 . . 3 wff (βˆ€π‘ ∈ (mTCβ€˜π‘‘)((mUVβ€˜π‘‘) β€œ {𝑐}) βŠ† ((mUVβ€˜π‘‘) β€œ {((mSynβ€˜π‘‘)β€˜π‘)}) ∧ βˆ€π‘£ ∈ (mUVβ€˜π‘)βˆ€π‘€ ∈ (mUVβ€˜π‘)(𝑣(mFreshβ€˜π‘‘)𝑀 ↔ 𝑣(mFreshβ€˜π‘‘)((mUSynβ€˜π‘‘)β€˜π‘€)) ∧ βˆ€π‘š ∈ (mVLβ€˜π‘‘)βˆ€π‘’ ∈ (mExβ€˜π‘‘)((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, π‘’βŸ©}) = (((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}) ∩ ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)})))
62 cmgfs 34867 . . . 4 class mGFS
63 cmdl 34888 . . . 4 class mMdl
6462, 63cin 3947 . . 3 class (mGFS ∩ mMdl)
6561, 2, 64crab 3432 . 2 class {𝑑 ∈ (mGFS ∩ mMdl) ∣ (βˆ€π‘ ∈ (mTCβ€˜π‘‘)((mUVβ€˜π‘‘) β€œ {𝑐}) βŠ† ((mUVβ€˜π‘‘) β€œ {((mSynβ€˜π‘‘)β€˜π‘)}) ∧ βˆ€π‘£ ∈ (mUVβ€˜π‘)βˆ€π‘€ ∈ (mUVβ€˜π‘)(𝑣(mFreshβ€˜π‘‘)𝑀 ↔ 𝑣(mFreshβ€˜π‘‘)((mUSynβ€˜π‘‘)β€˜π‘€)) ∧ βˆ€π‘š ∈ (mVLβ€˜π‘‘)βˆ€π‘’ ∈ (mExβ€˜π‘‘)((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, π‘’βŸ©}) = (((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}) ∩ ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)})))}
661, 65wceq 1541 1 wff mGMdl = {𝑑 ∈ (mGFS ∩ mMdl) ∣ (βˆ€π‘ ∈ (mTCβ€˜π‘‘)((mUVβ€˜π‘‘) β€œ {𝑐}) βŠ† ((mUVβ€˜π‘‘) β€œ {((mSynβ€˜π‘‘)β€˜π‘)}) ∧ βˆ€π‘£ ∈ (mUVβ€˜π‘)βˆ€π‘€ ∈ (mUVβ€˜π‘)(𝑣(mFreshβ€˜π‘‘)𝑀 ↔ 𝑣(mFreshβ€˜π‘‘)((mUSynβ€˜π‘‘)β€˜π‘€)) ∧ βˆ€π‘š ∈ (mVLβ€˜π‘‘)βˆ€π‘’ ∈ (mExβ€˜π‘‘)((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, π‘’βŸ©}) = (((mEvalβ€˜π‘‘) β€œ {βŸ¨π‘š, ((mESynβ€˜π‘‘)β€˜π‘’)⟩}) ∩ ((mUVβ€˜π‘‘) β€œ {(1st β€˜π‘’)})))}
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator