Metamath Proof Explorer

Theorem ss2mcls

Description: The closure is monotonic under subsets of the original set of expressions and the set of disjoint variable conditions. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mclsval.d ⊢ 𝐷 = ( mDV ‘ 𝑇 )
mclsval.e ⊢ 𝐸 = ( mEx ‘ 𝑇 )
mclsval.c ⊢ 𝐶 = ( mCls ‘ 𝑇 )
mclsval.1 ⊢ ( 𝜑 → 𝑇 ∈ mFS )
mclsval.2 ⊢ ( 𝜑 → 𝐾 ⊆ 𝐷 )
mclsval.3 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐸 )
ss2mcls.4 ⊢ ( 𝜑 → 𝑋 ⊆ 𝐾 )
ss2mcls.5 ⊢ ( 𝜑 → 𝑌 ⊆ 𝐵 )
Assertion ss2mcls ( 𝜑 → ( 𝑋 𝐶 𝑌 ) ⊆ ( 𝐾 𝐶 𝐵 ) )

Proof

Step Hyp Ref Expression
1 mclsval.d ⊢ 𝐷 = ( mDV ‘ 𝑇 )
2 mclsval.e ⊢ 𝐸 = ( mEx ‘ 𝑇 )
3 mclsval.c ⊢ 𝐶 = ( mCls ‘ 𝑇 )
4 mclsval.1 ⊢ ( 𝜑 → 𝑇 ∈ mFS )
5 mclsval.2 ⊢ ( 𝜑 → 𝐾 ⊆ 𝐷 )
6 mclsval.3 ⊢ ( 𝜑 → 𝐵 ⊆ 𝐸 )
7 ss2mcls.4 ⊢ ( 𝜑 → 𝑋 ⊆ 𝐾 )
8 ss2mcls.5 ⊢ ( 𝜑 → 𝑌 ⊆ 𝐵 )
9 unss1 ⊢ ( 𝑌 ⊆ 𝐵 → ( 𝑌 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) )
10 sstr2 ⊢ ( ( 𝑌 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) → ( ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 → ( 𝑌 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ) )
11 8 9 10 3syl ⊢ ( 𝜑 → ( ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 → ( 𝑌 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ) )
12 sstr2 ⊢ ( ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 → ( 𝑋 ⊆ 𝐾 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) )
13 7 12 syl5com ⊢ ( 𝜑 → ( ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) )
14 13 imim2d ⊢ ( 𝜑 → ( ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 ) → ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) )
15 14 2alimdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 ) → ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) )
16 15 anim2d ⊢ ( 𝜑 → ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 ) ) → ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) ) )
17 16 imim1d ⊢ ( 𝜑 → ( ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) → ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) )
18 17 ralimdv ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) )
19 18 imim2d ⊢ ( 𝜑 → ( ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) → ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) )
20 19 alimdv ⊢ ( 𝜑 → ( ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) → ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) )
21 20 2alimdv ⊢ ( 𝜑 → ( ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) → ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) )
22 11 21 anim12d ⊢ ( 𝜑 → ( ( ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) → ( ( 𝑌 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) ) )
23 22 ss2abdv ⊢ ( 𝜑 → { 𝑐 ∣ ( ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ { 𝑐 ∣ ( ( 𝑌 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
24 intss ⊢ ( { 𝑐 ∣ ( ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ { 𝑐 ∣ ( ( 𝑌 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } → ∩ { 𝑐 ∣ ( ( 𝑌 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
25 23 24 syl ⊢ ( 𝜑 → ∩ { 𝑐 ∣ ( ( 𝑌 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
26 7 5 sstrd ⊢ ( 𝜑 → 𝑋 ⊆ 𝐷 )
27 8 6 sstrd ⊢ ( 𝜑 → 𝑌 ⊆ 𝐸 )
28 eqid ⊢ ( mVH ‘ 𝑇 ) = ( mVH ‘ 𝑇 )
29 eqid ⊢ ( mAx ‘ 𝑇 ) = ( mAx ‘ 𝑇 )
30 eqid ⊢ ( mSubst ‘ 𝑇 ) = ( mSubst ‘ 𝑇 )
31 eqid ⊢ ( mVars ‘ 𝑇 ) = ( mVars ‘ 𝑇 )
32 1 2 3 4 26 27 28 29 30 31 mclsval ⊢ ( 𝜑 → ( 𝑋 𝐶 𝑌 ) = ∩ { 𝑐 ∣ ( ( 𝑌 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝑋 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
33 1 2 3 4 5 6 28 29 30 31 mclsval ⊢ ( 𝜑 → ( 𝐾 𝐶 𝐵 ) = ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
34 25 32 33 3sstr4d ⊢ ( 𝜑 → ( 𝑋 𝐶 𝑌 ) ⊆ ( 𝐾 𝐶 𝐵 ) )