Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mfs Structured version   Visualization version   GIF version

Definition df-mfs 31519
Description: Define the set of all formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mfs mFS = {𝑡 ∣ ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin))}
Distinct variable group:   𝑣,𝑡

Detailed syntax breakdown of Definition df-mfs
StepHypRef Expression
1 cmfs 31499 . 2 class mFS
2 vt . . . . . . . . 9 setvar 𝑡
32cv 1522 . . . . . . . 8 class 𝑡
4 cmcn 31483 . . . . . . . 8 class mCN
53, 4cfv 5926 . . . . . . 7 class (mCN‘𝑡)
6 cmvar 31484 . . . . . . . 8 class mVR
73, 6cfv 5926 . . . . . . 7 class (mVR‘𝑡)
85, 7cin 3606 . . . . . 6 class ((mCN‘𝑡) ∩ (mVR‘𝑡))
9 c0 3948 . . . . . 6 class
108, 9wceq 1523 . . . . 5 wff ((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅
11 cmtc 31487 . . . . . . 7 class mTC
123, 11cfv 5926 . . . . . 6 class (mTC‘𝑡)
13 cmty 31485 . . . . . . 7 class mType
143, 13cfv 5926 . . . . . 6 class (mType‘𝑡)
157, 12, 14wf 5922 . . . . 5 wff (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)
1610, 15wa 383 . . . 4 wff (((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡))
17 cmax 31488 . . . . . . 7 class mAx
183, 17cfv 5926 . . . . . 6 class (mAx‘𝑡)
19 cmsta 31498 . . . . . . 7 class mStat
203, 19cfv 5926 . . . . . 6 class (mStat‘𝑡)
2118, 20wss 3607 . . . . 5 wff (mAx‘𝑡) ⊆ (mStat‘𝑡)
2214ccnv 5142 . . . . . . . . 9 class (mType‘𝑡)
23 vv . . . . . . . . . . 11 setvar 𝑣
2423cv 1522 . . . . . . . . . 10 class 𝑣
2524csn 4210 . . . . . . . . 9 class {𝑣}
2622, 25cima 5146 . . . . . . . 8 class ((mType‘𝑡) “ {𝑣})
27 cfn 7997 . . . . . . . 8 class Fin
2826, 27wcel 2030 . . . . . . 7 wff ((mType‘𝑡) “ {𝑣}) ∈ Fin
2928wn 3 . . . . . 6 wff ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin
30 cmvt 31486 . . . . . . 7 class mVT
313, 30cfv 5926 . . . . . 6 class (mVT‘𝑡)
3229, 23, 31wral 2941 . . . . 5 wff 𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin
3321, 32wa 383 . . . 4 wff ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin)
3416, 33wa 383 . . 3 wff ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin))
3534, 2cab 2637 . 2 class {𝑡 ∣ ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin))}
361, 35wceq 1523 1 wff mFS = {𝑡 ∣ ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin))}
Colors of variables: wff setvar class
This definition is referenced by:  ismfs  31572
  Copyright terms: Public domain W3C validator