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

Definition df-mcls 31155
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
StepHypRef Expression
1 cmcls 31135 . 2 class mCls
2 vt . . 3 setvar 𝑡
3 cvv 3190 . . 3 class V
4 vd . . . 4 setvar 𝑑
5 vh . . . 4 setvar
62cv 1479 . . . . . 6 class 𝑡
7 cmdv 31126 . . . . . 6 class mDV
86, 7cfv 5857 . . . . 5 class (mDV‘𝑡)
98cpw 4136 . . . 4 class 𝒫 (mDV‘𝑡)
10 cmex 31125 . . . . . 6 class mEx
116, 10cfv 5857 . . . . 5 class (mEx‘𝑡)
1211cpw 4136 . . . 4 class 𝒫 (mEx‘𝑡)
135cv 1479 . . . . . . . . 9 class
14 cmvh 31130 . . . . . . . . . . 11 class mVH
156, 14cfv 5857 . . . . . . . . . 10 class (mVH‘𝑡)
1615crn 5085 . . . . . . . . 9 class ran (mVH‘𝑡)
1713, 16cun 3558 . . . . . . . 8 class ( ∪ ran (mVH‘𝑡))
18 vc . . . . . . . . 9 setvar 𝑐
1918cv 1479 . . . . . . . 8 class 𝑐
2017, 19wss 3560 . . . . . . 7 wff ( ∪ ran (mVH‘𝑡)) ⊆ 𝑐
21 vm . . . . . . . . . . . . . 14 setvar 𝑚
2221cv 1479 . . . . . . . . . . . . 13 class 𝑚
23 vo . . . . . . . . . . . . . 14 setvar 𝑜
2423cv 1479 . . . . . . . . . . . . 13 class 𝑜
25 vp . . . . . . . . . . . . . 14 setvar 𝑝
2625cv 1479 . . . . . . . . . . . . 13 class 𝑝
2722, 24, 26cotp 4163 . . . . . . . . . . . 12 class 𝑚, 𝑜, 𝑝
28 cmax 31123 . . . . . . . . . . . . 13 class mAx
296, 28cfv 5857 . . . . . . . . . . . 12 class (mAx‘𝑡)
3027, 29wcel 1987 . . . . . . . . . . 11 wff 𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡)
31 vs . . . . . . . . . . . . . . . . 17 setvar 𝑠
3231cv 1479 . . . . . . . . . . . . . . . 16 class 𝑠
3324, 16cun 3558 . . . . . . . . . . . . . . . 16 class (𝑜 ∪ ran (mVH‘𝑡))
3432, 33cima 5087 . . . . . . . . . . . . . . 15 class (𝑠 “ (𝑜 ∪ ran (mVH‘𝑡)))
3534, 19wss 3560 . . . . . . . . . . . . . 14 wff (𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐
36 vx . . . . . . . . . . . . . . . . . . 19 setvar 𝑥
3736cv 1479 . . . . . . . . . . . . . . . . . 18 class 𝑥
38 vy . . . . . . . . . . . . . . . . . . 19 setvar 𝑦
3938cv 1479 . . . . . . . . . . . . . . . . . 18 class 𝑦
4037, 39, 22wbr 4623 . . . . . . . . . . . . . . . . 17 wff 𝑥𝑚𝑦
4137, 15cfv 5857 . . . . . . . . . . . . . . . . . . . . 21 class ((mVH‘𝑡)‘𝑥)
4241, 32cfv 5857 . . . . . . . . . . . . . . . . . . . 20 class (𝑠‘((mVH‘𝑡)‘𝑥))
43 cmvrs 31127 . . . . . . . . . . . . . . . . . . . . 21 class mVars
446, 43cfv 5857 . . . . . . . . . . . . . . . . . . . 20 class (mVars‘𝑡)
4542, 44cfv 5857 . . . . . . . . . . . . . . . . . . 19 class ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥)))
4639, 15cfv 5857 . . . . . . . . . . . . . . . . . . . . 21 class ((mVH‘𝑡)‘𝑦)
4746, 32cfv 5857 . . . . . . . . . . . . . . . . . . . 20 class (𝑠‘((mVH‘𝑡)‘𝑦))
4847, 44cfv 5857 . . . . . . . . . . . . . . . . . . 19 class ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))
4945, 48cxp 5082 . . . . . . . . . . . . . . . . . 18 class (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦))))
504cv 1479 . . . . . . . . . . . . . . . . . 18 class 𝑑
5149, 50wss 3560 . . . . . . . . . . . . . . . . 17 wff (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑
5240, 51wi 4 . . . . . . . . . . . . . . . 16 wff (𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)
5352, 38wal 1478 . . . . . . . . . . . . . . 15 wff 𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)
5453, 36wal 1478 . . . . . . . . . . . . . 14 wff 𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)
5535, 54wa 384 . . . . . . . . . . . . 13 wff ((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑))
5626, 32cfv 5857 . . . . . . . . . . . . . 14 class (𝑠𝑝)
5756, 19wcel 1987 . . . . . . . . . . . . 13 wff (𝑠𝑝) ∈ 𝑐
5855, 57wi 4 . . . . . . . . . . . 12 wff (((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)
59 cmsub 31129 . . . . . . . . . . . . . 14 class mSubst
606, 59cfv 5857 . . . . . . . . . . . . 13 class (mSubst‘𝑡)
6160crn 5085 . . . . . . . . . . . 12 class ran (mSubst‘𝑡)
6258, 31, 61wral 2908 . . . . . . . . . . 11 wff 𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)
6330, 62wi 4 . . . . . . . . . 10 wff (⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐))
6463, 25wal 1478 . . . . . . . . 9 wff 𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐))
6564, 23wal 1478 . . . . . . . 8 wff 𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐))
6665, 21wal 1478 . . . . . . 7 wff 𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐))
6720, 66wa 384 . . . . . 6 wff (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))
6867, 18cab 2607 . . . . 5 class {𝑐 ∣ (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}
6968cint 4447 . . . 4 class {𝑐 ∣ (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}
704, 5, 9, 12, 69cmpt2 6617 . . 3 class (𝑑 ∈ 𝒫 (mDV‘𝑡), ∈ 𝒫 (mEx‘𝑡) ↦ {𝑐 ∣ (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))})
712, 3, 70cmpt 4683 . 2 class (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ∈ 𝒫 (mEx‘𝑡) ↦ {𝑐 ∣ (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}))
721, 71wceq 1480 1 wff mCls = (𝑡 ∈ V ↦ (𝑑 ∈ 𝒫 (mDV‘𝑡), ∈ 𝒫 (mEx‘𝑡) ↦ {𝑐 ∣ (( ∪ ran (mVH‘𝑡)) ⊆ 𝑐 ∧ ∀𝑚𝑜𝑝(⟨𝑚, 𝑜, 𝑝⟩ ∈ (mAx‘𝑡) → ∀𝑠 ∈ ran (mSubst‘𝑡)(((𝑠 “ (𝑜 ∪ ran (mVH‘𝑡))) ⊆ 𝑐 ∧ ∀𝑥𝑦(𝑥𝑚𝑦 → (((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑥))) × ((mVars‘𝑡)‘(𝑠‘((mVH‘𝑡)‘𝑦)))) ⊆ 𝑑)) → (𝑠𝑝) ∈ 𝑐)))}))
Colors of variables: wff setvar class
This definition is referenced by:  mclsrcl  31219  mclsval  31221
  Copyright terms: Public domain W3C validator