Definition df-mwgfs 30748

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

Step	Hyp	Ref	Expression
1		cmwgfs 30738	. 2 class mWGFS
2		vd	. . . . . . . . . . 11 setvar 𝑑
3	2	cv 1474	. . . . . . . . . 10 class 𝑑
4		vh	. . . . . . . . . . 11 setvar ℎ
5	4	cv 1474	. . . . . . . . . 10 class ℎ
6		va	. . . . . . . . . . 11 setvar 𝑎
7	6	cv 1474	. . . . . . . . . 10 class 𝑎
8	3, 5, 7	cotp 4133	. . . . . . . . 9 class ⟨𝑑, ℎ, 𝑎⟩
9		vt	. . . . . . . . . . 11 setvar 𝑡
10	9	cv 1474	. . . . . . . . . 10 class 𝑡
11		cmax 30616	. . . . . . . . . 10 class mAx
12	10, 11	cfv 5804	. . . . . . . . 9 class (mAx‘𝑡)
13	8, 12	wcel 1977	. . . . . . . 8 wff ⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡)
14		c1st 7057	. . . . . . . . . 10 class 1st
15	7, 14	cfv 5804	. . . . . . . . 9 class (1st ‘𝑎)
16		cmvt 30614	. . . . . . . . . 10 class mVT
17	10, 16	cfv 5804	. . . . . . . . 9 class (mVT‘𝑡)
18	15, 17	wcel 1977	. . . . . . . 8 wff (1st ‘𝑎) ∈ (mVT‘𝑡)
19	13, 18	wa 383	. . . . . . 7 wff (⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡))
20		vs	. . . . . . . . . . 11 setvar 𝑠
21	20	cv 1474	. . . . . . . . . 10 class 𝑠
22		cmsa 30737	. . . . . . . . . . 11 class mSA
23	10, 22	cfv 5804	. . . . . . . . . 10 class (mSA‘𝑡)
24	21, 23	cima 5041	. . . . . . . . 9 class (𝑠 “ (mSA‘𝑡))
25	7, 24	wcel 1977	. . . . . . . 8 wff 𝑎 ∈ (𝑠 “ (mSA‘𝑡))
26		cmsub 30622	. . . . . . . . . 10 class mSubst
27	10, 26	cfv 5804	. . . . . . . . 9 class (mSubst‘𝑡)
28	27	crn 5039	. . . . . . . 8 class ran (mSubst‘𝑡)
29	25, 20, 28	wrex 2897	. . . . . . 7 wff ∃𝑠 ∈ ran (mSubst‘𝑡)𝑎 ∈ (𝑠 “ (mSA‘𝑡))
30	19, 29	wi 4	. . . . . 6 wff ((⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡)) → ∃𝑠 ∈ ran (mSubst‘𝑡)𝑎 ∈ (𝑠 “ (mSA‘𝑡)))
31	30, 6	wal 1473	. . . . 5 wff ∀𝑎((⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡)) → ∃𝑠 ∈ ran (mSubst‘𝑡)𝑎 ∈ (𝑠 “ (mSA‘𝑡)))
32	31, 4	wal 1473	. . . 4 wff ∀ℎ∀𝑎((⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡)) → ∃𝑠 ∈ ran (mSubst‘𝑡)𝑎 ∈ (𝑠 “ (mSA‘𝑡)))
33	32, 2	wal 1473	. . 3 wff ∀𝑑∀ℎ∀𝑎((⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡)) → ∃𝑠 ∈ ran (mSubst‘𝑡)𝑎 ∈ (𝑠 “ (mSA‘𝑡)))
34		cmfs 30627	. . 3 class mFS
35	33, 9, 34	crab 2900	. 2 class {𝑡 ∈ mFS ∣ ∀𝑑∀ℎ∀𝑎((⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡)) → ∃𝑠 ∈ ran (mSubst‘𝑡)𝑎 ∈ (𝑠 “ (mSA‘𝑡)))}
36	1, 35	wceq 1475	1 wff mWGFS = {𝑡 ∈ mFS ∣ ∀𝑑∀ℎ∀𝑎((⟨𝑑, ℎ, 𝑎⟩ ∈ (mAx‘𝑡) ∧ (1st ‘𝑎) ∈ (mVT‘𝑡)) → ∃𝑠 ∈ ran (mSubst‘𝑡)𝑎 ∈ (𝑠 “ (mSA‘𝑡)))}

This definition is referenced by: (None)