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