Metamath Proof Explorer

Theorem mclsssv

Description: The closure of a set of expressions is a set of expressions. (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
Assertion mclsssv ⊢ φ → K C B ⊆ E

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 eqid ⊢ mVH ⁡ T = mVH ⁡ T
8 eqid ⊢ mAx ⁡ T = mAx ⁡ T
9 eqid ⊢ mSubst ⁡ T = mSubst ⁡ T
10 eqid ⊢ mVars ⁡ T = mVars ⁡ T
11 1 2 3 4 5 6 7 8 9 10 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
12 1 2 3 4 5 6 7 8 9 10 mclsssvlem ⊢ φ → ⋂ 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 ⊆ E
13 11 12 eqsstrd ⊢ φ → K C B ⊆ E