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 ⊢D=mDV⁡T
mclsval.e ⊢E=mEx⁡T
mclsval.c ⊢C=mCls⁡T
mclsval.1 ⊢φ→T∈mFS
mclsval.2 ⊢φ→K⊆D
mclsval.3 ⊢φ→B⊆E
ss2mcls.4 ⊢φ→X⊆K
ss2mcls.5 ⊢φ→Y⊆B
Assertion ss2mcls ⊢φ→XCY⊆KCB

Proof

Step Hyp Ref Expression
1 mclsval.d ⊢D=mDV⁡T
2 mclsval.e ⊢E=mEx⁡T
3 mclsval.c ⊢C=mCls⁡T
4 mclsval.1 ⊢φ→T∈mFS
5 mclsval.2 ⊢φ→K⊆D
6 mclsval.3 ⊢φ→B⊆E
7 ss2mcls.4 ⊢φ→X⊆K
8 ss2mcls.5 ⊢φ→Y⊆B
9 unss1 ⊢Y⊆B→Y∪ran⁡mVH⁡T⊆B∪ran⁡mVH⁡T
10 sstr2 ⊢Y∪ran⁡mVH⁡T⊆B∪ran⁡mVH⁡T→B∪ran⁡mVH⁡T⊆c→Y∪ran⁡mVH⁡T⊆c
11 8 9 10 3syl ⊢φ→B∪ran⁡mVH⁡T⊆c→Y∪ran⁡mVH⁡T⊆c
12 sstr2 ⊢mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆X→X⊆K→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆K
13 7 12 syl5com ⊢φ→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆X→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆K
14 13 imim2d ⊢φ→xmy→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆X→xmy→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆K
15 14 2alimdv ⊢φ→∀x∀yxmy→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆X→∀x∀yxmy→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆K
16 15 anim2d ⊢φ→so∪ran⁡mVH⁡T⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆X→so∪ran⁡mVH⁡T⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆K
17 16 imim1d ⊢φ→so∪ran⁡mVH⁡T⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆K→s⁡p∈c→so∪ran⁡mVH⁡T⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆X→s⁡p∈c
18 17 ralimdv ⊢φ→∀s∈ran⁡mSubst⁡Tso∪ran⁡mVH⁡T⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆K→s⁡p∈c→∀s∈ran⁡mSubst⁡Tso∪ran⁡mVH⁡T⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆X→s⁡p∈c
19 18 imim2d ⊢φ→mop∈mAx⁡T→∀s∈ran⁡mSubst⁡Tso∪ran⁡mVH⁡T⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆K→s⁡p∈c→mop∈mAx⁡T→∀s∈ran⁡mSubst⁡Tso∪ran⁡mVH⁡T⊆c∧∀x∀yxmy→mVars⁡T⁡s⁡mVH⁡T⁡x×mVars⁡T⁡s⁡mVH⁡T⁡y⊆X→s⁡p∈c
20 19 alimdv ⊢φ→∀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⊆K→s⁡p∈c→∀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⊆X→s⁡p∈c
21 20 2alimdv ⊢φ→∀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⊆K→s⁡p∈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⊆X→s⁡p∈c
22 11 21 anim12d ⊢φ→B∪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⊆K→s⁡p∈c→Y∪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⊆X→s⁡p∈c
23 22 ss2abdv ⊢φ→c|B∪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⊆K→s⁡p∈c⊆c|Y∪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⊆X→s⁡p∈c
24 intss ⊢c|B∪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⊆K→s⁡p∈c⊆c|Y∪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⊆X→s⁡p∈c→⋂c|Y∪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⊆X→s⁡p∈c⊆⋂c|B∪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⊆K→s⁡p∈c
25 23 24 syl ⊢φ→⋂c|Y∪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⊆X→s⁡p∈c⊆⋂c|B∪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⊆K→s⁡p∈c
26 7 5 sstrd ⊢φ→X⊆D
27 8 6 sstrd ⊢φ→Y⊆E
28 eqid ⊢mVH⁡T=mVH⁡T
29 eqid ⊢mAx⁡T=mAx⁡T
30 eqid ⊢mSubst⁡T=mSubst⁡T
31 eqid ⊢mVars⁡T=mVars⁡T
32 1 2 3 4 26 27 28 29 30 31 mclsval ⊢φ→XCY=⋂c|Y∪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⊆X→s⁡p∈c
33 1 2 3 4 5 6 28 29 30 31 mclsval ⊢φ→KCB=⋂c|B∪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⊆K→s⁡p∈c
34 25 32 33 3sstr4d ⊢φ→XCY⊆KCB