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 31378
 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 31358 . 2 class mFS
2 vt . . . . . . . . 9 setvar 𝑡
32cv 1481 . . . . . . . 8 class 𝑡
4 cmcn 31342 . . . . . . . 8 class mCN
53, 4cfv 5886 . . . . . . 7 class (mCN‘𝑡)
6 cmvar 31343 . . . . . . . 8 class mVR
73, 6cfv 5886 . . . . . . 7 class (mVR‘𝑡)
85, 7cin 3571 . . . . . 6 class ((mCN‘𝑡) ∩ (mVR‘𝑡))
9 c0 3913 . . . . . 6 class
108, 9wceq 1482 . . . . 5 wff ((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅
11 cmtc 31346 . . . . . . 7 class mTC
123, 11cfv 5886 . . . . . 6 class (mTC‘𝑡)
13 cmty 31344 . . . . . . 7 class mType
143, 13cfv 5886 . . . . . 6 class (mType‘𝑡)
157, 12, 14wf 5882 . . . . 5 wff (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)
1610, 15wa 384 . . . 4 wff (((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡))
17 cmax 31347 . . . . . . 7 class mAx
183, 17cfv 5886 . . . . . 6 class (mAx‘𝑡)
19 cmsta 31357 . . . . . . 7 class mStat
203, 19cfv 5886 . . . . . 6 class (mStat‘𝑡)
2118, 20wss 3572 . . . . 5 wff (mAx‘𝑡) ⊆ (mStat‘𝑡)
2214ccnv 5111 . . . . . . . . 9 class (mType‘𝑡)
23 vv . . . . . . . . . . 11 setvar 𝑣
2423cv 1481 . . . . . . . . . 10 class 𝑣
2524csn 4175 . . . . . . . . 9 class {𝑣}
2622, 25cima 5115 . . . . . . . 8 class ((mType‘𝑡) “ {𝑣})
27 cfn 7952 . . . . . . . 8 class Fin
2826, 27wcel 1989 . . . . . . 7 wff ((mType‘𝑡) “ {𝑣}) ∈ Fin
2928wn 3 . . . . . 6 wff ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin
30 cmvt 31345 . . . . . . 7 class mVT
313, 30cfv 5886 . . . . . 6 class (mVT‘𝑡)
3229, 23, 31wral 2911 . . . . 5 wff 𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin
3321, 32wa 384 . . . 4 wff ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin)
3416, 33wa 384 . . 3 wff ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin))
3534, 2cab 2607 . 2 class {𝑡 ∣ ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin))}
361, 35wceq 1482 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  31431
 Copyright terms: Public domain W3C validator