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

Detailed syntax breakdown

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