Metamath Proof Explorer

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 = t ∈ mFS | ∀ d ∀ h ∀ a d h a ∈ mAx ⁡ t ∧ 1 st ⁡ a ∈ mVT ⁡ t → ∃ s ∈ ran ⁡ mSubst ⁡ t a ∈ s mSA ⁡ t

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmwgfs class mWGFS
1 vt setvar t
2 cmfs class mFS
3 vd setvar d
4 vh setvar h
5 va setvar a
6 3 cv setvar d
7 4 cv setvar h
8 5 cv setvar a
9 6 7 8 cotp class d h a
10 cmax class mAx
11 1 cv setvar t
12 11 10 cfv class mAx ⁡ t
13 9 12 wcel wff d h a ∈ mAx ⁡ t
14 c1st class 1 st
15 8 14 cfv class 1 st ⁡ a
16 cmvt class mVT
17 11 16 cfv class mVT ⁡ t
18 15 17 wcel wff 1 st ⁡ a ∈ mVT ⁡ t
19 13 18 wa wff d h a ∈ mAx ⁡ t ∧ 1 st ⁡ a ∈ mVT ⁡ t
20 vs setvar s
21 cmsub class mSubst
22 11 21 cfv class mSubst ⁡ t
23 22 crn class ran ⁡ mSubst ⁡ t
24 20 cv setvar s
25 cmsa class mSA
26 11 25 cfv class mSA ⁡ t
27 24 26 cima class s mSA ⁡ t
28 8 27 wcel wff a ∈ s mSA ⁡ t
29 28 20 23 wrex wff ∃ s ∈ ran ⁡ mSubst ⁡ t a ∈ s mSA ⁡ t
30 19 29 wi wff d h a ∈ mAx ⁡ t ∧ 1 st ⁡ a ∈ mVT ⁡ t → ∃ s ∈ ran ⁡ mSubst ⁡ t a ∈ s mSA ⁡ t
31 30 5 wal wff ∀ a d h a ∈ mAx ⁡ t ∧ 1 st ⁡ a ∈ mVT ⁡ t → ∃ s ∈ ran ⁡ mSubst ⁡ t a ∈ s mSA ⁡ t
32 31 4 wal wff ∀ h ∀ a d h a ∈ mAx ⁡ t ∧ 1 st ⁡ a ∈ mVT ⁡ t → ∃ s ∈ ran ⁡ mSubst ⁡ t a ∈ s mSA ⁡ t
33 32 3 wal wff ∀ d ∀ h ∀ a d h a ∈ mAx ⁡ t ∧ 1 st ⁡ a ∈ mVT ⁡ t → ∃ s ∈ ran ⁡ mSubst ⁡ t a ∈ s mSA ⁡ t
34 33 1 2 crab class t ∈ mFS | ∀ d ∀ h ∀ a d h a ∈ mAx ⁡ t ∧ 1 st ⁡ a ∈ mVT ⁡ t → ∃ s ∈ ran ⁡ mSubst ⁡ t a ∈ s mSA ⁡ t
35 0 34 wceq wff mWGFS = t ∈ mFS | ∀ d ∀ h ∀ a d h a ∈ mAx ⁡ t ∧ 1 st ⁡ a ∈ mVT ⁡ t → ∃ s ∈ ran ⁡ mSubst ⁡ t a ∈ s mSA ⁡ t