Metamath Proof Explorer

Definition df-mcls

Description: Define the closure of a set of statements relative to a set of disjointness constraints. (Contributed by Mario Carneiro, 14-Jul-2016)

Ref Expression
Assertion 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 ) ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmcls 
 |-  mCls
1 vt 
 |-  t
2 cvv 
 |-  _V
3 vd 
 |-  d
4 cmdv 
 |-  mDV
5 1 cv 
 |-  t
6 5 4 cfv 
 |-  ( mDV ` t )
7 6 cpw 
 |-  ~P ( mDV ` t )
8 vh 
 |-  h
9 cmex 
 |-  mEx
10 5 9 cfv 
 |-  ( mEx ` t )
11 10 cpw 
 |-  ~P ( mEx ` t )
12 vc 
 |-  c
13 8 cv 
 |-  h
14 cmvh 
 |-  mVH
15 5 14 cfv 
 |-  ( mVH ` t )
16 15 crn 
 |-  ran ( mVH ` t )
17 13 16 cun 
 |-  ( h u. ran ( mVH ` t ) )
18 12 cv 
 |-  c
19 17 18 wss 
 |-  ( h u. ran ( mVH ` t ) ) C_ c
20 vm 
 |-  m
21 vo 
 |-  o
22 vp 
 |-  p
23 20 cv 
 |-  m
24 21 cv 
 |-  o
25 22 cv 
 |-  p
26 23 24 25 cotp 
 |-  <. m , o , p >.
27 cmax 
 |-  mAx
28 5 27 cfv 
 |-  ( mAx ` t )
29 26 28 wcel 
 |-  <. m , o , p >. e. ( mAx ` t )
30 vs 
 |-  s
31 cmsub 
 |-  mSubst
32 5 31 cfv 
 |-  ( mSubst ` t )
33 32 crn 
 |-  ran ( mSubst ` t )
34 30 cv 
 |-  s
35 24 16 cun 
 |-  ( o u. ran ( mVH ` t ) )
36 34 35 cima 
 |-  ( s " ( o u. ran ( mVH ` t ) ) )
37 36 18 wss 
 |-  ( s " ( o u. ran ( mVH ` t ) ) ) C_ c
38 vx 
 |-  x
39 vy 
 |-  y
40 38 cv 
 |-  x
41 39 cv 
 |-  y
42 40 41 23 wbr 
 |-  x m y
43 cmvrs 
 |-  mVars
44 5 43 cfv 
 |-  ( mVars ` t )
45 40 15 cfv 
 |-  ( ( mVH ` t ) ` x )
46 45 34 cfv 
 |-  ( s ` ( ( mVH ` t ) ` x ) )
47 46 44 cfv 
 |-  ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) )
48 41 15 cfv 
 |-  ( ( mVH ` t ) ` y )
49 48 34 cfv 
 |-  ( s ` ( ( mVH ` t ) ` y ) )
50 49 44 cfv 
 |-  ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) )
51 47 50 cxp 
 |-  ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) )
52 3 cv 
 |-  d
53 51 52 wss 
 |-  ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d
54 42 53 wi 
 |-  ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d )
55 54 39 wal 
 |-  A. y ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d )
56 55 38 wal 
 |-  A. x A. y ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d )
57 37 56 wa 
 |-  ( ( 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 ) )
58 25 34 cfv 
 |-  ( s ` p )
59 58 18 wcel 
 |-  ( s ` p ) e. c
60 57 59 wi 
 |-  ( ( ( 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 )
61 60 30 33 wral 
 |-  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 )
62 29 61 wi 
 |-  ( <. 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 ) )
63 62 22 wal 
 |-  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 ) )
64 63 21 wal 
 |-  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 ) )
65 64 20 wal 
 |-  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 ) )
66 19 65 wa 
 |-  ( ( 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 ) ) )
67 66 12 cab 
 |-  { 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 ) ) ) }
68 67 cint 
 |-  |^| { 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 ) ) ) }
69 3 8 7 11 68 cmpo 
 |-  ( 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 ) ) ) } )
70 1 2 69 cmpt 
 |-  ( 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 ) ) ) } ) )
71 0 70 wceq 
 |-  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 ) ) ) } ) )