Definition df-mcls 31394

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

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

This definition is referenced by:  mclsrcl  31458  mclsval  31460