Definition df-mwgfs 31494

Description: Define the set of weakly grammatical formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.)

Assertion

Ref	Expression
df-mwgfs	|- mWGFS = { t e. mFS | A. d A. h A. a ( ( <. d , h , a >. e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) ) -> E. s e. ran (mSubst ` t ) a e. ( s " (mSA ` t ) ) ) }

Distinct variable group:   a, d, h, s, t

Detailed syntax breakdown of Definition df-mwgfs

Step	Hyp	Ref	Expression
1		cmwgfs 31484	. 2 class mWGFS
2		vd	. . . . . . . . . . 11 setvar d
3	2	cv 1482	. . . . . . . . . 10 class d
4		vh	. . . . . . . . . . 11 setvar h
5	4	cv 1482	. . . . . . . . . 10 class h
6		va	. . . . . . . . . . 11 setvar a
7	6	cv 1482	. . . . . . . . . 10 class a
8	3, 5, 7	cotp 4185	. . . . . . . . 9 class <. d , h , a >.
9		vt	. . . . . . . . . . 11 setvar t
10	9	cv 1482	. . . . . . . . . 10 class t
11		cmax 31362	. . . . . . . . . 10 class mAx
12	10, 11	cfv 5888	. . . . . . . . 9 class (mAx ` t )
13	8, 12	wcel 1990	. . . . . . . 8 wff <. d , h , a >. e. (mAx ` t )
14		c1st 7166	. . . . . . . . . 10 class 1st
15	7, 14	cfv 5888	. . . . . . . . 9 class ( 1st ` a )
16		cmvt 31360	. . . . . . . . . 10 class mVT
17	10, 16	cfv 5888	. . . . . . . . 9 class (mVT ` t )
18	15, 17	wcel 1990	. . . . . . . 8 wff ( 1st ` a ) e. (mVT ` t )
19	13, 18	wa 384	. . . . . . 7 wff ( <. d , h , a >. e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) )
20		vs	. . . . . . . . . . 11 setvar s
21	20	cv 1482	. . . . . . . . . 10 class s
22		cmsa 31483	. . . . . . . . . . 11 class mSA
23	10, 22	cfv 5888	. . . . . . . . . 10 class (mSA ` t )
24	21, 23	cima 5117	. . . . . . . . 9 class ( s " (mSA ` t ) )
25	7, 24	wcel 1990	. . . . . . . 8 wff a e. ( s " (mSA ` t ) )
26		cmsub 31368	. . . . . . . . . 10 class mSubst
27	10, 26	cfv 5888	. . . . . . . . 9 class (mSubst ` t )
28	27	crn 5115	. . . . . . . 8 class ran (mSubst ` t )
29	25, 20, 28	wrex 2913	. . . . . . 7 wff E. s e. ran (mSubst ` t ) a e. ( s " (mSA ` t ) )
30	19, 29	wi 4	. . . . . 6 wff ( ( <. d , h , a >. e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) ) -> E. s e. ran (mSubst ` t ) a e. ( s " (mSA ` t ) ) )
31	30, 6	wal 1481	. . . . 5 wff A. a ( ( <. d , h , a >. e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) ) -> E. s e. ran (mSubst ` t ) a e. ( s " (mSA ` t ) ) )
32	31, 4	wal 1481	. . . 4 wff A. h A. a ( ( <. d , h , a >. e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) ) -> E. s e. ran (mSubst ` t ) a e. ( s " (mSA ` t ) ) )
33	32, 2	wal 1481	. . 3 wff A. d A. h A. a ( ( <. d , h , a >. e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) ) -> E. s e. ran (mSubst ` t ) a e. ( s " (mSA ` t ) ) )
34		cmfs 31373	. . 3 class mFS
35	33, 9, 34	crab 2916	. 2 class { t e. mFS | A. d A. h A. a ( ( <. d , h , a >. e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) ) -> E. s e. ran (mSubst ` t ) a e. ( s " (mSA ` t ) ) ) }
36	1, 35	wceq 1483	1 wff mWGFS = { t e. mFS | A. d A. h A. a ( ( <. d , h , a >. e. (mAx ` t ) /\ ( 1st ` a ) e. (mVT ` t ) ) -> E. s e. ran (mSubst ` t ) a e. ( s " (mSA ` t ) ) ) }

This definition is referenced by: (None)