Definition df-mgfs

Description: Define the set of grammatical formal systems. (Contributed by Mario Carneiro, 12-Jun-2023)

	Ref	Expression
Assertion	df-mgfs	⊢ mGFS = { 𝑡 ∈ mWGFS ∣ ( ( mSyn ‘ 𝑡 ) : ( mTC ‘ 𝑡 ) ⟶ ( mVT ‘ 𝑡 ) ∧ ∀ 𝑐 ∈ ( mVT ‘ 𝑡 ) ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) = 𝑐 ∧ ∀ 𝑑 ∀ ℎ ∀ 𝑎 ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑒 ∈ ( ℎ ∪ { 𝑎 } ) ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ∈ ( mPPSt ‘ 𝑡 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmgfs	⊢ mGFS
1		vt	⊢ 𝑡
2		cmwgfs	⊢ mWGFS
3		cmsy	⊢ mSyn
4	1	cv	⊢ 𝑡
5	4 3	cfv	⊢ ( mSyn ‘ 𝑡 )
6		cmtc	⊢ mTC
7	4 6	cfv	⊢ ( mTC ‘ 𝑡 )
8		cmvt	⊢ mVT
9	4 8	cfv	⊢ ( mVT ‘ 𝑡 )
10	7 9 5	wf	⊢ ( mSyn ‘ 𝑡 ) : ( mTC ‘ 𝑡 ) ⟶ ( mVT ‘ 𝑡 )
11		vc	⊢ 𝑐
12	11	cv	⊢ 𝑐
13	12 5	cfv	⊢ ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 )
14	13 12	wceq	⊢ ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) = 𝑐
15	14 11 9	wral	⊢ ∀ 𝑐 ∈ ( mVT ‘ 𝑡 ) ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) = 𝑐
16		vd	⊢ 𝑑
17		vh	⊢ ℎ
18		va	⊢ 𝑎
19	16	cv	⊢ 𝑑
20	17	cv	⊢ ℎ
21	18	cv	⊢ 𝑎
22	19 20 21	cotp	⊢ ⟨ 𝑑 , ℎ , 𝑎 ⟩
23		cmax	⊢ mAx
24	4 23	cfv	⊢ ( mAx ‘ 𝑡 )
25	22 24	wcel	⊢ ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 )
26		ve	⊢ 𝑒
27	21	csn	⊢ { 𝑎 }
28	20 27	cun	⊢ ( ℎ ∪ { 𝑎 } )
29		cmesy	⊢ mESyn
30	4 29	cfv	⊢ ( mESyn ‘ 𝑡 )
31	26	cv	⊢ 𝑒
32	31 30	cfv	⊢ ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 )
33		cmpps	⊢ mPPSt
34	4 33	cfv	⊢ ( mPPSt ‘ 𝑡 )
35	32 34	wcel	⊢ ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ∈ ( mPPSt ‘ 𝑡 )
36	35 26 28	wral	⊢ ∀ 𝑒 ∈ ( ℎ ∪ { 𝑎 } ) ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ∈ ( mPPSt ‘ 𝑡 )
37	25 36	wi	⊢ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑒 ∈ ( ℎ ∪ { 𝑎 } ) ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ∈ ( mPPSt ‘ 𝑡 ) )
38	37 18	wal	⊢ ∀ 𝑎 ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑒 ∈ ( ℎ ∪ { 𝑎 } ) ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ∈ ( mPPSt ‘ 𝑡 ) )
39	38 17	wal	⊢ ∀ ℎ ∀ 𝑎 ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑒 ∈ ( ℎ ∪ { 𝑎 } ) ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ∈ ( mPPSt ‘ 𝑡 ) )
40	39 16	wal	⊢ ∀ 𝑑 ∀ ℎ ∀ 𝑎 ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑒 ∈ ( ℎ ∪ { 𝑎 } ) ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ∈ ( mPPSt ‘ 𝑡 ) )
41	10 15 40	w3a	⊢ ( ( mSyn ‘ 𝑡 ) : ( mTC ‘ 𝑡 ) ⟶ ( mVT ‘ 𝑡 ) ∧ ∀ 𝑐 ∈ ( mVT ‘ 𝑡 ) ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) = 𝑐 ∧ ∀ 𝑑 ∀ ℎ ∀ 𝑎 ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑒 ∈ ( ℎ ∪ { 𝑎 } ) ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ∈ ( mPPSt ‘ 𝑡 ) ) )
42	41 1 2	crab	⊢ { 𝑡 ∈ mWGFS ∣ ( ( mSyn ‘ 𝑡 ) : ( mTC ‘ 𝑡 ) ⟶ ( mVT ‘ 𝑡 ) ∧ ∀ 𝑐 ∈ ( mVT ‘ 𝑡 ) ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) = 𝑐 ∧ ∀ 𝑑 ∀ ℎ ∀ 𝑎 ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑒 ∈ ( ℎ ∪ { 𝑎 } ) ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ∈ ( mPPSt ‘ 𝑡 ) ) ) }
43	0 42	wceq	⊢ mGFS = { 𝑡 ∈ mWGFS ∣ ( ( mSyn ‘ 𝑡 ) : ( mTC ‘ 𝑡 ) ⟶ ( mVT ‘ 𝑡 ) ∧ ∀ 𝑐 ∈ ( mVT ‘ 𝑡 ) ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) = 𝑐 ∧ ∀ 𝑑 ∀ ℎ ∀ 𝑎 ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) → ∀ 𝑒 ∈ ( ℎ ∪ { 𝑎 } ) ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ∈ ( mPPSt ‘ 𝑡 ) ) ) }