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

Definition df-mwgfs 35116
Description: Define the set of weakly grammatical formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mwgfs mWGFS = {𝑑 ∈ mFS ∣ βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž((βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) ∧ (1st β€˜π‘Ž) ∈ (mVTβ€˜π‘‘)) β†’ βˆƒπ‘  ∈ ran (mSubstβ€˜π‘‘)π‘Ž ∈ (𝑠 β€œ (mSAβ€˜π‘‘)))}
Distinct variable group:   π‘Ž,𝑑,β„Ž,𝑠,𝑑

Detailed syntax breakdown of Definition df-mwgfs
StepHypRef Expression
1 cmwgfs 35106 . 2 class mWGFS
2 vd . . . . . . . . . . 11 setvar 𝑑
32cv 1532 . . . . . . . . . 10 class 𝑑
4 vh . . . . . . . . . . 11 setvar β„Ž
54cv 1532 . . . . . . . . . 10 class β„Ž
6 va . . . . . . . . . . 11 setvar π‘Ž
76cv 1532 . . . . . . . . . 10 class π‘Ž
83, 5, 7cotp 4631 . . . . . . . . 9 class βŸ¨π‘‘, β„Ž, π‘ŽβŸ©
9 vt . . . . . . . . . . 11 setvar 𝑑
109cv 1532 . . . . . . . . . 10 class 𝑑
11 cmax 34984 . . . . . . . . . 10 class mAx
1210, 11cfv 6537 . . . . . . . . 9 class (mAxβ€˜π‘‘)
138, 12wcel 2098 . . . . . . . 8 wff βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘)
14 c1st 7972 . . . . . . . . . 10 class 1st
157, 14cfv 6537 . . . . . . . . 9 class (1st β€˜π‘Ž)
16 cmvt 34982 . . . . . . . . . 10 class mVT
1710, 16cfv 6537 . . . . . . . . 9 class (mVTβ€˜π‘‘)
1815, 17wcel 2098 . . . . . . . 8 wff (1st β€˜π‘Ž) ∈ (mVTβ€˜π‘‘)
1913, 18wa 395 . . . . . . 7 wff (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) ∧ (1st β€˜π‘Ž) ∈ (mVTβ€˜π‘‘))
20 vs . . . . . . . . . . 11 setvar 𝑠
2120cv 1532 . . . . . . . . . 10 class 𝑠
22 cmsa 35105 . . . . . . . . . . 11 class mSA
2310, 22cfv 6537 . . . . . . . . . 10 class (mSAβ€˜π‘‘)
2421, 23cima 5672 . . . . . . . . 9 class (𝑠 β€œ (mSAβ€˜π‘‘))
257, 24wcel 2098 . . . . . . . 8 wff π‘Ž ∈ (𝑠 β€œ (mSAβ€˜π‘‘))
26 cmsub 34990 . . . . . . . . . 10 class mSubst
2710, 26cfv 6537 . . . . . . . . 9 class (mSubstβ€˜π‘‘)
2827crn 5670 . . . . . . . 8 class ran (mSubstβ€˜π‘‘)
2925, 20, 28wrex 3064 . . . . . . 7 wff βˆƒπ‘  ∈ ran (mSubstβ€˜π‘‘)π‘Ž ∈ (𝑠 β€œ (mSAβ€˜π‘‘))
3019, 29wi 4 . . . . . 6 wff ((βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) ∧ (1st β€˜π‘Ž) ∈ (mVTβ€˜π‘‘)) β†’ βˆƒπ‘  ∈ ran (mSubstβ€˜π‘‘)π‘Ž ∈ (𝑠 β€œ (mSAβ€˜π‘‘)))
3130, 6wal 1531 . . . . 5 wff βˆ€π‘Ž((βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) ∧ (1st β€˜π‘Ž) ∈ (mVTβ€˜π‘‘)) β†’ βˆƒπ‘  ∈ ran (mSubstβ€˜π‘‘)π‘Ž ∈ (𝑠 β€œ (mSAβ€˜π‘‘)))
3231, 4wal 1531 . . . 4 wff βˆ€β„Žβˆ€π‘Ž((βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) ∧ (1st β€˜π‘Ž) ∈ (mVTβ€˜π‘‘)) β†’ βˆƒπ‘  ∈ ran (mSubstβ€˜π‘‘)π‘Ž ∈ (𝑠 β€œ (mSAβ€˜π‘‘)))
3332, 2wal 1531 . . 3 wff βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž((βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) ∧ (1st β€˜π‘Ž) ∈ (mVTβ€˜π‘‘)) β†’ βˆƒπ‘  ∈ ran (mSubstβ€˜π‘‘)π‘Ž ∈ (𝑠 β€œ (mSAβ€˜π‘‘)))
34 cmfs 34995 . . 3 class mFS
3533, 9, 34crab 3426 . 2 class {𝑑 ∈ mFS ∣ βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž((βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) ∧ (1st β€˜π‘Ž) ∈ (mVTβ€˜π‘‘)) β†’ βˆƒπ‘  ∈ ran (mSubstβ€˜π‘‘)π‘Ž ∈ (𝑠 β€œ (mSAβ€˜π‘‘)))}
361, 35wceq 1533 1 wff mWGFS = {𝑑 ∈ mFS ∣ βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž((βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) ∧ (1st β€˜π‘Ž) ∈ (mVTβ€˜π‘‘)) β†’ βˆƒπ‘  ∈ ran (mSubstβ€˜π‘‘)π‘Ž ∈ (𝑠 β€œ (mSAβ€˜π‘‘)))}
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator