Theorem vhmcls

Description: All variable hypotheses are 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	⊢ ( 𝜑 → 𝐵 ⊆ 𝐸 )
	ssmclslem.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
	vhmcls.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	vhmcls.3	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	vhmcls	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) ∈ ( 𝐾 𝐶 𝐵 ) )

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		ssmclslem.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
8		vhmcls.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
9		vhmcls.3	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10	1 2 3 4 5 6 7	ssmclslem	⊢ ( 𝜑 → ( 𝐵 ∪ ran 𝐻 ) ⊆ ( 𝐾 𝐶 𝐵 ) )
11	10	unssbd	⊢ ( 𝜑 → ran 𝐻 ⊆ ( 𝐾 𝐶 𝐵 ) )
12	8 2 7	mvhf	⊢ ( 𝑇 ∈ mFS → 𝐻 : 𝑉 ⟶ 𝐸 )
13		ffn	⊢ ( 𝐻 : 𝑉 ⟶ 𝐸 → 𝐻 Fn 𝑉 )
14	4 12 13	3syl	⊢ ( 𝜑 → 𝐻 Fn 𝑉 )
15		fnfvelrn	⊢ ( ( 𝐻 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐻 ‘ 𝑋 ) ∈ ran 𝐻 )
16	14 9 15	syl2anc	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) ∈ ran 𝐻 )
17	11 16	sseldd	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) ∈ ( 𝐾 𝐶 𝐵 ) )