Metamath Proof Explorer

Definition df-mwgfs

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

Ref Expression
Assertion 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 ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmwgfs 
 |-  mWGFS
1 vt 
 |-  t
2 cmfs 
 |-  mFS
3 vd 
 |-  d
4 vh 
 |-  h
5 va 
 |-  a
6 3 cv 
 |-  d
7 4 cv 
 |-  h
8 5 cv 
 |-  a
9 6 7 8 cotp 
 |-  <. d , h , a >.
10 cmax 
 |-  mAx
11 1 cv 
 |-  t
12 11 10 cfv 
 |-  ( mAx ` t )
13 9 12 wcel 
 |-  <. d , h , a >. e. ( mAx ` t )
14 c1st 
 |-  1st
15 8 14 cfv 
 |-  ( 1st ` a )
16 cmvt 
 |-  mVT
17 11 16 cfv 
 |-  ( mVT ` t )
18 15 17 wcel 
 |-  ( 1st ` a ) e. ( mVT ` t )
19 13 18 wa 
 |-  ( <. d , h , a >. e. ( mAx ` t ) /\ ( 1st ` a ) e. ( mVT ` t ) )
20 vs 
 |-  s
21 cmsub 
 |-  mSubst
22 11 21 cfv 
 |-  ( mSubst ` t )
23 22 crn 
 |-  ran ( mSubst ` t )
24 20 cv 
 |-  s
25 cmsa 
 |-  mSA
26 11 25 cfv 
 |-  ( mSA ` t )
27 24 26 cima 
 |-  ( s " ( mSA ` t ) )
28 8 27 wcel 
 |-  a e. ( s " ( mSA ` t ) )
29 28 20 23 wrex 
 |-  E. s e. ran ( mSubst ` t ) a e. ( s " ( mSA ` t ) )
30 19 29 wi 
 |-  ( ( <. d , h , a >. e. ( mAx ` t ) /\ ( 1st ` a ) e. ( mVT ` t ) ) -> E. s e. ran ( mSubst ` t ) a e. ( s " ( mSA ` t ) ) )
31 30 5 wal 
 |-  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 
 |-  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 3 wal 
 |-  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 33 1 2 crab 
 |-  { 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 ) ) ) }
35 0 34 wceq 
 |-  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 ) ) ) }