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 32640
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 32620 . 2 class mFS
2 vt . . . . . . . . 9 setvar 𝑡
32cv 1527 . . . . . . . 8 class 𝑡
4 cmcn 32604 . . . . . . . 8 class mCN
53, 4cfv 6348 . . . . . . 7 class (mCN‘𝑡)
6 cmvar 32605 . . . . . . . 8 class mVR
73, 6cfv 6348 . . . . . . 7 class (mVR‘𝑡)
85, 7cin 3932 . . . . . 6 class ((mCN‘𝑡) ∩ (mVR‘𝑡))
9 c0 4288 . . . . . 6 class
108, 9wceq 1528 . . . . 5 wff ((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅
11 cmtc 32608 . . . . . . 7 class mTC
123, 11cfv 6348 . . . . . 6 class (mTC‘𝑡)
13 cmty 32606 . . . . . . 7 class mType
143, 13cfv 6348 . . . . . 6 class (mType‘𝑡)
157, 12, 14wf 6344 . . . . 5 wff (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)
1610, 15wa 396 . . . 4 wff (((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡))
17 cmax 32609 . . . . . . 7 class mAx
183, 17cfv 6348 . . . . . 6 class (mAx‘𝑡)
19 cmsta 32619 . . . . . . 7 class mStat
203, 19cfv 6348 . . . . . 6 class (mStat‘𝑡)
2118, 20wss 3933 . . . . 5 wff (mAx‘𝑡) ⊆ (mStat‘𝑡)
2214ccnv 5547 . . . . . . . . 9 class (mType‘𝑡)
23 vv . . . . . . . . . . 11 setvar 𝑣
2423cv 1527 . . . . . . . . . 10 class 𝑣
2524csn 4557 . . . . . . . . 9 class {𝑣}
2622, 25cima 5551 . . . . . . . 8 class ((mType‘𝑡) “ {𝑣})
27 cfn 8497 . . . . . . . 8 class Fin
2826, 27wcel 2105 . . . . . . 7 wff ((mType‘𝑡) “ {𝑣}) ∈ Fin
2928wn 3 . . . . . 6 wff ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin
30 cmvt 32607 . . . . . . 7 class mVT
313, 30cfv 6348 . . . . . 6 class (mVT‘𝑡)
3229, 23, 31wral 3135 . . . . 5 wff 𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin
3321, 32wa 396 . . . 4 wff ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin)
3416, 33wa 396 . . 3 wff ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin))
3534, 2cab 2796 . 2 class {𝑡 ∣ ((((mCN‘𝑡) ∩ (mVR‘𝑡)) = ∅ ∧ (mType‘𝑡):(mVR‘𝑡)⟶(mTC‘𝑡)) ∧ ((mAx‘𝑡) ⊆ (mStat‘𝑡) ∧ ∀𝑣 ∈ (mVT‘𝑡) ¬ ((mType‘𝑡) “ {𝑣}) ∈ Fin))}
361, 35wceq 1528 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  32693
  Copyright terms: Public domain W3C validator