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 
|- D = ( C |`s A )
resshom.2 
|- H = ( Hom ` C )
Assertion resshom 
|- ( A e. V -> H = ( Hom ` D ) )

Proof

Step Hyp Ref Expression
1 resshom.1 
 |-  D = ( C |`s A )
2 resshom.2 
 |-  H = ( Hom ` C )
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 
 |-  ( A e. V -> H = ( Hom ` D ) )