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 = { 𝑡 ∈ mFS ∣ ∀ 𝑑 ∀ ℎ ∀ 𝑎 ( ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) ∧ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 ) ) → ∃ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) 𝑎 ∈ ( 𝑠 “ ( mSA ‘ 𝑡 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmwgfs	⊢ mWGFS
1		vt	⊢ 𝑡
2		cmfs	⊢ mFS
3		vd	⊢ 𝑑
4		vh	⊢ ℎ
5		va	⊢ 𝑎
6	3	cv	⊢ 𝑑
7	4	cv	⊢ ℎ
8	5	cv	⊢ 𝑎
9	6 7 8	cotp	⊢ ⟨ 𝑑 , ℎ , 𝑎 ⟩
10		cmax	⊢ mAx
11	1	cv	⊢ 𝑡
12	11 10	cfv	⊢ ( mAx ‘ 𝑡 )
13	9 12	wcel	⊢ ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 )
14		c1st	⊢ 1st
15	8 14	cfv	⊢ ( 1st ‘ 𝑎 )
16		cmvt	⊢ mVT
17	11 16	cfv	⊢ ( mVT ‘ 𝑡 )
18	15 17	wcel	⊢ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 )
19	13 18	wa	⊢ ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) ∧ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 ) )
20		vs	⊢ 𝑠
21		cmsub	⊢ mSubst
22	11 21	cfv	⊢ ( mSubst ‘ 𝑡 )
23	22	crn	⊢ ran ( mSubst ‘ 𝑡 )
24	20	cv	⊢ 𝑠
25		cmsa	⊢ mSA
26	11 25	cfv	⊢ ( mSA ‘ 𝑡 )
27	24 26	cima	⊢ ( 𝑠 “ ( mSA ‘ 𝑡 ) )
28	8 27	wcel	⊢ 𝑎 ∈ ( 𝑠 “ ( mSA ‘ 𝑡 ) )
29	28 20 23	wrex	⊢ ∃ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) 𝑎 ∈ ( 𝑠 “ ( mSA ‘ 𝑡 ) )
30	19 29	wi	⊢ ( ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) ∧ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 ) ) → ∃ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) 𝑎 ∈ ( 𝑠 “ ( mSA ‘ 𝑡 ) ) )
31	30 5	wal	⊢ ∀ 𝑎 ( ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) ∧ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 ) ) → ∃ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) 𝑎 ∈ ( 𝑠 “ ( mSA ‘ 𝑡 ) ) )
32	31 4	wal	⊢ ∀ ℎ ∀ 𝑎 ( ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) ∧ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 ) ) → ∃ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) 𝑎 ∈ ( 𝑠 “ ( mSA ‘ 𝑡 ) ) )
33	32 3	wal	⊢ ∀ 𝑑 ∀ ℎ ∀ 𝑎 ( ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) ∧ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 ) ) → ∃ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) 𝑎 ∈ ( 𝑠 “ ( mSA ‘ 𝑡 ) ) )
34	33 1 2	crab	⊢ { 𝑡 ∈ mFS ∣ ∀ 𝑑 ∀ ℎ ∀ 𝑎 ( ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) ∧ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 ) ) → ∃ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) 𝑎 ∈ ( 𝑠 “ ( mSA ‘ 𝑡 ) ) ) }
35	0 34	wceq	⊢ mWGFS = { 𝑡 ∈ mFS ∣ ∀ 𝑑 ∀ ℎ ∀ 𝑎 ( ( ⟨ 𝑑 , ℎ , 𝑎 ⟩ ∈ ( mAx ‘ 𝑡 ) ∧ ( 1st ‘ 𝑎 ) ∈ ( mVT ‘ 𝑡 ) ) → ∃ 𝑠 ∈ ran ( mSubst ‘ 𝑡 ) 𝑎 ∈ ( 𝑠 “ ( mSA ‘ 𝑡 ) ) ) }