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 ⊢ φ → X C Y ⊆ K C B

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 ⊢ φ → x m y → mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ x × mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ y ⊆ X → x m y → mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ x × mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ y ⊆ K
15 14 2alimdv ⊢ φ → ∀ x ∀ y x m y → mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ x × mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ y ⊆ X → ∀ x ∀ y x m y → mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ x × mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ y ⊆ K
16 15 anim2d ⊢ φ → s o ∪ ran ⁡ mVH ⁡ T ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ x × mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ y ⊆ X → s o ∪ ran ⁡ mVH ⁡ T ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ x × mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ y ⊆ K
17 16 imim1d ⊢ φ → s o ∪ ran ⁡ mVH ⁡ T ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ x × mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ y ⊆ K → s ⁡ p ∈ c → s o ∪ ran ⁡ mVH ⁡ T ⊆ c ∧ ∀ x ∀ y x m y → mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ x × mVars ⁡ T ⁡ s ⁡ mVH ⁡ T ⁡ y ⊆ X → s ⁡ p ∈ c
18 17 ralimdv ⊢ φ → ∀ 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 ⊆ K → s ⁡ p ∈ c → ∀ 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 ⊆ X → s ⁡ p ∈ c
19 18 imim2d ⊢ φ → 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 ⊆ K → s ⁡ p ∈ c → 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 ⊆ X → s ⁡ p ∈ c
20 19 alimdv ⊢ φ → ∀ 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 ⊆ K → s ⁡ p ∈ c → ∀ 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 ⊆ X → s ⁡ p ∈ c
21 20 2alimdv ⊢ φ → ∀ 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 ⊆ K → s ⁡ p ∈ 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 ⊆ X → s ⁡ p ∈ c
22 11 21 anim12d ⊢ φ → B ∪ 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 ⊆ K → s ⁡ p ∈ c → Y ∪ 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 ⊆ X → s ⁡ p ∈ c
23 22 ss2abdv ⊢ φ → c | B ∪ 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 ⊆ K → s ⁡ p ∈ c ⊆ c | Y ∪ 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 ⊆ X → s ⁡ p ∈ c
24 intss ⊢ c | B ∪ 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 ⊆ K → s ⁡ p ∈ c ⊆ c | Y ∪ 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 ⊆ X → s ⁡ p ∈ c → ⋂ c | Y ∪ 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 ⊆ X → s ⁡ p ∈ c ⊆ ⋂ c | B ∪ 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 ⊆ K → s ⁡ p ∈ c
25 23 24 syl ⊢ φ → ⋂ c | Y ∪ 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 ⊆ X → s ⁡ p ∈ c ⊆ ⋂ c | B ∪ 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 ⊆ 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 ⊢ φ → X C Y = ⋂ c | Y ∪ 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 ⊆ X → s ⁡ p ∈ c
33 1 2 3 4 5 6 28 29 30 31 mclsval ⊢ φ → K C B = ⋂ c | B ∪ 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 ⊆ K → s ⁡ p ∈ c
34 25 32 33 3sstr4d ⊢ φ → X C Y ⊆ K C B