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 -1 v ∈ Fin

Detailed syntax breakdown

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