Theorem rescval2

Description: Value of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	rescval.1	⊢ 𝐷 = ( 𝐶 ↾cat 𝐻 )
	rescval2.1	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	rescval2.2	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
	rescval2.3	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
Assertion	rescval2	⊢ ( 𝜑 → 𝐷 = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		rescval.1	⊢ 𝐷 = ( 𝐶 ↾cat 𝐻 )
2		rescval2.1	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
3		rescval2.2	⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
4		rescval2.3	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
5	3 3	xpexd	⊢ ( 𝜑 → ( 𝑆 × 𝑆 ) ∈ V )
6		fnex	⊢ ( ( 𝐻 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝑆 × 𝑆 ) ∈ V ) → 𝐻 ∈ V )
7	4 5 6	syl2anc	⊢ ( 𝜑 → 𝐻 ∈ V )
8	1	rescval	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐻 ∈ V ) → 𝐷 = ( ( 𝐶 ↾s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
9	2 7 8	syl2anc	⊢ ( 𝜑 → 𝐷 = ( ( 𝐶 ↾s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
10	4	fndmd	⊢ ( 𝜑 → dom 𝐻 = ( 𝑆 × 𝑆 ) )
11	10	dmeqd	⊢ ( 𝜑 → dom dom 𝐻 = dom ( 𝑆 × 𝑆 ) )
12		dmxpid	⊢ dom ( 𝑆 × 𝑆 ) = 𝑆
13	11 12	eqtrdi	⊢ ( 𝜑 → dom dom 𝐻 = 𝑆 )
14	13	oveq2d	⊢ ( 𝜑 → ( 𝐶 ↾s dom dom 𝐻 ) = ( 𝐶 ↾s 𝑆 ) )
15	14	oveq1d	⊢ ( 𝜑 → ( ( 𝐶 ↾s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
16	9 15	eqtrd	⊢ ( 𝜑 → 𝐷 = ( ( 𝐶 ↾s 𝑆 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )