# 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 ${⊢}\mathrm{mFS}=\left\{{t}|\left(\left(\mathrm{mCN}\left({t}\right)\cap \mathrm{mVR}\left({t}\right)=\varnothing \wedge \mathrm{mType}\left({t}\right):\mathrm{mVR}\left({t}\right)⟶\mathrm{mTC}\left({t}\right)\right)\wedge \left(\mathrm{mAx}\left({t}\right)\subseteq \mathrm{mStat}\left({t}\right)\wedge \forall {v}\in \mathrm{mVT}\left({t}\right)\phantom{\rule{.4em}{0ex}}¬{\mathrm{mType}\left({t}\right)}^{-1}\left[\left\{{v}\right\}\right]\in \mathrm{Fin}\right)\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cmfs ${class}\mathrm{mFS}$
1 vt ${setvar}{t}$
2 cmcn ${class}\mathrm{mCN}$
3 1 cv ${setvar}{t}$
4 3 2 cfv ${class}\mathrm{mCN}\left({t}\right)$
5 cmvar ${class}\mathrm{mVR}$
6 3 5 cfv ${class}\mathrm{mVR}\left({t}\right)$
7 4 6 cin ${class}\left(\mathrm{mCN}\left({t}\right)\cap \mathrm{mVR}\left({t}\right)\right)$
8 c0 ${class}\varnothing$
9 7 8 wceq ${wff}\mathrm{mCN}\left({t}\right)\cap \mathrm{mVR}\left({t}\right)=\varnothing$
10 cmty ${class}\mathrm{mType}$
11 3 10 cfv ${class}\mathrm{mType}\left({t}\right)$
12 cmtc ${class}\mathrm{mTC}$
13 3 12 cfv ${class}\mathrm{mTC}\left({t}\right)$
14 6 13 11 wf ${wff}\mathrm{mType}\left({t}\right):\mathrm{mVR}\left({t}\right)⟶\mathrm{mTC}\left({t}\right)$
15 9 14 wa ${wff}\left(\mathrm{mCN}\left({t}\right)\cap \mathrm{mVR}\left({t}\right)=\varnothing \wedge \mathrm{mType}\left({t}\right):\mathrm{mVR}\left({t}\right)⟶\mathrm{mTC}\left({t}\right)\right)$
16 cmax ${class}\mathrm{mAx}$
17 3 16 cfv ${class}\mathrm{mAx}\left({t}\right)$
18 cmsta ${class}\mathrm{mStat}$
19 3 18 cfv ${class}\mathrm{mStat}\left({t}\right)$
20 17 19 wss ${wff}\mathrm{mAx}\left({t}\right)\subseteq \mathrm{mStat}\left({t}\right)$
21 vv ${setvar}{v}$
22 cmvt ${class}\mathrm{mVT}$
23 3 22 cfv ${class}\mathrm{mVT}\left({t}\right)$
24 11 ccnv ${class}{\mathrm{mType}\left({t}\right)}^{-1}$
25 21 cv ${setvar}{v}$
26 25 csn ${class}\left\{{v}\right\}$
27 24 26 cima ${class}{\mathrm{mType}\left({t}\right)}^{-1}\left[\left\{{v}\right\}\right]$
28 cfn ${class}\mathrm{Fin}$
29 27 28 wcel ${wff}{\mathrm{mType}\left({t}\right)}^{-1}\left[\left\{{v}\right\}\right]\in \mathrm{Fin}$
30 29 wn ${wff}¬{\mathrm{mType}\left({t}\right)}^{-1}\left[\left\{{v}\right\}\right]\in \mathrm{Fin}$
31 30 21 23 wral ${wff}\forall {v}\in \mathrm{mVT}\left({t}\right)\phantom{\rule{.4em}{0ex}}¬{\mathrm{mType}\left({t}\right)}^{-1}\left[\left\{{v}\right\}\right]\in \mathrm{Fin}$
32 20 31 wa ${wff}\left(\mathrm{mAx}\left({t}\right)\subseteq \mathrm{mStat}\left({t}\right)\wedge \forall {v}\in \mathrm{mVT}\left({t}\right)\phantom{\rule{.4em}{0ex}}¬{\mathrm{mType}\left({t}\right)}^{-1}\left[\left\{{v}\right\}\right]\in \mathrm{Fin}\right)$
33 15 32 wa ${wff}\left(\left(\mathrm{mCN}\left({t}\right)\cap \mathrm{mVR}\left({t}\right)=\varnothing \wedge \mathrm{mType}\left({t}\right):\mathrm{mVR}\left({t}\right)⟶\mathrm{mTC}\left({t}\right)\right)\wedge \left(\mathrm{mAx}\left({t}\right)\subseteq \mathrm{mStat}\left({t}\right)\wedge \forall {v}\in \mathrm{mVT}\left({t}\right)\phantom{\rule{.4em}{0ex}}¬{\mathrm{mType}\left({t}\right)}^{-1}\left[\left\{{v}\right\}\right]\in \mathrm{Fin}\right)\right)$
34 33 1 cab ${class}\left\{{t}|\left(\left(\mathrm{mCN}\left({t}\right)\cap \mathrm{mVR}\left({t}\right)=\varnothing \wedge \mathrm{mType}\left({t}\right):\mathrm{mVR}\left({t}\right)⟶\mathrm{mTC}\left({t}\right)\right)\wedge \left(\mathrm{mAx}\left({t}\right)\subseteq \mathrm{mStat}\left({t}\right)\wedge \forall {v}\in \mathrm{mVT}\left({t}\right)\phantom{\rule{.4em}{0ex}}¬{\mathrm{mType}\left({t}\right)}^{-1}\left[\left\{{v}\right\}\right]\in \mathrm{Fin}\right)\right)\right\}$
35 0 34 wceq ${wff}\mathrm{mFS}=\left\{{t}|\left(\left(\mathrm{mCN}\left({t}\right)\cap \mathrm{mVR}\left({t}\right)=\varnothing \wedge \mathrm{mType}\left({t}\right):\mathrm{mVR}\left({t}\right)⟶\mathrm{mTC}\left({t}\right)\right)\wedge \left(\mathrm{mAx}\left({t}\right)\subseteq \mathrm{mStat}\left({t}\right)\wedge \forall {v}\in \mathrm{mVT}\left({t}\right)\phantom{\rule{.4em}{0ex}}¬{\mathrm{mType}\left({t}\right)}^{-1}\left[\left\{{v}\right\}\right]\in \mathrm{Fin}\right)\right)\right\}$