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 ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → 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 class mCls
1 vt setvar t
2 cvv class V
3 vd setvar d
4 cmdv class mDV
5 1 cv setvar t
6 5 4 cfv class mDV ⁡ t
7 6 cpw class 𝒫 mDV ⁡ t
8 vh setvar h
9 cmex class mEx
10 5 9 cfv class mEx ⁡ t
11 10 cpw class 𝒫 mEx ⁡ t
12 vc setvar c
13 8 cv setvar h
14 cmvh class mVH
15 5 14 cfv class mVH ⁡ t
16 15 crn class ran ⁡ mVH ⁡ t
17 13 16 cun class h ∪ ran ⁡ mVH ⁡ t
18 12 cv setvar c
19 17 18 wss wff h ∪ ran ⁡ mVH ⁡ t ⊆ c
20 vm setvar m
21 vo setvar o
22 vp setvar p
23 20 cv setvar m
24 21 cv setvar o
25 22 cv setvar p
26 23 24 25 cotp class m o p
27 cmax class mAx
28 5 27 cfv class mAx ⁡ t
29 26 28 wcel wff m o p ∈ mAx ⁡ t
30 vs setvar s
31 cmsub class mSubst
32 5 31 cfv class mSubst ⁡ t
33 32 crn class ran ⁡ mSubst ⁡ t
34 30 cv setvar s
35 24 16 cun class o ∪ ran ⁡ mVH ⁡ t
36 34 35 cima class s o ∪ ran ⁡ mVH ⁡ t
37 36 18 wss wff s o ∪ ran ⁡ mVH ⁡ t ⊆ c
38 vx setvar x
39 vy setvar y
40 38 cv setvar x
41 39 cv setvar y
42 40 41 23 wbr wff x m y
43 cmvrs class mVars
44 5 43 cfv class mVars ⁡ t
45 40 15 cfv class mVH ⁡ t ⁡ x
46 45 34 cfv class s ⁡ mVH ⁡ t ⁡ x
47 46 44 cfv class mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x
48 41 15 cfv class mVH ⁡ t ⁡ y
49 48 34 cfv class s ⁡ mVH ⁡ t ⁡ y
50 49 44 cfv class mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y
51 47 50 cxp class mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y
52 3 cv setvar d
53 51 52 wss wff mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d
54 42 53 wi wff x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d
55 54 39 wal wff ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d
56 55 38 wal wff ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d
57 37 56 wa wff s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d
58 25 34 cfv class s ⁡ p
59 58 18 wcel wff s ⁡ p ∈ c
60 57 59 wi wff s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → 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 ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c
62 29 61 wi wff m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c
63 62 22 wal wff ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c
64 63 21 wal wff ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c
65 64 20 wal wff ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c
66 19 65 wa wff h ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c
67 66 12 cab class c | h ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → 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 ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c
69 3 8 7 11 68 cmpo class d ∈ 𝒫 mDV ⁡ t , h ∈ 𝒫 mEx ⁡ t ⟼ ⋂ c | h ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c
70 1 2 69 cmpt class t ∈ V ⟼ d ∈ 𝒫 mDV ⁡ t , h ∈ 𝒫 mEx ⁡ t ⟼ ⋂ c | h ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c
71 0 70 wceq wff mCls = t ∈ V ⟼ d ∈ 𝒫 mDV ⁡ t , h ∈ 𝒫 mEx ⁡ t ⟼ ⋂ c | h ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ m ∀ o ∀ p m o p ∈ mAx ⁡ t → ∀ s ∈ ran ⁡ mSubst ⁡ t s o ∪ ran ⁡ mVH ⁡ t ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ x × mVars ⁡ t ⁡ s ⁡ mVH ⁡ t ⁡ y ⊆ d → s ⁡ p ∈ c