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

Metamath Proof Explorer

Theorem ressco

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

Ref Expression
Hypotheses resshom.1 
|- D = ( C |`s A )
ressco.2 
|- .x. = ( comp ` C )
Assertion ressco 
|- ( A e. V -> .x. = ( comp ` D ) )

Proof

Step Hyp Ref Expression
1 resshom.1 
 |-  D = ( C |`s A )
2 ressco.2 
 |-  .x. = ( comp ` C )
3 ccoid 
 |-  comp = Slot ( comp ` ndx )
4 slotsbhcdif 
 |-  ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) )
5 simp2 
 |-  ( ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) ) -> ( Base ` ndx ) =/= ( comp ` ndx ) )
6 5 necomd 
 |-  ( ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) ) -> ( comp ` ndx ) =/= ( Base ` ndx ) )
7 4 6 ax-mp 
 |-  ( comp ` ndx ) =/= ( Base ` ndx )
8 1 2 3 7 resseqnbas 
 |-  ( A e. V -> .x. = ( comp ` D ) )