Metamath Proof Explorer

Definition df-gmdl

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

Ref Expression
Assertion df-gmdl 
|- mGMdl = { t e. ( mGFS i^i mMdl ) | ( A. c e. ( mTC ` t ) ( ( mUV ` t ) " { c } ) C_ ( ( mUV ` t ) " { ( ( mSyn ` t ) ` c ) } ) /\ A. v e. ( mUV ` c ) A. w e. ( mUV ` c ) ( v ( mFresh ` t ) w <-> v ( mFresh ` t ) ( ( mUSyn ` t ) ` w ) ) /\ A. m e. ( mVL ` t ) A. e e. ( mEx ` t ) ( ( mEval ` t ) " { <. m , e >. } ) = ( ( ( mEval ` t ) " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgmdl 
 |-  mGMdl
1 vt 
 |-  t
2 cmgfs 
 |-  mGFS
3 cmdl 
 |-  mMdl
4 2 3 cin 
 |-  ( mGFS i^i mMdl )
5 vc 
 |-  c
6 cmtc 
 |-  mTC
7 1 cv 
 |-  t
8 7 6 cfv 
 |-  ( mTC ` t )
9 cmuv 
 |-  mUV
10 7 9 cfv 
 |-  ( mUV ` t )
11 5 cv 
 |-  c
12 11 csn 
 |-  { c }
13 10 12 cima 
 |-  ( ( mUV ` t ) " { c } )
14 cmsy 
 |-  mSyn
15 7 14 cfv 
 |-  ( mSyn ` t )
16 11 15 cfv 
 |-  ( ( mSyn ` t ) ` c )
17 16 csn 
 |-  { ( ( mSyn ` t ) ` c ) }
18 10 17 cima 
 |-  ( ( mUV ` t ) " { ( ( mSyn ` t ) ` c ) } )
19 13 18 wss 
 |-  ( ( mUV ` t ) " { c } ) C_ ( ( mUV ` t ) " { ( ( mSyn ` t ) ` c ) } )
20 19 5 8 wral 
 |-  A. c e. ( mTC ` t ) ( ( mUV ` t ) " { c } ) C_ ( ( mUV ` t ) " { ( ( mSyn ` t ) ` c ) } )
21 vv 
 |-  v
22 11 9 cfv 
 |-  ( mUV ` c )
23 vw 
 |-  w
24 21 cv 
 |-  v
25 cmfsh 
 |-  mFresh
26 7 25 cfv 
 |-  ( mFresh ` t )
27 23 cv 
 |-  w
28 24 27 26 wbr 
 |-  v ( mFresh ` t ) w
29 cusyn 
 |-  mUSyn
30 7 29 cfv 
 |-  ( mUSyn ` t )
31 27 30 cfv 
 |-  ( ( mUSyn ` t ) ` w )
32 24 31 26 wbr 
 |-  v ( mFresh ` t ) ( ( mUSyn ` t ) ` w )
33 28 32 wb 
 |-  ( v ( mFresh ` t ) w <-> v ( mFresh ` t ) ( ( mUSyn ` t ) ` w ) )
34 33 23 22 wral 
 |-  A. w e. ( mUV ` c ) ( v ( mFresh ` t ) w <-> v ( mFresh ` t ) ( ( mUSyn ` t ) ` w ) )
35 34 21 22 wral 
 |-  A. v e. ( mUV ` c ) A. w e. ( mUV ` c ) ( v ( mFresh ` t ) w <-> v ( mFresh ` t ) ( ( mUSyn ` t ) ` w ) )
36 vm 
 |-  m
37 cmvl 
 |-  mVL
38 7 37 cfv 
 |-  ( mVL ` t )
39 ve 
 |-  e
40 cmex 
 |-  mEx
41 7 40 cfv 
 |-  ( mEx ` t )
42 cmevl 
 |-  mEval
43 7 42 cfv 
 |-  ( mEval ` t )
44 36 cv 
 |-  m
45 39 cv 
 |-  e
46 44 45 cop 
 |-  <. m , e >.
47 46 csn 
 |-  { <. m , e >. }
48 43 47 cima 
 |-  ( ( mEval ` t ) " { <. m , e >. } )
49 cmesy 
 |-  mESyn
50 7 49 cfv 
 |-  ( mESyn ` t )
51 45 50 cfv 
 |-  ( ( mESyn ` t ) ` e )
52 44 51 cop 
 |-  <. m , ( ( mESyn ` t ) ` e ) >.
53 52 csn 
 |-  { <. m , ( ( mESyn ` t ) ` e ) >. }
54 43 53 cima 
 |-  ( ( mEval ` t ) " { <. m , ( ( mESyn ` t ) ` e ) >. } )
55 c1st 
 |-  1st
56 45 55 cfv 
 |-  ( 1st ` e )
57 56 csn 
 |-  { ( 1st ` e ) }
58 10 57 cima 
 |-  ( ( mUV ` t ) " { ( 1st ` e ) } )
59 54 58 cin 
 |-  ( ( ( mEval ` t ) " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) )
60 48 59 wceq 
 |-  ( ( mEval ` t ) " { <. m , e >. } ) = ( ( ( mEval ` t ) " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) )
61 60 39 41 wral 
 |-  A. e e. ( mEx ` t ) ( ( mEval ` t ) " { <. m , e >. } ) = ( ( ( mEval ` t ) " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) )
62 61 36 38 wral 
 |-  A. m e. ( mVL ` t ) A. e e. ( mEx ` t ) ( ( mEval ` t ) " { <. m , e >. } ) = ( ( ( mEval ` t ) " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) )
63 20 35 62 w3a 
 |-  ( A. c e. ( mTC ` t ) ( ( mUV ` t ) " { c } ) C_ ( ( mUV ` t ) " { ( ( mSyn ` t ) ` c ) } ) /\ A. v e. ( mUV ` c ) A. w e. ( mUV ` c ) ( v ( mFresh ` t ) w <-> v ( mFresh ` t ) ( ( mUSyn ` t ) ` w ) ) /\ A. m e. ( mVL ` t ) A. e e. ( mEx ` t ) ( ( mEval ` t ) " { <. m , e >. } ) = ( ( ( mEval ` t ) " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) ) )
64 63 1 4 crab 
 |-  { t e. ( mGFS i^i mMdl ) | ( A. c e. ( mTC ` t ) ( ( mUV ` t ) " { c } ) C_ ( ( mUV ` t ) " { ( ( mSyn ` t ) ` c ) } ) /\ A. v e. ( mUV ` c ) A. w e. ( mUV ` c ) ( v ( mFresh ` t ) w <-> v ( mFresh ` t ) ( ( mUSyn ` t ) ` w ) ) /\ A. m e. ( mVL ` t ) A. e e. ( mEx ` t ) ( ( mEval ` t ) " { <. m , e >. } ) = ( ( ( mEval ` t ) " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) ) ) }
65 0 64 wceq 
 |-  mGMdl = { t e. ( mGFS i^i mMdl ) | ( A. c e. ( mTC ` t ) ( ( mUV ` t ) " { c } ) C_ ( ( mUV ` t ) " { ( ( mSyn ` t ) ` c ) } ) /\ A. v e. ( mUV ` c ) A. w e. ( mUV ` c ) ( v ( mFresh ` t ) w <-> v ( mFresh ` t ) ( ( mUSyn ` t ) ` w ) ) /\ A. m e. ( mVL ` t ) A. e e. ( mEx ` t ) ( ( mEval ` t ) " { <. m , e >. } ) = ( ( ( mEval ` t ) " { <. m , ( ( mESyn ` t ) ` e ) >. } ) i^i ( ( mUV ` t ) " { ( 1st ` e ) } ) ) ) }