Metamath Proof Explorer

Definition df-mgfs

Description: Define the set of grammatical formal systems. (Contributed by Mario Carneiro, 12-Jun-2023)

Ref Expression
Assertion df-mgfs ⊢mGFS=t∈mWGFS|mSyn⁡t:mTC⁡t⟶mVT⁡t∧∀c∈mVT⁡tmSyn⁡t⁡c=c∧∀d∀h∀adha∈mAx⁡t→∀e∈h∪amESyn⁡t⁡e∈mPPSt⁡t

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgfs classmGFS
1 vt setvart
2 cmwgfs classmWGFS
3 cmsy classmSyn
4 1 cv setvart
5 4 3 cfv classmSyn⁡t
6 cmtc classmTC
7 4 6 cfv classmTC⁡t
8 cmvt classmVT
9 4 8 cfv classmVT⁡t
10 7 9 5 wf wffmSyn⁡t:mTC⁡t⟶mVT⁡t
11 vc setvarc
12 11 cv setvarc
13 12 5 cfv classmSyn⁡t⁡c
14 13 12 wceq wffmSyn⁡t⁡c=c
15 14 11 9 wral wff∀c∈mVT⁡tmSyn⁡t⁡c=c
16 vd setvard
17 vh setvarh
18 va setvara
19 16 cv setvard
20 17 cv setvarh
21 18 cv setvara
22 19 20 21 cotp classdha
23 cmax classmAx
24 4 23 cfv classmAx⁡t
25 22 24 wcel wffdha∈mAx⁡t
26 ve setvare
27 21 csn classa
28 20 27 cun classh∪a
29 cmesy classmESyn
30 4 29 cfv classmESyn⁡t
31 26 cv setvare
32 31 30 cfv classmESyn⁡t⁡e
33 cmpps classmPPSt
34 4 33 cfv classmPPSt⁡t
35 32 34 wcel wffmESyn⁡t⁡e∈mPPSt⁡t
36 35 26 28 wral wff∀e∈h∪amESyn⁡t⁡e∈mPPSt⁡t
37 25 36 wi wffdha∈mAx⁡t→∀e∈h∪amESyn⁡t⁡e∈mPPSt⁡t
38 37 18 wal wff∀adha∈mAx⁡t→∀e∈h∪amESyn⁡t⁡e∈mPPSt⁡t
39 38 17 wal wff∀h∀adha∈mAx⁡t→∀e∈h∪amESyn⁡t⁡e∈mPPSt⁡t
40 39 16 wal wff∀d∀h∀adha∈mAx⁡t→∀e∈h∪amESyn⁡t⁡e∈mPPSt⁡t
41 10 15 40 w3a wffmSyn⁡t:mTC⁡t⟶mVT⁡t∧∀c∈mVT⁡tmSyn⁡t⁡c=c∧∀d∀h∀adha∈mAx⁡t→∀e∈h∪amESyn⁡t⁡e∈mPPSt⁡t
42 41 1 2 crab classt∈mWGFS|mSyn⁡t:mTC⁡t⟶mVT⁡t∧∀c∈mVT⁡tmSyn⁡t⁡c=c∧∀d∀h∀adha∈mAx⁡t→∀e∈h∪amESyn⁡t⁡e∈mPPSt⁡t
43 0 42 wceq wffmGFS=t∈mWGFS|mSyn⁡t:mTC⁡t⟶mVT⁡t∧∀c∈mVT⁡tmSyn⁡t⁡c=c∧∀d∀h∀adha∈mAx⁡t→∀e∈h∪amESyn⁡t⁡e∈mPPSt⁡t