Theorem resshom

Description: Hom is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017)

	Ref	Expression
Hypotheses	resshom.1	⊢ 𝐷 = ( 𝐶 ↾s 𝐴 )
	resshom.2	⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion	resshom	⊢ ( 𝐴 ∈ 𝑉 → 𝐻 = ( Hom ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		resshom.1	⊢ 𝐷 = ( 𝐶 ↾s 𝐴 )
2		resshom.2	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		homid	⊢ Hom = Slot ( Hom ‘ ndx )
4		slotsbhcdif	⊢ ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) )
5		simp1	⊢ ( ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) ) → ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) )
6	5	necomd	⊢ ( ( ( Base ‘ ndx ) ≠ ( Hom ‘ ndx ) ∧ ( Base ‘ ndx ) ≠ ( comp ‘ ndx ) ∧ ( Hom ‘ ndx ) ≠ ( comp ‘ ndx ) ) → ( Hom ‘ ndx ) ≠ ( Base ‘ ndx ) )
7	4 6	ax-mp	⊢ ( Hom ‘ ndx ) ≠ ( Base ‘ ndx )
8	1 2 3 7	resseqnbas	⊢ ( 𝐴 ∈ 𝑉 → 𝐻 = ( Hom ‘ 𝐷 ) )