Definition df-mgfs 35542

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

Step	Hyp	Ref	Expression
1		cmgfs 35532	. 2 class mGFS
2		vt	. . . . . . 7 setvar 𝑡
3	2	cv 1538	. . . . . 6 class 𝑡
4		cmtc 35406	. . . . . 6 class mTC
5	3, 4	cfv 6542	. . . . 5 class (mTC‘𝑡)
6		cmvt 35405	. . . . . 6 class mVT
7	3, 6	cfv 6542	. . . . 5 class (mVT‘𝑡)
8		cmsy 35530	. . . . . 6 class mSyn
9	3, 8	cfv 6542	. . . . 5 class (mSyn‘𝑡)
10	5, 7, 9	wf 6538	. . . 4 wff (mSyn‘𝑡):(mTC‘𝑡)⟶(mVT‘𝑡)
11		vc	. . . . . . . 8 setvar 𝑐
12	11	cv 1538	. . . . . . 7 class 𝑐
13	12, 9	cfv 6542	. . . . . 6 class ((mSyn‘𝑡)‘𝑐)
14	13, 12	wceq 1539	. . . . 5 wff ((mSyn‘𝑡)‘𝑐) = 𝑐
15	14, 11, 7	wral 3050	. . . 4 wff ∀𝑐 ∈ (mVT‘𝑡)((mSyn‘𝑡)‘𝑐) = 𝑐
16		vd	. . . . . . . . . . 11 setvar 𝑑
17	16	cv 1538	. . . . . . . . . 10 class 𝑑
18		vh	. . . . . . . . . . 11 setvar ℎ
19	18	cv 1538	. . . . . . . . . 10 class ℎ
20		va	. . . . . . . . . . 11 setvar 𝑎
21	20	cv 1538	. . . . . . . . . 10 class 𝑎
22	17, 19, 21	cotp 4616	. . . . . . . . 9 class ⟨𝑑, ℎ, 𝑎⟩
23		cmax 35407	. . . . . . . . . 10 class mAx
24	3, 23	cfv 6542	. . . . . . . . 9 class (mAx‘𝑡)
25	22, 24	wcel 2107	. . . . . . . 8 wff ⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡)
26		ve	. . . . . . . . . . . 12 setvar 𝑒
27	26	cv 1538	. . . . . . . . . . 11 class 𝑒
28		cmesy 35531	. . . . . . . . . . . 12 class mESyn
29	3, 28	cfv 6542	. . . . . . . . . . 11 class (mESyn‘𝑡)
30	27, 29	cfv 6542	. . . . . . . . . 10 class ((mESyn‘𝑡)‘𝑒)
31		cmpps 35420	. . . . . . . . . . 11 class mPPSt
32	3, 31	cfv 6542	. . . . . . . . . 10 class (mPPSt‘𝑡)
33	30, 32	wcel 2107	. . . . . . . . 9 wff ((mESyn‘𝑡)‘𝑒) ∈ (mPPSt‘𝑡)
34	21	csn 4608	. . . . . . . . . 10 class {𝑎}
35	19, 34	cun 3931	. . . . . . . . 9 class (ℎ ∪ {𝑎})
36	33, 26, 35	wral 3050	. . . . . . . 8 wff ∀𝑒 ∈ (ℎ ∪ {𝑎})((mESyn‘𝑡)‘𝑒) ∈ (mPPSt‘𝑡)
37	25, 36	wi 4	. . . . . . 7 wff (⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ∀𝑒 ∈ (ℎ ∪ {𝑎})((mESyn‘𝑡)‘𝑒) ∈ (mPPSt‘𝑡))
38	37, 20	wal 1537	. . . . . 6 wff ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ∀𝑒 ∈ (ℎ ∪ {𝑎})((mESyn‘𝑡)‘𝑒) ∈ (mPPSt‘𝑡))
39	38, 18	wal 1537	. . . . 5 wff ∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ∀𝑒 ∈ (ℎ ∪ {𝑎})((mESyn‘𝑡)‘𝑒) ∈ (mPPSt‘𝑡))
40	39, 16	wal 1537	. . . 4 wff ∀𝑑∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ∀𝑒 ∈ (ℎ ∪ {𝑎})((mESyn‘𝑡)‘𝑒) ∈ (mPPSt‘𝑡))
41	10, 15, 40	w3a 1086	. . 3 wff ((mSyn‘𝑡):(mTC‘𝑡)⟶(mVT‘𝑡) ∧ ∀𝑐 ∈ (mVT‘𝑡)((mSyn‘𝑡)‘𝑐) = 𝑐 ∧ ∀𝑑∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ∀𝑒 ∈ (ℎ ∪ {𝑎})((mESyn‘𝑡)‘𝑒) ∈ (mPPSt‘𝑡)))
42		cmwgfs 35529	. . 3 class mWGFS
43	41, 2, 42	crab 3420	. 2 class {𝑡 ∈ mWGFS ∣ ((mSyn‘𝑡):(mTC‘𝑡)⟶(mVT‘𝑡) ∧ ∀𝑐 ∈ (mVT‘𝑡)((mSyn‘𝑡)‘𝑐) = 𝑐 ∧ ∀𝑑∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ∀𝑒 ∈ (ℎ ∪ {𝑎})((mESyn‘𝑡)‘𝑒) ∈ (mPPSt‘𝑡)))}
44	1, 43	wceq 1539	1 wff mGFS = {𝑡 ∈ mWGFS ∣ ((mSyn‘𝑡):(mTC‘𝑡)⟶(mVT‘𝑡) ∧ ∀𝑐 ∈ (mVT‘𝑡)((mSyn‘𝑡)‘𝑐) = 𝑐 ∧ ∀𝑑∀ℎ∀𝑎(⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) → ∀𝑒 ∈ (ℎ ∪ {𝑎})((mESyn‘𝑡)‘𝑒) ∈ (mPPSt‘𝑡)))}

This definition is referenced by: (None)