Metamath Proof Explorer

Definition df-mgfs

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

Ref Expression
Assertion df-mgfs ⊢ mGFS = t ∈ mWGFS | mSyn ⁡ t : mTC ⁡ t ⟶ mVT ⁡ t ∧ ∀ c ∈ mVT ⁡ t mSyn ⁡ t ⁡ c = c ∧ ∀ d ∀ h ∀ a d h a ∈ mAx ⁡ t → ∀ e ∈ h ∪ a mESyn ⁡ t ⁡ e ∈ mPPSt ⁡ t

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgfs class mGFS
1 vt setvar t
2 cmwgfs class mWGFS
3 cmsy class mSyn
4 1 cv setvar t
5 4 3 cfv class mSyn ⁡ t
6 cmtc class mTC
7 4 6 cfv class mTC ⁡ t
8 cmvt class mVT
9 4 8 cfv class mVT ⁡ t
10 7 9 5 wf wff mSyn ⁡ t : mTC ⁡ t ⟶ mVT ⁡ t
11 vc setvar c
12 11 cv setvar c
13 12 5 cfv class mSyn ⁡ t ⁡ c
14 13 12 wceq wff mSyn ⁡ t ⁡ c = c
15 14 11 9 wral wff ∀ c ∈ mVT ⁡ t mSyn ⁡ t ⁡ c = c
16 vd setvar d
17 vh setvar h
18 va setvar a
19 16 cv setvar d
20 17 cv setvar h
21 18 cv setvar a
22 19 20 21 cotp class d h a
23 cmax class mAx
24 4 23 cfv class mAx ⁡ t
25 22 24 wcel wff d h a ∈ mAx ⁡ t
26 ve setvar e
27 21 csn class a
28 20 27 cun class h ∪ a
29 cmesy class mESyn
30 4 29 cfv class mESyn ⁡ t
31 26 cv setvar e
32 31 30 cfv class mESyn ⁡ t ⁡ e
33 cmpps class mPPSt
34 4 33 cfv class mPPSt ⁡ t
35 32 34 wcel wff mESyn ⁡ t ⁡ e ∈ mPPSt ⁡ t
36 35 26 28 wral wff ∀ e ∈ h ∪ a mESyn ⁡ t ⁡ e ∈ mPPSt ⁡ t
37 25 36 wi wff d h a ∈ mAx ⁡ t → ∀ e ∈ h ∪ a mESyn ⁡ t ⁡ e ∈ mPPSt ⁡ t
38 37 18 wal wff ∀ a d h a ∈ mAx ⁡ t → ∀ e ∈ h ∪ a mESyn ⁡ t ⁡ e ∈ mPPSt ⁡ t
39 38 17 wal wff ∀ h ∀ a d h a ∈ mAx ⁡ t → ∀ e ∈ h ∪ a mESyn ⁡ t ⁡ e ∈ mPPSt ⁡ t
40 39 16 wal wff ∀ d ∀ h ∀ a d h a ∈ mAx ⁡ t → ∀ e ∈ h ∪ a mESyn ⁡ t ⁡ e ∈ mPPSt ⁡ t
41 10 15 40 w3a wff mSyn ⁡ t : mTC ⁡ t ⟶ mVT ⁡ t ∧ ∀ c ∈ mVT ⁡ t mSyn ⁡ t ⁡ c = c ∧ ∀ d ∀ h ∀ a d h a ∈ mAx ⁡ t → ∀ e ∈ h ∪ a mESyn ⁡ t ⁡ e ∈ mPPSt ⁡ t
42 41 1 2 crab class t ∈ mWGFS | mSyn ⁡ t : mTC ⁡ t ⟶ mVT ⁡ t ∧ ∀ c ∈ mVT ⁡ t mSyn ⁡ t ⁡ c = c ∧ ∀ d ∀ h ∀ a d h a ∈ mAx ⁡ t → ∀ e ∈ h ∪ a mESyn ⁡ t ⁡ e ∈ mPPSt ⁡ t
43 0 42 wceq wff mGFS = t ∈ mWGFS | mSyn ⁡ t : mTC ⁡ t ⟶ mVT ⁡ t ∧ ∀ c ∈ mVT ⁡ t mSyn ⁡ t ⁡ c = c ∧ ∀ d ∀ h ∀ a d h a ∈ mAx ⁡ t → ∀ e ∈ h ∪ a mESyn ⁡ t ⁡ e ∈ mPPSt ⁡ t