This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐷 ) )