Theorem rescbas

Description: Base set of the category restriction. (Contributed by Mario Carneiro, 4-Jan-2017)

	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		1re	|- 1 e. RR
8		1nn	|- 1 e. NN
9		4nn0	|- 4 e. NN0
10		1nn0	|- 1 e. NN0
11		1lt10	|- 1 < ; 1 0
12	8 9 10 11	declti	|- 1 < ; 1 4
13	7 12	ltneii	|- 1 =/= ; 1 4
14		basendx	|- ( Base ` ndx ) = 1
15		homndx	|- ( Hom ` ndx ) = ; 1 4
16	14 15	neeq12i	|- ( ( Base ` ndx ) =/= ( Hom ` ndx ) <-> 1 =/= ; 1 4 )
17	13 16	mpbir	|- ( Base ` ndx ) =/= ( Hom ` ndx )
18	6 17	setsnid	|- ( Base ` ( C |`s S ) ) = ( Base ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
19		eqid	|- ( C |`s S ) = ( C |`s S )
20	19 2	ressbas2	|- ( S C_ B -> S = ( Base ` ( C |`s S ) ) )
21	5 20	syl	|- ( ph -> S = ( Base ` ( C |`s S ) ) )
22	2	fvexi	|- B e. _V
23	22	ssex	|- ( S C_ B -> S e. _V )
24	5 23	syl	|- ( ph -> S e. _V )
25	1 3 24 4	rescval2	|- ( ph -> D = ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) )
26	25	fveq2d	|- ( ph -> ( Base ` D ) = ( Base ` ( ( C |`s S ) sSet <. ( Hom ` ndx ) , H >. ) ) )
27	18 21 26	3eqtr4a	|- ( ph -> S = ( Base ` D ) )