Theorem rescbas

Description: Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof shortened by AV, 18-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 )
Assertion	rescbas	|- ( ph -> S = ( Base ` 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		baseid	|- Base = Slot ( Base ` ndx )
7		slotsbhcdif	|- ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) )
8	7	simp1i	|- ( Base ` ndx ) =/= ( Hom ` ndx )
9	6 8	setsnid	|- ( Base ` ( C |`s S ) ) = ( Base ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
10		eqid	|- ( C |`s S ) = ( C |`s S )
11	10 2	ressbas2	|- ( S C_ B -> S = ( Base ` ( C |`s S ) ) )
12	5 11	syl	|- ( ph -> S = ( Base ` ( C |`s S ) ) )
13	2	fvexi	|- B e. _V
14	13	ssex	|- ( S C_ B -> S e. _V )
15	5 14	syl	|- ( ph -> S e. _V )
16	1 3 15 4	rescval2	|- ( ph -> D = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
17	16	fveq2d	|- ( ph -> ( Base ` D ) = ( Base ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) )
18	9 12 17	3eqtr4a	|- ( ph -> S = ( Base ` D ) )