Metamath Proof Explorer

Definition df-mfs

Description: Define the set of all formal systems. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion df-mfs ⊢mFS=t|mCN⁡t∩mVR⁡t=∅∧mType⁡t:mVR⁡t⟶mTC⁡t∧mAx⁡t⊆mStat⁡t∧∀v∈mVT⁡t¬mType⁡t-1v∈Fin

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmfs classmFS
1 vt setvart
2 cmcn classmCN
3 1 cv setvart
4 3 2 cfv classmCN⁡t
5 cmvar classmVR
6 3 5 cfv classmVR⁡t
7 4 6 cin classmCN⁡t∩mVR⁡t
8 c0 class∅
9 7 8 wceq wffmCN⁡t∩mVR⁡t=∅
10 cmty classmType
11 3 10 cfv classmType⁡t
12 cmtc classmTC
13 3 12 cfv classmTC⁡t
14 6 13 11 wf wffmType⁡t:mVR⁡t⟶mTC⁡t
15 9 14 wa wffmCN⁡t∩mVR⁡t=∅∧mType⁡t:mVR⁡t⟶mTC⁡t
16 cmax classmAx
17 3 16 cfv classmAx⁡t
18 cmsta classmStat
19 3 18 cfv classmStat⁡t
20 17 19 wss wffmAx⁡t⊆mStat⁡t
21 vv setvarv
22 cmvt classmVT
23 3 22 cfv classmVT⁡t
24 11 ccnv classmType⁡t-1
25 21 cv setvarv
26 25 csn classv
27 24 26 cima classmType⁡t-1v
28 cfn classFin
29 27 28 wcel wffmType⁡t-1v∈Fin
30 29 wn wff¬mType⁡t-1v∈Fin
31 30 21 23 wral wff∀v∈mVT⁡t¬mType⁡t-1v∈Fin
32 20 31 wa wffmAx⁡t⊆mStat⁡t∧∀v∈mVT⁡t¬mType⁡t-1v∈Fin
33 15 32 wa wffmCN⁡t∩mVR⁡t=∅∧mType⁡t:mVR⁡t⟶mTC⁡t∧mAx⁡t⊆mStat⁡t∧∀v∈mVT⁡t¬mType⁡t-1v∈Fin
34 33 1 cab classt|mCN⁡t∩mVR⁡t=∅∧mType⁡t:mVR⁡t⟶mTC⁡t∧mAx⁡t⊆mStat⁡t∧∀v∈mVT⁡t¬mType⁡t-1v∈Fin
35 0 34 wceq wffmFS=t|mCN⁡t∩mVR⁡t=∅∧mType⁡t:mVR⁡t⟶mTC⁡t∧mAx⁡t⊆mStat⁡t∧∀v∈mVT⁡t¬mType⁡t-1v∈Fin