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	⊢ 𝐷 = ( mDV ‘ 𝑇 )
	mclsval.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
	mclsval.c	⊢ 𝐶 = ( mCls ‘ 𝑇 )
	mclsval.1	⊢ ( 𝜑 → 𝑇 ∈ mFS )
	mclsval.2	⊢ ( 𝜑 → 𝐾 ⊆ 𝐷 )
	mclsval.3	⊢ ( 𝜑 → 𝐵 ⊆ 𝐸 )
Assertion	mclsssv	⊢ ( 𝜑 → ( 𝐾 𝐶 𝐵 ) ⊆ 𝐸 )

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		eqid	⊢ ( mVH ‘ 𝑇 ) = ( mVH ‘ 𝑇 )
8		eqid	⊢ ( mAx ‘ 𝑇 ) = ( mAx ‘ 𝑇 )
9		eqid	⊢ ( mSubst ‘ 𝑇 ) = ( mSubst ‘ 𝑇 )
10		eqid	⊢ ( mVars ‘ 𝑇 ) = ( mVars ‘ 𝑇 )
11	1 2 3 4 5 6 7 8 9 10	mclsval	⊢ ( 𝜑 → ( 𝐾 𝐶 𝐵 ) = ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } )
12	1 2 3 4 5 6 7 8 9 10	mclsssvlem	⊢ ( 𝜑 → ∩ { 𝑐 ∣ ( ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ 𝑐 ∧ ∀ 𝑚 ∀ 𝑜 ∀ 𝑝 ( ⟨ 𝑚 , 𝑜 , 𝑝 ⟩ ∈ ( mAx ‘ 𝑇 ) → ∀ 𝑠 ∈ ran ( mSubst ‘ 𝑇 ) ( ( ( 𝑠 “ ( 𝑜 ∪ ran ( mVH ‘ 𝑇 ) ) ) ⊆ 𝑐 ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑚 𝑦 → ( ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑥 ) ) ) × ( ( mVars ‘ 𝑇 ) ‘ ( 𝑠 ‘ ( ( mVH ‘ 𝑇 ) ‘ 𝑦 ) ) ) ) ⊆ 𝐾 ) ) → ( 𝑠 ‘ 𝑝 ) ∈ 𝑐 ) ) ) } ⊆ 𝐸 )
13	11 12	eqsstrd	⊢ ( 𝜑 → ( 𝐾 𝐶 𝐵 ) ⊆ 𝐸 )