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 = { 𝑡 ∈ ( mGFS ∩ mMdl ) ∣ ( ∀ 𝑐 ∈ ( mTC ‘ 𝑡 ) ( ( mUV ‘ 𝑡 ) “ { 𝑐 } ) ⊆ ( ( mUV ‘ 𝑡 ) “ { ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) } ) ∧ ∀ 𝑣 ∈ ( mUV ‘ 𝑐 ) ∀ 𝑤 ∈ ( mUV ‘ 𝑐 ) ( 𝑣 ( mFresh ‘ 𝑡 ) 𝑤 ↔ 𝑣 ( mFresh ‘ 𝑡 ) ( ( mUSyn ‘ 𝑡 ) ‘ 𝑤 ) ) ∧ ∀ 𝑚 ∈ ( mVL ‘ 𝑡 ) ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgmdl	⊢ mGMdl
1		vt	⊢ 𝑡
2		cmgfs	⊢ mGFS
3		cmdl	⊢ mMdl
4	2 3	cin	⊢ ( mGFS ∩ mMdl )
5		vc	⊢ 𝑐
6		cmtc	⊢ mTC
7	1	cv	⊢ 𝑡
8	7 6	cfv	⊢ ( mTC ‘ 𝑡 )
9		cmuv	⊢ mUV
10	7 9	cfv	⊢ ( mUV ‘ 𝑡 )
11	5	cv	⊢ 𝑐
12	11	csn	⊢ { 𝑐 }
13	10 12	cima	⊢ ( ( mUV ‘ 𝑡 ) “ { 𝑐 } )
14		cmsy	⊢ mSyn
15	7 14	cfv	⊢ ( mSyn ‘ 𝑡 )
16	11 15	cfv	⊢ ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 )
17	16	csn	⊢ { ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) }
18	10 17	cima	⊢ ( ( mUV ‘ 𝑡 ) “ { ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) } )
19	13 18	wss	⊢ ( ( mUV ‘ 𝑡 ) “ { 𝑐 } ) ⊆ ( ( mUV ‘ 𝑡 ) “ { ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) } )
20	19 5 8	wral	⊢ ∀ 𝑐 ∈ ( mTC ‘ 𝑡 ) ( ( mUV ‘ 𝑡 ) “ { 𝑐 } ) ⊆ ( ( mUV ‘ 𝑡 ) “ { ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) } )
21		vv	⊢ 𝑣
22	11 9	cfv	⊢ ( mUV ‘ 𝑐 )
23		vw	⊢ 𝑤
24	21	cv	⊢ 𝑣
25		cmfsh	⊢ mFresh
26	7 25	cfv	⊢ ( mFresh ‘ 𝑡 )
27	23	cv	⊢ 𝑤
28	24 27 26	wbr	⊢ 𝑣 ( mFresh ‘ 𝑡 ) 𝑤
29		cusyn	⊢ mUSyn
30	7 29	cfv	⊢ ( mUSyn ‘ 𝑡 )
31	27 30	cfv	⊢ ( ( mUSyn ‘ 𝑡 ) ‘ 𝑤 )
32	24 31 26	wbr	⊢ 𝑣 ( mFresh ‘ 𝑡 ) ( ( mUSyn ‘ 𝑡 ) ‘ 𝑤 )
33	28 32	wb	⊢ ( 𝑣 ( mFresh ‘ 𝑡 ) 𝑤 ↔ 𝑣 ( mFresh ‘ 𝑡 ) ( ( mUSyn ‘ 𝑡 ) ‘ 𝑤 ) )
34	33 23 22	wral	⊢ ∀ 𝑤 ∈ ( mUV ‘ 𝑐 ) ( 𝑣 ( mFresh ‘ 𝑡 ) 𝑤 ↔ 𝑣 ( mFresh ‘ 𝑡 ) ( ( mUSyn ‘ 𝑡 ) ‘ 𝑤 ) )
35	34 21 22	wral	⊢ ∀ 𝑣 ∈ ( mUV ‘ 𝑐 ) ∀ 𝑤 ∈ ( mUV ‘ 𝑐 ) ( 𝑣 ( mFresh ‘ 𝑡 ) 𝑤 ↔ 𝑣 ( mFresh ‘ 𝑡 ) ( ( mUSyn ‘ 𝑡 ) ‘ 𝑤 ) )
36		vm	⊢ 𝑚
37		cmvl	⊢ mVL
38	7 37	cfv	⊢ ( mVL ‘ 𝑡 )
39		ve	⊢ 𝑒
40		cmex	⊢ mEx
41	7 40	cfv	⊢ ( mEx ‘ 𝑡 )
42		cmevl	⊢ mEval
43	7 42	cfv	⊢ ( mEval ‘ 𝑡 )
44	36	cv	⊢ 𝑚
45	39	cv	⊢ 𝑒
46	44 45	cop	⊢ ⟨ 𝑚 , 𝑒 ⟩
47	46	csn	⊢ { ⟨ 𝑚 , 𝑒 ⟩ }
48	43 47	cima	⊢ ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , 𝑒 ⟩ } )
49		cmesy	⊢ mESyn
50	7 49	cfv	⊢ ( mESyn ‘ 𝑡 )
51	45 50	cfv	⊢ ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 )
52	44 51	cop	⊢ ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩
53	52	csn	⊢ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ }
54	43 53	cima	⊢ ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } )
55		c1st	⊢ 1st
56	45 55	cfv	⊢ ( 1st ‘ 𝑒 )
57	56	csn	⊢ { ( 1st ‘ 𝑒 ) }
58	10 57	cima	⊢ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } )
59	54 58	cin	⊢ ( ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) )
60	48 59	wceq	⊢ ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) )
61	60 39 41	wral	⊢ ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) )
62	61 36 38	wral	⊢ ∀ 𝑚 ∈ ( mVL ‘ 𝑡 ) ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) )
63	20 35 62	w3a	⊢ ( ∀ 𝑐 ∈ ( mTC ‘ 𝑡 ) ( ( mUV ‘ 𝑡 ) “ { 𝑐 } ) ⊆ ( ( mUV ‘ 𝑡 ) “ { ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) } ) ∧ ∀ 𝑣 ∈ ( mUV ‘ 𝑐 ) ∀ 𝑤 ∈ ( mUV ‘ 𝑐 ) ( 𝑣 ( mFresh ‘ 𝑡 ) 𝑤 ↔ 𝑣 ( mFresh ‘ 𝑡 ) ( ( mUSyn ‘ 𝑡 ) ‘ 𝑤 ) ) ∧ ∀ 𝑚 ∈ ( mVL ‘ 𝑡 ) ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) ) )
64	63 1 4	crab	⊢ { 𝑡 ∈ ( mGFS ∩ mMdl ) ∣ ( ∀ 𝑐 ∈ ( mTC ‘ 𝑡 ) ( ( mUV ‘ 𝑡 ) “ { 𝑐 } ) ⊆ ( ( mUV ‘ 𝑡 ) “ { ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) } ) ∧ ∀ 𝑣 ∈ ( mUV ‘ 𝑐 ) ∀ 𝑤 ∈ ( mUV ‘ 𝑐 ) ( 𝑣 ( mFresh ‘ 𝑡 ) 𝑤 ↔ 𝑣 ( mFresh ‘ 𝑡 ) ( ( mUSyn ‘ 𝑡 ) ‘ 𝑤 ) ) ∧ ∀ 𝑚 ∈ ( mVL ‘ 𝑡 ) ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) ) ) }
65	0 64	wceq	⊢ mGMdl = { 𝑡 ∈ ( mGFS ∩ mMdl ) ∣ ( ∀ 𝑐 ∈ ( mTC ‘ 𝑡 ) ( ( mUV ‘ 𝑡 ) “ { 𝑐 } ) ⊆ ( ( mUV ‘ 𝑡 ) “ { ( ( mSyn ‘ 𝑡 ) ‘ 𝑐 ) } ) ∧ ∀ 𝑣 ∈ ( mUV ‘ 𝑐 ) ∀ 𝑤 ∈ ( mUV ‘ 𝑐 ) ( 𝑣 ( mFresh ‘ 𝑡 ) 𝑤 ↔ 𝑣 ( mFresh ‘ 𝑡 ) ( ( mUSyn ‘ 𝑡 ) ‘ 𝑤 ) ) ∧ ∀ 𝑚 ∈ ( mVL ‘ 𝑡 ) ∀ 𝑒 ∈ ( mEx ‘ 𝑡 ) ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , 𝑒 ⟩ } ) = ( ( ( mEval ‘ 𝑡 ) “ { ⟨ 𝑚 , ( ( mESyn ‘ 𝑡 ) ‘ 𝑒 ) ⟩ } ) ∩ ( ( mUV ‘ 𝑡 ) “ { ( 1st ‘ 𝑒 ) } ) ) ) }