Theorem 2ndf2

Description: Value of the first projection on a morphism. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	1stfval.t	|- T = ( C Xc. D )
	1stfval.b	|- B = ( Base ` T )
	1stfval.h	|- H = ( Hom ` T )
	1stfval.c	|- ( ph -> C e. Cat )
	1stfval.d	|- ( ph -> D e. Cat )
	2ndfval.p	|- Q = ( C 2ndF D )
	2ndf1.p	|- ( ph -> R e. B )
	2ndf2.p	|- ( ph -> S e. B )
Assertion	2ndf2	|- ( ph -> ( R ( 2nd ` Q ) S ) = ( 2nd |` ( R H S ) ) )

Proof

Step	Hyp	Ref	Expression
1		1stfval.t	|- T = ( C Xc. D )
2		1stfval.b	|- B = ( Base ` T )
3		1stfval.h	|- H = ( Hom ` T )
4		1stfval.c	|- ( ph -> C e. Cat )
5		1stfval.d	|- ( ph -> D e. Cat )
6		2ndfval.p	|- Q = ( C 2ndF D )
7		2ndf1.p	|- ( ph -> R e. B )
8		2ndf2.p	|- ( ph -> S e. B )
9	1 2 3 4 5 6	2ndfval	|- ( ph -> Q = <. ( 2nd |` B ) , ( x e. B , y e. B |-> ( 2nd |` ( x H y ) ) ) >. )
10		fo2nd	|- 2nd : _V -onto-> _V
11		fofun	|- ( 2nd : _V -onto-> _V -> Fun 2nd )
12	10 11	ax-mp	|- Fun 2nd
13	2	fvexi	|- B e. _V
14		resfunexg	|- ( ( Fun 2nd /\ B e. _V ) -> ( 2nd |` B ) e. _V )
15	12 13 14	mp2an	|- ( 2nd |` B ) e. _V
16	13 13	mpoex	|- ( x e. B , y e. B |-> ( 2nd |` ( x H y ) ) ) e. _V
17	15 16	op2ndd	|- ( Q = <. ( 2nd |` B ) , ( x e. B , y e. B |-> ( 2nd |` ( x H y ) ) ) >. -> ( 2nd ` Q ) = ( x e. B , y e. B |-> ( 2nd |` ( x H y ) ) ) )
18	9 17	syl	|- ( ph -> ( 2nd ` Q ) = ( x e. B , y e. B |-> ( 2nd |` ( x H y ) ) ) )
19		simprl	|- ( ( ph /\ ( x = R /\ y = S ) ) -> x = R )
20		simprr	|- ( ( ph /\ ( x = R /\ y = S ) ) -> y = S )
21	19 20	oveq12d	|- ( ( ph /\ ( x = R /\ y = S ) ) -> ( x H y ) = ( R H S ) )
22	21	reseq2d	|- ( ( ph /\ ( x = R /\ y = S ) ) -> ( 2nd |` ( x H y ) ) = ( 2nd |` ( R H S ) ) )
23		ovex	|- ( R H S ) e. _V
24		resfunexg	|- ( ( Fun 2nd /\ ( R H S ) e. _V ) -> ( 2nd |` ( R H S ) ) e. _V )
25	12 23 24	mp2an	|- ( 2nd |` ( R H S ) ) e. _V
26	25	a1i	|- ( ph -> ( 2nd |` ( R H S ) ) e. _V )
27	18 22 7 8 26	ovmpod	|- ( ph -> ( R ( 2nd ` Q ) S ) = ( 2nd |` ( R H S ) ) )