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

Definition df-mcls 30128
Description: Define the closure of a set of statements relative to a set of disjointness constraints. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mcls  |- mCls  =  ( t  e.  _V  |->  ( d  e.  ~P (mDV `  t ) ,  h  e.  ~P (mEx `  t
)  |->  |^| { c  |  ( ( h  u. 
ran  (mVH `  t )
)  C_  c  /\  A. m A. o A. p ( <. m ,  o ,  p >.  e.  (mAx `  t
)  ->  A. s  e.  ran  (mSubst `  t
) ( ( ( s " ( o  u.  ran  (mVH `  t ) ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  C_  d )
)  ->  ( s `  p )  e.  c ) ) ) } ) )
Distinct variable group:    c, d, h, m, o, p, s, t, x, y

Detailed syntax breakdown of Definition df-mcls
StepHypRef Expression
1 cmcls 30108 . 2  class mCls
2 vt . . 3  setvar  t
3 cvv 3081 . . 3  class  _V
4 vd . . . 4  setvar  d
5 vh . . . 4  setvar  h
62cv 1436 . . . . . 6  class  t
7 cmdv 30099 . . . . . 6  class mDV
86, 7cfv 5597 . . . . 5  class  (mDV `  t )
98cpw 3979 . . . 4  class  ~P (mDV `  t )
10 cmex 30098 . . . . . 6  class mEx
116, 10cfv 5597 . . . . 5  class  (mEx `  t )
1211cpw 3979 . . . 4  class  ~P (mEx `  t )
135cv 1436 . . . . . . . . 9  class  h
14 cmvh 30103 . . . . . . . . . . 11  class mVH
156, 14cfv 5597 . . . . . . . . . 10  class  (mVH `  t )
1615crn 4850 . . . . . . . . 9  class  ran  (mVH `  t )
1713, 16cun 3434 . . . . . . . 8  class  ( h  u.  ran  (mVH `  t ) )
18 vc . . . . . . . . 9  setvar  c
1918cv 1436 . . . . . . . 8  class  c
2017, 19wss 3436 . . . . . . 7  wff  ( h  u.  ran  (mVH `  t ) )  C_  c
21 vm . . . . . . . . . . . . . 14  setvar  m
2221cv 1436 . . . . . . . . . . . . 13  class  m
23 vo . . . . . . . . . . . . . 14  setvar  o
2423cv 1436 . . . . . . . . . . . . 13  class  o
25 vp . . . . . . . . . . . . . 14  setvar  p
2625cv 1436 . . . . . . . . . . . . 13  class  p
2722, 24, 26cotp 4004 . . . . . . . . . . . 12  class  <. m ,  o ,  p >.
28 cmax 30096 . . . . . . . . . . . . 13  class mAx
296, 28cfv 5597 . . . . . . . . . . . 12  class  (mAx `  t )
3027, 29wcel 1868 . . . . . . . . . . 11  wff  <. m ,  o ,  p >.  e.  (mAx `  t
)
31 vs . . . . . . . . . . . . . . . . 17  setvar  s
3231cv 1436 . . . . . . . . . . . . . . . 16  class  s
3324, 16cun 3434 . . . . . . . . . . . . . . . 16  class  ( o  u.  ran  (mVH `  t ) )
3432, 33cima 4852 . . . . . . . . . . . . . . 15  class  ( s
" ( o  u. 
ran  (mVH `  t )
) )
3534, 19wss 3436 . . . . . . . . . . . . . 14  wff  ( s
" ( o  u. 
ran  (mVH `  t )
) )  C_  c
36 vx . . . . . . . . . . . . . . . . . . 19  setvar  x
3736cv 1436 . . . . . . . . . . . . . . . . . 18  class  x
38 vy . . . . . . . . . . . . . . . . . . 19  setvar  y
3938cv 1436 . . . . . . . . . . . . . . . . . 18  class  y
4037, 39, 22wbr 4420 . . . . . . . . . . . . . . . . 17  wff  x m y
4137, 15cfv 5597 . . . . . . . . . . . . . . . . . . . . 21  class  ( (mVH
`  t ) `  x )
4241, 32cfv 5597 . . . . . . . . . . . . . . . . . . . 20  class  ( s `
 ( (mVH `  t ) `  x
) )
43 cmvrs 30100 . . . . . . . . . . . . . . . . . . . . 21  class mVars
446, 43cfv 5597 . . . . . . . . . . . . . . . . . . . 20  class  (mVars `  t )
4542, 44cfv 5597 . . . . . . . . . . . . . . . . . . 19  class  ( (mVars `  t ) `  (
s `  ( (mVH `  t ) `  x
) ) )
4639, 15cfv 5597 . . . . . . . . . . . . . . . . . . . . 21  class  ( (mVH
`  t ) `  y )
4746, 32cfv 5597 . . . . . . . . . . . . . . . . . . . 20  class  ( s `
 ( (mVH `  t ) `  y
) )
4847, 44cfv 5597 . . . . . . . . . . . . . . . . . . 19  class  ( (mVars `  t ) `  (
s `  ( (mVH `  t ) `  y
) ) )
4945, 48cxp 4847 . . . . . . . . . . . . . . . . . 18  class  ( ( (mVars `  t ) `  ( s `  (
(mVH `  t ) `  x ) ) )  X.  ( (mVars `  t ) `  (
s `  ( (mVH `  t ) `  y
) ) ) )
504cv 1436 . . . . . . . . . . . . . . . . . 18  class  d
5149, 50wss 3436 . . . . . . . . . . . . . . . . 17  wff  ( ( (mVars `  t ) `  ( s `  (
(mVH `  t ) `  x ) ) )  X.  ( (mVars `  t ) `  (
s `  ( (mVH `  t ) `  y
) ) ) ) 
C_  d
5240, 51wi 4 . . . . . . . . . . . . . . . 16  wff  ( x m y  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  C_  d )
5352, 38wal 1435 . . . . . . . . . . . . . . 15  wff  A. y
( x m y  ->  ( ( (mVars `  t ) `  (
s `  ( (mVH `  t ) `  x
) ) )  X.  ( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  y )
) ) )  C_  d )
5453, 36wal 1435 . . . . . . . . . . . . . 14  wff  A. x A. y ( x m y  ->  ( (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  x ) ) )  X.  ( (mVars `  t ) `  (
s `  ( (mVH `  t ) `  y
) ) ) ) 
C_  d )
5535, 54wa 370 . . . . . . . . . . . . 13  wff  ( ( s " ( o  u.  ran  (mVH `  t ) ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  C_  d )
)
5626, 32cfv 5597 . . . . . . . . . . . . . 14  class  ( s `
 p )
5756, 19wcel 1868 . . . . . . . . . . . . 13  wff  ( s `
 p )  e.  c
5855, 57wi 4 . . . . . . . . . . . 12  wff  ( ( ( s " (
o  u.  ran  (mVH `  t ) ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  C_  d )
)  ->  ( s `  p )  e.  c )
59 cmsub 30102 . . . . . . . . . . . . . 14  class mSubst
606, 59cfv 5597 . . . . . . . . . . . . 13  class  (mSubst `  t )
6160crn 4850 . . . . . . . . . . . 12  class  ran  (mSubst `  t )
6258, 31, 61wral 2775 . . . . . . . . . . 11  wff  A. s  e.  ran  (mSubst `  t
) ( ( ( s " ( o  u.  ran  (mVH `  t ) ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  C_  d )
)  ->  ( s `  p )  e.  c )
6330, 62wi 4 . . . . . . . . . 10  wff  ( <.
m ,  o ,  p >.  e.  (mAx `  t )  ->  A. s  e.  ran  (mSubst `  t
) ( ( ( s " ( o  u.  ran  (mVH `  t ) ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  C_  d )
)  ->  ( s `  p )  e.  c ) )
6463, 25wal 1435 . . . . . . . . 9  wff  A. p
( <. m ,  o ,  p >.  e.  (mAx
`  t )  ->  A. s  e.  ran  (mSubst `  t ) ( ( ( s "
( o  u.  ran  (mVH `  t ) ) )  C_  c  /\  A. x A. y ( x m y  -> 
( ( (mVars `  t ) `  (
s `  ( (mVH `  t ) `  x
) ) )  X.  ( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  y )
) ) )  C_  d ) )  -> 
( s `  p
)  e.  c ) )
6564, 23wal 1435 . . . . . . . 8  wff  A. o A. p ( <. m ,  o ,  p >.  e.  (mAx `  t
)  ->  A. s  e.  ran  (mSubst `  t
) ( ( ( s " ( o  u.  ran  (mVH `  t ) ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  C_  d )
)  ->  ( s `  p )  e.  c ) )
6665, 21wal 1435 . . . . . . 7  wff  A. m A. o A. p (
<. m ,  o ,  p >.  e.  (mAx `  t )  ->  A. s  e.  ran  (mSubst `  t
) ( ( ( s " ( o  u.  ran  (mVH `  t ) ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  C_  d )
)  ->  ( s `  p )  e.  c ) )
6720, 66wa 370 . . . . . 6  wff  ( ( h  u.  ran  (mVH `  t ) )  C_  c  /\  A. m A. o A. p ( <.
m ,  o ,  p >.  e.  (mAx `  t )  ->  A. s  e.  ran  (mSubst `  t
) ( ( ( s " ( o  u.  ran  (mVH `  t ) ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  C_  d )
)  ->  ( s `  p )  e.  c ) ) )
6867, 18cab 2407 . . . . 5  class  { c  |  ( ( h  u.  ran  (mVH `  t ) )  C_  c  /\  A. m A. o A. p ( <.
m ,  o ,  p >.  e.  (mAx `  t )  ->  A. s  e.  ran  (mSubst `  t
) ( ( ( s " ( o  u.  ran  (mVH `  t ) ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  C_  d )
)  ->  ( s `  p )  e.  c ) ) ) }
6968cint 4252 . . . 4  class  |^| { c  |  ( ( h  u.  ran  (mVH `  t ) )  C_  c  /\  A. m A. o A. p ( <.
m ,  o ,  p >.  e.  (mAx `  t )  ->  A. s  e.  ran  (mSubst `  t
) ( ( ( s " ( o  u.  ran  (mVH `  t ) ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  C_  d )
)  ->  ( s `  p )  e.  c ) ) ) }
704, 5, 9, 12, 69cmpt2 6303 . . 3  class  ( d  e.  ~P (mDV `  t ) ,  h  e.  ~P (mEx `  t
)  |->  |^| { c  |  ( ( h  u. 
ran  (mVH `  t )
)  C_  c  /\  A. m A. o A. p ( <. m ,  o ,  p >.  e.  (mAx `  t
)  ->  A. s  e.  ran  (mSubst `  t
) ( ( ( s " ( o  u.  ran  (mVH `  t ) ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  C_  d )
)  ->  ( s `  p )  e.  c ) ) ) } )
712, 3, 70cmpt 4479 . 2  class  ( t  e.  _V  |->  ( d  e.  ~P (mDV `  t ) ,  h  e.  ~P (mEx `  t
)  |->  |^| { c  |  ( ( h  u. 
ran  (mVH `  t )
)  C_  c  /\  A. m A. o A. p ( <. m ,  o ,  p >.  e.  (mAx `  t
)  ->  A. s  e.  ran  (mSubst `  t
) ( ( ( s " ( o  u.  ran  (mVH `  t ) ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  C_  d )
)  ->  ( s `  p )  e.  c ) ) ) } ) )
721, 71wceq 1437 1  wff mCls  =  ( t  e.  _V  |->  ( d  e.  ~P (mDV `  t ) ,  h  e.  ~P (mEx `  t
)  |->  |^| { c  |  ( ( h  u. 
ran  (mVH `  t )
)  C_  c  /\  A. m A. o A. p ( <. m ,  o ,  p >.  e.  (mAx `  t
)  ->  A. s  e.  ran  (mSubst `  t
) ( ( ( s " ( o  u.  ran  (mVH `  t ) ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  C_  d )
)  ->  ( s `  p )  e.  c ) ) ) } ) )
Colors of variables: wff setvar class
This definition is referenced by:  mclsrcl  30192  mclsval  30194
  Copyright terms: Public domain W3C validator