Definition df-gmdl 31519

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

Assertion

Ref

Expression

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 ) } ) ) ) }

Distinct variable group:   e, c, m, t, v, w

Detailed syntax breakdown of Definition df-gmdl

Step	Hyp	Ref	Expression
1		cgmdl 31508	. 2 class mGMdl
2		vt	. . . . . . . . 9 setvar t
3	2	cv 1482	. . . . . . . 8 class t
4		cmuv 31500	. . . . . . . 8 class mUV
5	3, 4	cfv 5888	. . . . . . 7 class (mUV ` t )
6		vc	. . . . . . . . 9 setvar c
7	6	cv 1482	. . . . . . . 8 class c
8	7	csn 4177	. . . . . . 7 class { c }
9	5, 8	cima 5117	. . . . . 6 class ( (mUV ` t ) " { c } )
10		cmsy 31485	. . . . . . . . . 10 class mSyn
11	3, 10	cfv 5888	. . . . . . . . 9 class (mSyn ` t )
12	7, 11	cfv 5888	. . . . . . . 8 class ( (mSyn ` t ) ` c )
13	12	csn 4177	. . . . . . 7 class { ( (mSyn ` t ) ` c ) }
14	5, 13	cima 5117	. . . . . 6 class ( (mUV ` t ) " { ( (mSyn ` t ) ` c ) } )
15	9, 14	wss 3574	. . . . 5 wff ( (mUV ` t ) " { c } ) C_ ( (mUV ` t ) " { ( (mSyn ` t ) ` c ) } )
16		cmtc 31361	. . . . . 6 class mTC
17	3, 16	cfv 5888	. . . . 5 class (mTC ` t )
18	15, 6, 17	wral 2912	. . . 4 wff A. c e. (mTC ` t ) ( (mUV ` t ) " { c } ) C_ ( (mUV ` t ) " { ( (mSyn ` t ) ` c ) } )
19		vv	. . . . . . . . 9 setvar v
20	19	cv 1482	. . . . . . . 8 class v
21		vw	. . . . . . . . 9 setvar w
22	21	cv 1482	. . . . . . . 8 class w
23		cmfsh 31503	. . . . . . . . 9 class mFresh
24	3, 23	cfv 5888	. . . . . . . 8 class (mFresh ` t )
25	20, 22, 24	wbr 4653	. . . . . . 7 wff v (mFresh ` t ) w
26		cusyn 31507	. . . . . . . . . 10 class mUSyn
27	3, 26	cfv 5888	. . . . . . . . 9 class (mUSyn ` t )
28	22, 27	cfv 5888	. . . . . . . 8 class ( (mUSyn ` t ) ` w )
29	20, 28, 24	wbr 4653	. . . . . . 7 wff v (mFresh ` t ) ( (mUSyn ` t ) ` w )
30	25, 29	wb 196	. . . . . 6 wff ( v (mFresh ` t ) w <-> v (mFresh ` t ) ( (mUSyn ` t ) ` w ) )
31	7, 4	cfv 5888	. . . . . 6 class (mUV ` c )
32	30, 21, 31	wral 2912	. . . . 5 wff A. w e. (mUV ` c ) ( v (mFresh ` t ) w <-> v (mFresh ` t ) ( (mUSyn ` t ) ` w ) )
33	32, 19, 31	wral 2912	. . . 4 wff A. v e. (mUV ` c ) A. w e. (mUV ` c ) ( v (mFresh ` t ) w <-> v (mFresh ` t ) ( (mUSyn ` t ) ` w ) )
34		cmevl 31505	. . . . . . . . 9 class mEval
35	3, 34	cfv 5888	. . . . . . . 8 class (mEval ` t )
36		vm	. . . . . . . . . . 11 setvar m
37	36	cv 1482	. . . . . . . . . 10 class m
38		ve	. . . . . . . . . . 11 setvar e
39	38	cv 1482	. . . . . . . . . 10 class e
40	37, 39	cop 4183	. . . . . . . . 9 class <. m , e >.
41	40	csn 4177	. . . . . . . 8 class { <. m , e >. }
42	35, 41	cima 5117	. . . . . . 7 class ( (mEval ` t ) " { <. m , e >. } )
43		cmesy 31486	. . . . . . . . . . . . 13 class mESyn
44	3, 43	cfv 5888	. . . . . . . . . . . 12 class (mESyn ` t )
45	39, 44	cfv 5888	. . . . . . . . . . 11 class ( (mESyn ` t ) ` e )
46	37, 45	cop 4183	. . . . . . . . . 10 class <. m , ( (mESyn ` t ) ` e ) >.
47	46	csn 4177	. . . . . . . . 9 class { <. m , ( (mESyn ` t ) ` e ) >. }
48	35, 47	cima 5117	. . . . . . . 8 class ( (mEval ` t ) " { <. m , ( (mESyn ` t ) ` e ) >. } )
49		c1st 7166	. . . . . . . . . . 11 class 1st
50	39, 49	cfv 5888	. . . . . . . . . 10 class ( 1st ` e )
51	50	csn 4177	. . . . . . . . 9 class { ( 1st ` e ) }
52	5, 51	cima 5117	. . . . . . . 8 class ( (mUV ` t ) " { ( 1st ` e ) } )
53	48, 52	cin 3573	. . . . . . 7 class ( ( (mEval ` t ) " { <. m , ( (mESyn ` t ) ` e ) >. } ) i^i ( (mUV ` t ) " { ( 1st ` e ) } ) )
54	42, 53	wceq 1483	. . . . . 6 wff ( (mEval ` t ) " { <. m , e >. } ) = ( ( (mEval ` t ) " { <. m , ( (mESyn ` t ) ` e ) >. } ) i^i ( (mUV ` t ) " { ( 1st ` e ) } ) )
55		cmex 31364	. . . . . . 7 class mEx
56	3, 55	cfv 5888	. . . . . 6 class (mEx ` t )
57	54, 38, 56	wral 2912	. . . . 5 wff A. e e. (mEx ` t ) ( (mEval ` t ) " { <. m , e >. } ) = ( ( (mEval ` t ) " { <. m , ( (mESyn ` t ) ` e ) >. } ) i^i ( (mUV ` t ) " { ( 1st ` e ) } ) )
58		cmvl 31501	. . . . . 6 class mVL
59	3, 58	cfv 5888	. . . . 5 class (mVL ` t )
60	57, 36, 59	wral 2912	. . . 4 wff 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 ) } ) )
61	18, 33, 60	w3a 1037	. . 3 wff ( 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 ) } ) ) )
62		cmgfs 31487	. . . 4 class mGFS
63		cmdl 31506	. . . 4 class mMdl
64	62, 63	cin 3573	. . 3 class (mGFS i^i mMdl )
65	61, 2, 64	crab 2916	. 2 class { 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 ) } ) ) ) }
66	1, 65	wceq 1483	1 wff 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 ) } ) ) ) }

This definition is referenced by: (None)