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

Definition df-mgfs 34586
Description: Define the set of grammatical formal systems. (Contributed by Mario Carneiro, 12-Jun-2023.)
Assertion
Ref Expression
df-mgfs mGFS = {𝑑 ∈ mWGFS ∣ ((mSynβ€˜π‘‘):(mTCβ€˜π‘‘)⟢(mVTβ€˜π‘‘) ∧ βˆ€π‘ ∈ (mVTβ€˜π‘‘)((mSynβ€˜π‘‘)β€˜π‘) = 𝑐 ∧ βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘’ ∈ (β„Ž βˆͺ {π‘Ž})((mESynβ€˜π‘‘)β€˜π‘’) ∈ (mPPStβ€˜π‘‘)))}
Distinct variable group:   π‘Ž,𝑐,𝑑,𝑒,β„Ž,𝑑

Detailed syntax breakdown of Definition df-mgfs
StepHypRef Expression
1 cmgfs 34576 . 2 class mGFS
2 vt . . . . . . 7 setvar 𝑑
32cv 1540 . . . . . 6 class 𝑑
4 cmtc 34450 . . . . . 6 class mTC
53, 4cfv 6543 . . . . 5 class (mTCβ€˜π‘‘)
6 cmvt 34449 . . . . . 6 class mVT
73, 6cfv 6543 . . . . 5 class (mVTβ€˜π‘‘)
8 cmsy 34574 . . . . . 6 class mSyn
93, 8cfv 6543 . . . . 5 class (mSynβ€˜π‘‘)
105, 7, 9wf 6539 . . . 4 wff (mSynβ€˜π‘‘):(mTCβ€˜π‘‘)⟢(mVTβ€˜π‘‘)
11 vc . . . . . . . 8 setvar 𝑐
1211cv 1540 . . . . . . 7 class 𝑐
1312, 9cfv 6543 . . . . . 6 class ((mSynβ€˜π‘‘)β€˜π‘)
1413, 12wceq 1541 . . . . 5 wff ((mSynβ€˜π‘‘)β€˜π‘) = 𝑐
1514, 11, 7wral 3061 . . . 4 wff βˆ€π‘ ∈ (mVTβ€˜π‘‘)((mSynβ€˜π‘‘)β€˜π‘) = 𝑐
16 vd . . . . . . . . . . 11 setvar 𝑑
1716cv 1540 . . . . . . . . . 10 class 𝑑
18 vh . . . . . . . . . . 11 setvar β„Ž
1918cv 1540 . . . . . . . . . 10 class β„Ž
20 va . . . . . . . . . . 11 setvar π‘Ž
2120cv 1540 . . . . . . . . . 10 class π‘Ž
2217, 19, 21cotp 4636 . . . . . . . . 9 class βŸ¨π‘‘, β„Ž, π‘ŽβŸ©
23 cmax 34451 . . . . . . . . . 10 class mAx
243, 23cfv 6543 . . . . . . . . 9 class (mAxβ€˜π‘‘)
2522, 24wcel 2106 . . . . . . . 8 wff βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘)
26 ve . . . . . . . . . . . 12 setvar 𝑒
2726cv 1540 . . . . . . . . . . 11 class 𝑒
28 cmesy 34575 . . . . . . . . . . . 12 class mESyn
293, 28cfv 6543 . . . . . . . . . . 11 class (mESynβ€˜π‘‘)
3027, 29cfv 6543 . . . . . . . . . 10 class ((mESynβ€˜π‘‘)β€˜π‘’)
31 cmpps 34464 . . . . . . . . . . 11 class mPPSt
323, 31cfv 6543 . . . . . . . . . 10 class (mPPStβ€˜π‘‘)
3330, 32wcel 2106 . . . . . . . . 9 wff ((mESynβ€˜π‘‘)β€˜π‘’) ∈ (mPPStβ€˜π‘‘)
3421csn 4628 . . . . . . . . . 10 class {π‘Ž}
3519, 34cun 3946 . . . . . . . . 9 class (β„Ž βˆͺ {π‘Ž})
3633, 26, 35wral 3061 . . . . . . . 8 wff βˆ€π‘’ ∈ (β„Ž βˆͺ {π‘Ž})((mESynβ€˜π‘‘)β€˜π‘’) ∈ (mPPStβ€˜π‘‘)
3725, 36wi 4 . . . . . . 7 wff (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘’ ∈ (β„Ž βˆͺ {π‘Ž})((mESynβ€˜π‘‘)β€˜π‘’) ∈ (mPPStβ€˜π‘‘))
3837, 20wal 1539 . . . . . 6 wff βˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘’ ∈ (β„Ž βˆͺ {π‘Ž})((mESynβ€˜π‘‘)β€˜π‘’) ∈ (mPPStβ€˜π‘‘))
3938, 18wal 1539 . . . . 5 wff βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘’ ∈ (β„Ž βˆͺ {π‘Ž})((mESynβ€˜π‘‘)β€˜π‘’) ∈ (mPPStβ€˜π‘‘))
4039, 16wal 1539 . . . 4 wff βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘’ ∈ (β„Ž βˆͺ {π‘Ž})((mESynβ€˜π‘‘)β€˜π‘’) ∈ (mPPStβ€˜π‘‘))
4110, 15, 40w3a 1087 . . 3 wff ((mSynβ€˜π‘‘):(mTCβ€˜π‘‘)⟢(mVTβ€˜π‘‘) ∧ βˆ€π‘ ∈ (mVTβ€˜π‘‘)((mSynβ€˜π‘‘)β€˜π‘) = 𝑐 ∧ βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘’ ∈ (β„Ž βˆͺ {π‘Ž})((mESynβ€˜π‘‘)β€˜π‘’) ∈ (mPPStβ€˜π‘‘)))
42 cmwgfs 34573 . . 3 class mWGFS
4341, 2, 42crab 3432 . 2 class {𝑑 ∈ mWGFS ∣ ((mSynβ€˜π‘‘):(mTCβ€˜π‘‘)⟢(mVTβ€˜π‘‘) ∧ βˆ€π‘ ∈ (mVTβ€˜π‘‘)((mSynβ€˜π‘‘)β€˜π‘) = 𝑐 ∧ βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘’ ∈ (β„Ž βˆͺ {π‘Ž})((mESynβ€˜π‘‘)β€˜π‘’) ∈ (mPPStβ€˜π‘‘)))}
441, 43wceq 1541 1 wff mGFS = {𝑑 ∈ mWGFS ∣ ((mSynβ€˜π‘‘):(mTCβ€˜π‘‘)⟢(mVTβ€˜π‘‘) ∧ βˆ€π‘ ∈ (mVTβ€˜π‘‘)((mSynβ€˜π‘‘)β€˜π‘) = 𝑐 ∧ βˆ€π‘‘βˆ€β„Žβˆ€π‘Ž(βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘’ ∈ (β„Ž βˆͺ {π‘Ž})((mESynβ€˜π‘‘)β€˜π‘’) ∈ (mPPStβ€˜π‘‘)))}
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator