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

Definition df-mfs 29963
Description: Define the set of all formal systems. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mfs  |- mFS  =  {
t  |  ( ( ( (mCN `  t
)  i^i  (mVR `  t
) )  =  (/)  /\  (mType `  t ) : (mVR `  t ) --> (mTC `  t ) )  /\  ( (mAx `  t )  C_  (mStat `  t )  /\  A. v  e.  (mVT `  t
)  -.  ( `' (mType `  t ) " { v } )  e.  Fin ) ) }
Distinct variable group:    v, t

Detailed syntax breakdown of Definition df-mfs
StepHypRef Expression
1 cmfs 29943 . 2  class mFS
2 vt . . . . . . . . 9  setvar  t
32cv 1436 . . . . . . . 8  class  t
4 cmcn 29927 . . . . . . . 8  class mCN
53, 4cfv 5592 . . . . . . 7  class  (mCN `  t )
6 cmvar 29928 . . . . . . . 8  class mVR
73, 6cfv 5592 . . . . . . 7  class  (mVR `  t )
85, 7cin 3432 . . . . . 6  class  ( (mCN
`  t )  i^i  (mVR `  t )
)
9 c0 3758 . . . . . 6  class  (/)
108, 9wceq 1437 . . . . 5  wff  ( (mCN
`  t )  i^i  (mVR `  t )
)  =  (/)
11 cmtc 29931 . . . . . . 7  class mTC
123, 11cfv 5592 . . . . . 6  class  (mTC `  t )
13 cmty 29929 . . . . . . 7  class mType
143, 13cfv 5592 . . . . . 6  class  (mType `  t )
157, 12, 14wf 5588 . . . . 5  wff  (mType `  t ) : (mVR
`  t ) --> (mTC
`  t )
1610, 15wa 370 . . . 4  wff  ( ( (mCN `  t )  i^i  (mVR `  t )
)  =  (/)  /\  (mType `  t ) : (mVR
`  t ) --> (mTC
`  t ) )
17 cmax 29932 . . . . . . 7  class mAx
183, 17cfv 5592 . . . . . 6  class  (mAx `  t )
19 cmsta 29942 . . . . . . 7  class mStat
203, 19cfv 5592 . . . . . 6  class  (mStat `  t )
2118, 20wss 3433 . . . . 5  wff  (mAx `  t )  C_  (mStat `  t )
2214ccnv 4844 . . . . . . . . 9  class  `' (mType `  t )
23 vv . . . . . . . . . . 11  setvar  v
2423cv 1436 . . . . . . . . . 10  class  v
2524csn 3993 . . . . . . . . 9  class  { v }
2622, 25cima 4848 . . . . . . . 8  class  ( `' (mType `  t ) " { v } )
27 cfn 7568 . . . . . . . 8  class  Fin
2826, 27wcel 1867 . . . . . . 7  wff  ( `' (mType `  t ) " { v } )  e.  Fin
2928wn 3 . . . . . 6  wff  -.  ( `' (mType `  t ) " { v } )  e.  Fin
30 cmvt 29930 . . . . . . 7  class mVT
313, 30cfv 5592 . . . . . 6  class  (mVT `  t )
3229, 23, 31wral 2773 . . . . 5  wff  A. v  e.  (mVT `  t )  -.  ( `' (mType `  t ) " {
v } )  e. 
Fin
3321, 32wa 370 . . . 4  wff  ( (mAx
`  t )  C_  (mStat `  t )  /\  A. v  e.  (mVT `  t )  -.  ( `' (mType `  t ) " { v } )  e.  Fin )
3416, 33wa 370 . . 3  wff  ( ( ( (mCN `  t
)  i^i  (mVR `  t
) )  =  (/)  /\  (mType `  t ) : (mVR `  t ) --> (mTC `  t ) )  /\  ( (mAx `  t )  C_  (mStat `  t )  /\  A. v  e.  (mVT `  t
)  -.  ( `' (mType `  t ) " { v } )  e.  Fin ) )
3534, 2cab 2405 . 2  class  { t  |  ( ( ( (mCN `  t )  i^i  (mVR `  t )
)  =  (/)  /\  (mType `  t ) : (mVR
`  t ) --> (mTC
`  t ) )  /\  ( (mAx `  t )  C_  (mStat `  t )  /\  A. v  e.  (mVT `  t
)  -.  ( `' (mType `  t ) " { v } )  e.  Fin ) ) }
361, 35wceq 1437 1  wff mFS  =  {
t  |  ( ( ( (mCN `  t
)  i^i  (mVR `  t
) )  =  (/)  /\  (mType `  t ) : (mVR `  t ) --> (mTC `  t ) )  /\  ( (mAx `  t )  C_  (mStat `  t )  /\  A. v  e.  (mVT `  t
)  -.  ( `' (mType `  t ) " { v } )  e.  Fin ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  ismfs  30016
  Copyright terms: Public domain W3C validator