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∀adha∈mAx⁡t∧1st⁡a∈mVT⁡t→∃s∈ran⁡mSubst⁡ta∈smSA⁡t

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmwgfs classmWGFS
1 vt setvart
2 cmfs classmFS
3 vd setvard
4 vh setvarh
5 va setvara
6 3 cv setvard
7 4 cv setvarh
8 5 cv setvara
9 6 7 8 cotp classdha
10 cmax classmAx
11 1 cv setvart
12 11 10 cfv classmAx⁡t
13 9 12 wcel wffdha∈mAx⁡t
14 c1st class1st
15 8 14 cfv class1st⁡a
16 cmvt classmVT
17 11 16 cfv classmVT⁡t
18 15 17 wcel wff1st⁡a∈mVT⁡t
19 13 18 wa wffdha∈mAx⁡t∧1st⁡a∈mVT⁡t
20 vs setvars
21 cmsub classmSubst
22 11 21 cfv classmSubst⁡t
23 22 crn classran⁡mSubst⁡t
24 20 cv setvars
25 cmsa classmSA
26 11 25 cfv classmSA⁡t
27 24 26 cima classsmSA⁡t
28 8 27 wcel wffa∈smSA⁡t
29 28 20 23 wrex wff∃s∈ran⁡mSubst⁡ta∈smSA⁡t
30 19 29 wi wffdha∈mAx⁡t∧1st⁡a∈mVT⁡t→∃s∈ran⁡mSubst⁡ta∈smSA⁡t
31 30 5 wal wff∀adha∈mAx⁡t∧1st⁡a∈mVT⁡t→∃s∈ran⁡mSubst⁡ta∈smSA⁡t
32 31 4 wal wff∀h∀adha∈mAx⁡t∧1st⁡a∈mVT⁡t→∃s∈ran⁡mSubst⁡ta∈smSA⁡t
33 32 3 wal wff∀d∀h∀adha∈mAx⁡t∧1st⁡a∈mVT⁡t→∃s∈ran⁡mSubst⁡ta∈smSA⁡t
34 33 1 2 crab classt∈mFS|∀d∀h∀adha∈mAx⁡t∧1st⁡a∈mVT⁡t→∃s∈ran⁡mSubst⁡ta∈smSA⁡t
35 0 34 wceq wffmWGFS=t∈mFS|∀d∀h∀adha∈mAx⁡t∧1st⁡a∈mVT⁡t→∃s∈ran⁡mSubst⁡ta∈smSA⁡t