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 e. mWGFS | ( ( mSyn ` t ) : ( mTC ` t ) --> ( mVT ` t ) /\ A. c e. ( mVT ` t ) ( ( mSyn ` t ) ` c ) = c /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> A. e e. ( h u. { a } ) ( ( mESyn ` t ) ` e ) e. ( mPPSt ` t ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgfs 
 |-  mGFS
1 vt 
 |-  t
2 cmwgfs 
 |-  mWGFS
3 cmsy 
 |-  mSyn
4 1 cv 
 |-  t
5 4 3 cfv 
 |-  ( mSyn ` t )
6 cmtc 
 |-  mTC
7 4 6 cfv 
 |-  ( mTC ` t )
8 cmvt 
 |-  mVT
9 4 8 cfv 
 |-  ( mVT ` t )
10 7 9 5 wf 
 |-  ( mSyn ` t ) : ( mTC ` t ) --> ( mVT ` t )
11 vc 
 |-  c
12 11 cv 
 |-  c
13 12 5 cfv 
 |-  ( ( mSyn ` t ) ` c )
14 13 12 wceq 
 |-  ( ( mSyn ` t ) ` c ) = c
15 14 11 9 wral 
 |-  A. c e. ( mVT ` t ) ( ( mSyn ` t ) ` c ) = c
16 vd 
 |-  d
17 vh 
 |-  h
18 va 
 |-  a
19 16 cv 
 |-  d
20 17 cv 
 |-  h
21 18 cv 
 |-  a
22 19 20 21 cotp 
 |-  <. d , h , a >.
23 cmax 
 |-  mAx
24 4 23 cfv 
 |-  ( mAx ` t )
25 22 24 wcel 
 |-  <. d , h , a >. e. ( mAx ` t )
26 ve 
 |-  e
27 21 csn 
 |-  { a }
28 20 27 cun 
 |-  ( h u. { a } )
29 cmesy 
 |-  mESyn
30 4 29 cfv 
 |-  ( mESyn ` t )
31 26 cv 
 |-  e
32 31 30 cfv 
 |-  ( ( mESyn ` t ) ` e )
33 cmpps 
 |-  mPPSt
34 4 33 cfv 
 |-  ( mPPSt ` t )
35 32 34 wcel 
 |-  ( ( mESyn ` t ) ` e ) e. ( mPPSt ` t )
36 35 26 28 wral 
 |-  A. e e. ( h u. { a } ) ( ( mESyn ` t ) ` e ) e. ( mPPSt ` t )
37 25 36 wi 
 |-  ( <. d , h , a >. e. ( mAx ` t ) -> A. e e. ( h u. { a } ) ( ( mESyn ` t ) ` e ) e. ( mPPSt ` t ) )
38 37 18 wal 
 |-  A. a ( <. d , h , a >. e. ( mAx ` t ) -> A. e e. ( h u. { a } ) ( ( mESyn ` t ) ` e ) e. ( mPPSt ` t ) )
39 38 17 wal 
 |-  A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> A. e e. ( h u. { a } ) ( ( mESyn ` t ) ` e ) e. ( mPPSt ` t ) )
40 39 16 wal 
 |-  A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> A. e e. ( h u. { a } ) ( ( mESyn ` t ) ` e ) e. ( mPPSt ` t ) )
41 10 15 40 w3a 
 |-  ( ( mSyn ` t ) : ( mTC ` t ) --> ( mVT ` t ) /\ A. c e. ( mVT ` t ) ( ( mSyn ` t ) ` c ) = c /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> A. e e. ( h u. { a } ) ( ( mESyn ` t ) ` e ) e. ( mPPSt ` t ) ) )
42 41 1 2 crab 
 |-  { t e. mWGFS | ( ( mSyn ` t ) : ( mTC ` t ) --> ( mVT ` t ) /\ A. c e. ( mVT ` t ) ( ( mSyn ` t ) ` c ) = c /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> A. e e. ( h u. { a } ) ( ( mESyn ` t ) ` e ) e. ( mPPSt ` t ) ) ) }
43 0 42 wceq 
 |-  mGFS = { t e. mWGFS | ( ( mSyn ` t ) : ( mTC ` t ) --> ( mVT ` t ) /\ A. c e. ( mVT ` t ) ( ( mSyn ` t ) ` c ) = c /\ A. d A. h A. a ( <. d , h , a >. e. ( mAx ` t ) -> A. e e. ( h u. { a } ) ( ( mESyn ` t ) ` e ) e. ( mPPSt ` t ) ) ) }