Definition df-mcls 34091

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 = (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ℎ ∈ 𝒫 (mEx‘𝑡) ↦ ∩ {𝑐 ∣ ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))}))

Distinct variable group:   𝑐,𝑑,ℎ,𝑚,𝑜,𝑝,𝑠,𝑡,𝑥,𝑦

Detailed syntax breakdown of Definition df-mcls

Step	Hyp	Ref	Expression
1		cmcls 34071	. 2 class mCls
2		vt	. . 3 setvar 𝑡
3		cvv 3445	. . 3 class V
4		vd	. . . 4 setvar 𝑑
5		vh	. . . 4 setvar ℎ
6	2	cv 1540	. . . . . 6 class 𝑡
7		cmdv 34062	. . . . . 6 class mDV
8	6, 7	cfv 6496	. . . . 5 class (mDV‘𝑡)
9	8	cpw 4560	. . . 4 class 𝒫 (mDV‘𝑡)
10		cmex 34061	. . . . . 6 class mEx
11	6, 10	cfv 6496	. . . . 5 class (mEx‘𝑡)
12	11	cpw 4560	. . . 4 class 𝒫 (mEx‘𝑡)
13	5	cv 1540	. . . . . . . . 9 class ℎ
14		cmvh 34066	. . . . . . . . . . 11 class mVH
15	6, 14	cfv 6496	. . . . . . . . . 10 class (mVH‘𝑡)
16	15	crn 5634	. . . . . . . . 9 class ran (mVH‘𝑡)
17	13, 16	cun 3908	. . . . . . . 8 class (ℎ ∪ ran (mVH‘𝑡))
18		vc	. . . . . . . . 9 setvar 𝑐
19	18	cv 1540	. . . . . . . 8 class 𝑐
20	17, 19	wss 3910	. . . . . . 7 wff (ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐
21		vm	. . . . . . . . . . . . . 14 setvar 𝑚
22	21	cv 1540	. . . . . . . . . . . . 13 class 𝑚
23		vo	. . . . . . . . . . . . . 14 setvar 𝑜
24	23	cv 1540	. . . . . . . . . . . . 13 class 𝑜
25		vp	. . . . . . . . . . . . . 14 setvar 𝑝
26	25	cv 1540	. . . . . . . . . . . . 13 class 𝑝
27	22, 24, 26	cotp 4594	. . . . . . . . . . . 12 class ⟨𝑚, 𝑜, 𝑝⟩
28		cmax 34059	. . . . . . . . . . . . 13 class mAx
29	6, 28	cfv 6496	. . . . . . . . . . . 12 class (mAx‘𝑡)
30	27, 29	wcel 2106	. . . . . . . . . . 11 wff ⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡)
31		vs	. . . . . . . . . . . . . . . . 17 setvar 𝑠
32	31	cv 1540	. . . . . . . . . . . . . . . 16 class 𝑠
33	24, 16	cun 3908	. . . . . . . . . . . . . . . 16 class (𝑜 ∪ ran (mVH‘𝑡))
34	32, 33	cima 5636	. . . . . . . . . . . . . . 15 class (𝑠 “ (𝑜 ∪ ran (mVH‘𝑡)))
35	34, 19	wss 3910	. . . . . . . . . . . . . 14 wff (𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐
36		vx	. . . . . . . . . . . . . . . . . . 19 setvar 𝑥
37	36	cv 1540	. . . . . . . . . . . . . . . . . 18 class 𝑥
38		vy	. . . . . . . . . . . . . . . . . . 19 setvar 𝑦
39	38	cv 1540	. . . . . . . . . . . . . . . . . 18 class 𝑦
40	37, 39, 22	wbr 5105	. . . . . . . . . . . . . . . . 17 wff 𝑥𝑚𝑦
41	37, 15	cfv 6496	. . . . . . . . . . . . . . . . . . . . 21 class ((mVH‘𝑡)‘𝑥)
42	41, 32	cfv 6496	. . . . . . . . . . . . . . . . . . . 20 class (𝑠‘((mVH‘𝑡)‘𝑥))
43		cmvrs 34063	. . . . . . . . . . . . . . . . . . . . 21 class mVars
44	6, 43	cfv 6496	. . . . . . . . . . . . . . . . . . . 20 class (mVars‘𝑡)
45	42, 44	cfv 6496	. . . . . . . . . . . . . . . . . . 19 class ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥)))
46	39, 15	cfv 6496	. . . . . . . . . . . . . . . . . . . . 21 class ((mVH‘𝑡)‘𝑦)
47	46, 32	cfv 6496	. . . . . . . . . . . . . . . . . . . 20 class (𝑠‘((mVH‘𝑡)‘𝑦))
48	47, 44	cfv 6496	. . . . . . . . . . . . . . . . . . 19 class ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))
49	45, 48	cxp 5631	. . . . . . . . . . . . . . . . . 18 class (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦))))
50	4	cv 1540	. . . . . . . . . . . . . . . . . 18 class 𝑑
51	49, 50	wss 3910	. . . . . . . . . . . . . . . . 17 wff (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑
52	40, 51	wi 4	. . . . . . . . . . . . . . . 16 wff (𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)
53	52, 38	wal 1539	. . . . . . . . . . . . . . 15 wff ∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)
54	53, 36	wal 1539	. . . . . . . . . . . . . 14 wff ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)
55	35, 54	wa 396	. . . . . . . . . . . . 13 wff ((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑))
56	26, 32	cfv 6496	. . . . . . . . . . . . . 14 class (𝑠‘𝑝)
57	56, 19	wcel 2106	. . . . . . . . . . . . 13 wff (𝑠‘𝑝) ∈ 𝑐
58	55, 57	wi 4	. . . . . . . . . . . 12 wff (((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)
59		cmsub 34065	. . . . . . . . . . . . . 14 class mSubst
60	6, 59	cfv 6496	. . . . . . . . . . . . 13 class (mSubst‘𝑡)
61	60	crn 5634	. . . . . . . . . . . 12 class ran (mSubst‘𝑡)
62	58, 31, 61	wral 3064	. . . . . . . . . . 11 wff ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)
63	30, 62	wi 4	. . . . . . . . . 10 wff (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐))
64	63, 25	wal 1539	. . . . . . . . 9 wff ∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐))
65	64, 23	wal 1539	. . . . . . . 8 wff ∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐))
66	65, 21	wal 1539	. . . . . . 7 wff ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐))
67	20, 66	wa 396	. . . . . 6 wff ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))
68	67, 18	cab 2713	. . . . 5 class {𝑐 ∣ ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))}
69	68	cint 4907	. . . 4 class ∩ {𝑐 ∣ ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))}
70	4, 5, 9, 12, 69	cmpo 7359	. . 3 class (𝑑 ∈ 𝒫 (mDV‘𝑡), ℎ ∈ 𝒫 (mEx‘𝑡) ↦ ∩ {𝑐 ∣ ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))})
71	2, 3, 70	cmpt 5188	. 2 class (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ℎ ∈ 𝒫 (mEx‘𝑡) ↦ ∩ {𝑐 ∣ ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))}))
72	1, 71	wceq 1541	1 wff mCls = (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ℎ ∈ 𝒫 (mEx‘𝑡) ↦ ∩ {𝑐 ∣ ((ℎ ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚∀𝑜∀𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥∀𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠‘𝑝) ∈ 𝑐)))}))

This definition is referenced by:  mclsrcl  34155  mclsval  34157