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 ( 𝜑 → ( 𝑋 𝐶 𝑌 ) ⊆ ( 𝐾 𝐶 𝐵 ) )