Theorem rescco

Description: Composition in the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 13-Oct-2024)

	Ref	Expression
Hypotheses	rescbas.d	|- D = ( C |`cat H )
	rescbas.b	|- B = ( Base ` C )
	rescbas.c	|- ( ph -> C e. V )
	rescbas.h	|- ( ph -> H Fn ( S X. S ) )
	rescbas.s	|- ( ph -> S C_ B )
	rescco.o	|- .x. = ( comp ` C )
Assertion	rescco	|- ( ph -> .x. = ( comp ` D ) )

Proof

Step	Hyp	Ref	Expression
1		rescbas.d	|- D = ( C |`cat H )
2		rescbas.b	|- B = ( Base ` C )
3		rescbas.c	|- ( ph -> C e. V )
4		rescbas.h	|- ( ph -> H Fn ( S X. S ) )
5		rescbas.s	|- ( ph -> S C_ B )
6		rescco.o	|- .x. = ( comp ` C )
7		ccoid	|- comp = Slot ( comp ` ndx )
8		slotsbhcdif	|- ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) )
9		simp3	|- ( ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) ) -> ( Hom ` ndx ) =/= ( comp ` ndx ) )
10	9	necomd	|- ( ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) ) -> ( comp ` ndx ) =/= ( Hom ` ndx ) )
11	8 10	ax-mp	|- ( comp ` ndx ) =/= ( Hom ` ndx )
12	7 11	setsnid	|- ( comp ` ( C |`s S ) ) = ( comp ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
13	2	fvexi	|- B e. _V
14	13	ssex	|- ( S C_ B -> S e. _V )
15	5 14	syl	|- ( ph -> S e. _V )
16		eqid	|- ( C |`s S ) = ( C |`s S )
17	16 6	ressco	|- ( S e. _V -> .x. = ( comp ` ( C |`s S ) ) )
18	15 17	syl	|- ( ph -> .x. = ( comp ` ( C |`s S ) ) )
19	1 3 15 4	rescval2	|- ( ph -> D = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
20	19	fveq2d	|- ( ph -> ( comp ` D ) = ( comp ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) )
21	12 18 20	3eqtr4a	|- ( ph -> .x. = ( comp ` D ) )