Theorem ssmcls

Description: The original expressions are also in the closure. (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	ssmcls	⊢ ( 𝜑 → 𝐵 ⊆ ( 𝐾 𝐶 𝐵 ) )

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	1 2 3 4 5 6 7	ssmclslem	⊢ ( 𝜑 → ( 𝐵 ∪ ran ( mVH ‘ 𝑇 ) ) ⊆ ( 𝐾 𝐶 𝐵 ) )
9	8	unssad	⊢ ( 𝜑 → 𝐵 ⊆ ( 𝐾 𝐶 𝐵 ) )