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 34155
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 34135 . 2 class mCls
2 vt . . 3 setvar 𝑑
3 cvv 3447 . . 3 class V
4 vd . . . 4 setvar 𝑑
5 vh . . . 4 setvar β„Ž
62cv 1541 . . . . . 6 class 𝑑
7 cmdv 34126 . . . . . 6 class mDV
86, 7cfv 6500 . . . . 5 class (mDVβ€˜π‘‘)
98cpw 4564 . . . 4 class 𝒫 (mDVβ€˜π‘‘)
10 cmex 34125 . . . . . 6 class mEx
116, 10cfv 6500 . . . . 5 class (mExβ€˜π‘‘)
1211cpw 4564 . . . 4 class 𝒫 (mExβ€˜π‘‘)
135cv 1541 . . . . . . . . 9 class β„Ž
14 cmvh 34130 . . . . . . . . . . 11 class mVH
156, 14cfv 6500 . . . . . . . . . 10 class (mVHβ€˜π‘‘)
1615crn 5638 . . . . . . . . 9 class ran (mVHβ€˜π‘‘)
1713, 16cun 3912 . . . . . . . 8 class (β„Ž βˆͺ ran (mVHβ€˜π‘‘))
18 vc . . . . . . . . 9 setvar 𝑐
1918cv 1541 . . . . . . . 8 class 𝑐
2017, 19wss 3914 . . . . . . 7 wff (β„Ž βˆͺ ran (mVHβ€˜π‘‘)) βŠ† 𝑐
21 vm . . . . . . . . . . . . . 14 setvar π‘š
2221cv 1541 . . . . . . . . . . . . 13 class π‘š
23 vo . . . . . . . . . . . . . 14 setvar π‘œ
2423cv 1541 . . . . . . . . . . . . 13 class π‘œ
25 vp . . . . . . . . . . . . . 14 setvar 𝑝
2625cv 1541 . . . . . . . . . . . . 13 class 𝑝
2722, 24, 26cotp 4598 . . . . . . . . . . . 12 class βŸ¨π‘š, π‘œ, π‘βŸ©
28 cmax 34123 . . . . . . . . . . . . 13 class mAx
296, 28cfv 6500 . . . . . . . . . . . 12 class (mAxβ€˜π‘‘)
3027, 29wcel 2107 . . . . . . . . . . 11 wff βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘)
31 vs . . . . . . . . . . . . . . . . 17 setvar 𝑠
3231cv 1541 . . . . . . . . . . . . . . . 16 class 𝑠
3324, 16cun 3912 . . . . . . . . . . . . . . . 16 class (π‘œ βˆͺ ran (mVHβ€˜π‘‘))
3432, 33cima 5640 . . . . . . . . . . . . . . 15 class (𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘)))
3534, 19wss 3914 . . . . . . . . . . . . . 14 wff (𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐
36 vx . . . . . . . . . . . . . . . . . . 19 setvar π‘₯
3736cv 1541 . . . . . . . . . . . . . . . . . 18 class π‘₯
38 vy . . . . . . . . . . . . . . . . . . 19 setvar 𝑦
3938cv 1541 . . . . . . . . . . . . . . . . . 18 class 𝑦
4037, 39, 22wbr 5109 . . . . . . . . . . . . . . . . 17 wff π‘₯π‘šπ‘¦
4137, 15cfv 6500 . . . . . . . . . . . . . . . . . . . . 21 class ((mVHβ€˜π‘‘)β€˜π‘₯)
4241, 32cfv 6500 . . . . . . . . . . . . . . . . . . . 20 class (π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))
43 cmvrs 34127 . . . . . . . . . . . . . . . . . . . . 21 class mVars
446, 43cfv 6500 . . . . . . . . . . . . . . . . . . . 20 class (mVarsβ€˜π‘‘)
4542, 44cfv 6500 . . . . . . . . . . . . . . . . . . 19 class ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯)))
4639, 15cfv 6500 . . . . . . . . . . . . . . . . . . . . 21 class ((mVHβ€˜π‘‘)β€˜π‘¦)
4746, 32cfv 6500 . . . . . . . . . . . . . . . . . . . 20 class (π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦))
4847, 44cfv 6500 . . . . . . . . . . . . . . . . . . 19 class ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))
4945, 48cxp 5635 . . . . . . . . . . . . . . . . . 18 class (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦))))
504cv 1541 . . . . . . . . . . . . . . . . . 18 class 𝑑
5149, 50wss 3914 . . . . . . . . . . . . . . . . 17 wff (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑
5240, 51wi 4 . . . . . . . . . . . . . . . 16 wff (π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)
5352, 38wal 1540 . . . . . . . . . . . . . . 15 wff βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)
5453, 36wal 1540 . . . . . . . . . . . . . 14 wff βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)
5535, 54wa 397 . . . . . . . . . . . . 13 wff ((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑))
5626, 32cfv 6500 . . . . . . . . . . . . . 14 class (π‘ β€˜π‘)
5756, 19wcel 2107 . . . . . . . . . . . . 13 wff (π‘ β€˜π‘) ∈ 𝑐
5855, 57wi 4 . . . . . . . . . . . 12 wff (((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)
59 cmsub 34129 . . . . . . . . . . . . . 14 class mSubst
606, 59cfv 6500 . . . . . . . . . . . . 13 class (mSubstβ€˜π‘‘)
6160crn 5638 . . . . . . . . . . . 12 class ran (mSubstβ€˜π‘‘)
6258, 31, 61wral 3061 . . . . . . . . . . 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 1540 . . . . . . . . 9 wff βˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐))
6564, 23wal 1540 . . . . . . . 8 wff βˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐))
6665, 21wal 1540 . . . . . . 7 wff βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐))
6720, 66wa 397 . . . . . 6 wff ((β„Ž βˆͺ ran (mVHβ€˜π‘‘)) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))
6867, 18cab 2710 . . . . 5 class {𝑐 ∣ ((β„Ž βˆͺ ran (mVHβ€˜π‘‘)) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))}
6968cint 4911 . . . 4 class ∩ {𝑐 ∣ ((β„Ž βˆͺ ran (mVHβ€˜π‘‘)) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))}
704, 5, 9, 12, 69cmpo 7363 . . 3 class (𝑑 ∈ 𝒫 (mDVβ€˜π‘‘), β„Ž ∈ 𝒫 (mExβ€˜π‘‘) ↦ ∩ {𝑐 ∣ ((β„Ž βˆͺ ran (mVHβ€˜π‘‘)) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))})
712, 3, 70cmpt 5192 . 2 class (𝑑 ∈ V ↦ (𝑑 ∈ 𝒫 (mDVβ€˜π‘‘), β„Ž ∈ 𝒫 (mExβ€˜π‘‘) ↦ ∩ {𝑐 ∣ ((β„Ž βˆͺ ran (mVHβ€˜π‘‘)) βŠ† 𝑐 ∧ βˆ€π‘šβˆ€π‘œβˆ€π‘(βŸ¨π‘š, π‘œ, π‘βŸ© ∈ (mAxβ€˜π‘‘) β†’ βˆ€π‘  ∈ ran (mSubstβ€˜π‘‘)(((𝑠 β€œ (π‘œ βˆͺ ran (mVHβ€˜π‘‘))) βŠ† 𝑐 ∧ βˆ€π‘₯βˆ€π‘¦(π‘₯π‘šπ‘¦ β†’ (((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘₯))) Γ— ((mVarsβ€˜π‘‘)β€˜(π‘ β€˜((mVHβ€˜π‘‘)β€˜π‘¦)))) βŠ† 𝑑)) β†’ (π‘ β€˜π‘) ∈ 𝑐)))}))
721, 71wceq 1542 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  34219  mclsval  34221
  Copyright terms: Public domain W3C validator