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∈V⟼d∈𝒫mDV⁡t,h∈𝒫mEx⁡t⟼⋂c|h∪ran⁡mVH⁡t⊆c∧∀m∀o∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmcls classmCls
1 vt setvart
2 cvv classV
3 vd setvard
4 cmdv classmDV
5 1 cv setvart
6 5 4 cfv classmDV⁡t
7 6 cpw class𝒫mDV⁡t
8 vh setvarh
9 cmex classmEx
10 5 9 cfv classmEx⁡t
11 10 cpw class𝒫mEx⁡t
12 vc setvarc
13 8 cv setvarh
14 cmvh classmVH
15 5 14 cfv classmVH⁡t
16 15 crn classran⁡mVH⁡t
17 13 16 cun classh∪ran⁡mVH⁡t
18 12 cv setvarc
19 17 18 wss wffh∪ran⁡mVH⁡t⊆c
20 vm setvarm
21 vo setvaro
22 vp setvarp
23 20 cv setvarm
24 21 cv setvaro
25 22 cv setvarp
26 23 24 25 cotp classmop
27 cmax classmAx
28 5 27 cfv classmAx⁡t
29 26 28 wcel wffmop∈mAx⁡t
30 vs setvars
31 cmsub classmSubst
32 5 31 cfv classmSubst⁡t
33 32 crn classran⁡mSubst⁡t
34 30 cv setvars
35 24 16 cun classo∪ran⁡mVH⁡t
36 34 35 cima classso∪ran⁡mVH⁡t
37 36 18 wss wffso∪ran⁡mVH⁡t⊆c
38 vx setvarx
39 vy setvary
40 38 cv setvarx
41 39 cv setvary
42 40 41 23 wbr wffxmy
43 cmvrs classmVars
44 5 43 cfv classmVars⁡t
45 40 15 cfv classmVH⁡t⁡x
46 45 34 cfv classs⁡mVH⁡t⁡x
47 46 44 cfv classmVars⁡t⁡s⁡mVH⁡t⁡x
48 41 15 cfv classmVH⁡t⁡y
49 48 34 cfv classs⁡mVH⁡t⁡y
50 49 44 cfv classmVars⁡t⁡s⁡mVH⁡t⁡y
51 47 50 cxp classmVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y
52 3 cv setvard
53 51 52 wss wffmVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d
54 42 53 wi wffxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d
55 54 39 wal wff∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d
56 55 38 wal wff∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d
57 37 56 wa wffso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d
58 25 34 cfv classs⁡p
59 58 18 wcel wffs⁡p∈c
60 57 59 wi wffso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c
61 60 30 33 wral wff∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c
62 29 61 wi wffmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c
63 62 22 wal wff∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c
64 63 21 wal wff∀o∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c
65 64 20 wal wff∀m∀o∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c
66 19 65 wa wffh∪ran⁡mVH⁡t⊆c∧∀m∀o∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c
67 66 12 cab classc|h∪ran⁡mVH⁡t⊆c∧∀m∀o∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c
68 67 cint class⋂c|h∪ran⁡mVH⁡t⊆c∧∀m∀o∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c
69 3 8 7 11 68 cmpo classd∈𝒫mDV⁡t,h∈𝒫mEx⁡t⟼⋂c|h∪ran⁡mVH⁡t⊆c∧∀m∀o∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c
70 1 2 69 cmpt classt∈V⟼d∈𝒫mDV⁡t,h∈𝒫mEx⁡t⟼⋂c|h∪ran⁡mVH⁡t⊆c∧∀m∀o∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c
71 0 70 wceq wffmCls=t∈V⟼d∈𝒫mDV⁡t,h∈𝒫mEx⁡t⟼⋂c|h∪ran⁡mVH⁡t⊆c∧∀m∀o∀pmop∈mAx⁡t→∀s∈ran⁡mSubst⁡tso∪ran⁡mVH⁡t⊆c∧∀x∀yxmy→mVars⁡t⁡s⁡mVH⁡t⁡x×mVars⁡t⁡s⁡mVH⁡t⁡y⊆d→s⁡p∈c