Theorem rescval

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

	Ref	Expression
Hypothesis	rescval.1	⊢ 𝐷 = ( 𝐶 ↾cat 𝐻 )
Assertion	rescval	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊 ) → 𝐷 = ( ( 𝐶 ↾s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		rescval.1	⊢ 𝐷 = ( 𝐶 ↾cat 𝐻 )
2		elex	⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ V )
3		elex	⊢ ( 𝐻 ∈ 𝑊 → 𝐻 ∈ V )
4		simpl	⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → 𝑐 = 𝐶 )
5		simpr	⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ℎ = 𝐻 )
6	5	dmeqd	⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → dom ℎ = dom 𝐻 )
7	6	dmeqd	⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → dom dom ℎ = dom dom 𝐻 )
8	4 7	oveq12d	⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( 𝑐 ↾s dom dom ℎ ) = ( 𝐶 ↾s dom dom 𝐻 ) )
9	5	opeq2d	⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ⟨ ( Hom ‘ ndx ) , ℎ ⟩ = ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ )
10	8 9	oveq12d	⊢ ( ( 𝑐 = 𝐶 ∧ ℎ = 𝐻 ) → ( ( 𝑐 ↾s dom dom ℎ ) sSet ⟨ ( Hom ‘ ndx ) , ℎ ⟩ ) = ( ( 𝐶 ↾s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
11		df-resc	⊢ ↾cat = ( 𝑐 ∈ V , ℎ ∈ V ↦ ( ( 𝑐 ↾s dom dom ℎ ) sSet ⟨ ( Hom ‘ ndx ) , ℎ ⟩ ) )
12		ovex	⊢ ( ( 𝐶 ↾s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) ∈ V
13	10 11 12	ovmpoa	⊢ ( ( 𝐶 ∈ V ∧ 𝐻 ∈ V ) → ( 𝐶 ↾cat 𝐻 ) = ( ( 𝐶 ↾s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
14	2 3 13	syl2an	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊 ) → ( 𝐶 ↾cat 𝐻 ) = ( ( 𝐶 ↾s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )
15	1 14	syl5eq	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐻 ∈ 𝑊 ) → 𝐷 = ( ( 𝐶 ↾s dom dom 𝐻 ) sSet ⟨ ( Hom ‘ ndx ) , 𝐻 ⟩ ) )