Theorem vhmcls

Description: All variable hypotheses are in the closure. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mclsval.d	$$⊢D=\mathrm{mDV}\left(T\right)$$
	mclsval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
	mclsval.c	$$⊢C=\mathrm{mCls}\left(T\right)$$
	mclsval.1	$$⊢\phi \to T\in \mathrm{mFS}$$
	mclsval.2	$$⊢\phi \to K\subseteq D$$
	mclsval.3	$$⊢\phi \to B\subseteq E$$
	ssmclslem.h	$$⊢H=\mathrm{mVH}\left(T\right)$$
	vhmcls.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
	vhmcls.3	$$⊢\phi \to X\in V$$
Assertion	vhmcls	$$⊢\phi \to H\left(X\right)\in \left(KCB\right)$$

Proof

Step	Hyp	Ref	Expression
1		mclsval.d	$$⊢D=\mathrm{mDV}\left(T\right)$$
2		mclsval.e	$$⊢E=\mathrm{mEx}\left(T\right)$$
3		mclsval.c	$$⊢C=\mathrm{mCls}\left(T\right)$$
4		mclsval.1	$$⊢\phi \to T\in \mathrm{mFS}$$
5		mclsval.2	$$⊢\phi \to K\subseteq D$$
6		mclsval.3	$$⊢\phi \to B\subseteq E$$
7		ssmclslem.h	$$⊢H=\mathrm{mVH}\left(T\right)$$
8		vhmcls.v	$$⊢V=\mathrm{mVR}\left(T\right)$$
9		vhmcls.3	$$⊢\phi \to X\in V$$
10	1 2 3 4 5 6 7	ssmclslem	$$⊢\phi \to B\cup \mathrm{ran}H\subseteq KCB$$
11	10	unssbd	$$⊢\phi \to \mathrm{ran}H\subseteq KCB$$
12	8 2 7	mvhf	$$⊢T\in \mathrm{mFS}\to H:V⟶E$$
13		ffn	$$⊢H:V⟶E\to HFnV$$
14	4 12 13	3syl	$$⊢\phi \to HFnV$$
15		fnfvelrn	$$⊢\left(HFnV\wedge X\in V\right)\to H\left(X\right)\in \mathrm{ran}H$$
16	14 9 15	syl2anc	$$⊢\phi \to H\left(X\right)\in \mathrm{ran}H$$
17	11 16	sseldd	$$⊢\phi \to H\left(X\right)\in \left(KCB\right)$$