Theorem 1stf2

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 )
	1stfval.p	|- P = ( C 1stF D )
	1stf1.p	|- ( ph -> R e. B )
	1stf2.p	|- ( ph -> S e. B )
Assertion	1stf2	|- ( ph -> ( R ( 2nd ` P ) S ) = ( 1st |` ( 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		1stfval.p	|- P = ( C 1stF D )
7		1stf1.p	|- ( ph -> R e. B )
8		1stf2.p	|- ( ph -> S e. B )
9	1 2 3 4 5 6	1stfval	|- ( ph -> P = <. ( 1st |` B ) , ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) >. )
10		fo1st	|- 1st : _V -onto-> _V
11		fofun	|- ( 1st : _V -onto-> _V -> Fun 1st )
12	10 11	ax-mp	|- Fun 1st
13	2	fvexi	|- B e. _V
14		resfunexg	|- ( ( Fun 1st /\ B e. _V ) -> ( 1st |` B ) e. _V )
15	12 13 14	mp2an	|- ( 1st |` B ) e. _V
16	13 13	mpoex	|- ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) e. _V
17	15 16	op2ndd	|- ( P = <. ( 1st |` B ) , ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) >. -> ( 2nd ` P ) = ( x e. B , y e. B |-> ( 1st |` ( x H y ) ) ) )
18	9 17	syl	|- ( ph -> ( 2nd ` P ) = ( x e. B , y e. B |-> ( 1st |` ( 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 ) ) -> ( 1st |` ( x H y ) ) = ( 1st |` ( R H S ) ) )
23		ovex	|- ( R H S ) e. _V
24		resfunexg	|- ( ( Fun 1st /\ ( R H S ) e. _V ) -> ( 1st |` ( R H S ) ) e. _V )
25	12 23 24	mp2an	|- ( 1st |` ( R H S ) ) e. _V
26	25	a1i	|- ( ph -> ( 1st |` ( R H S ) ) e. _V )
27	18 22 7 8 26	ovmpod	|- ( ph -> ( R ( 2nd ` P ) S ) = ( 1st |` ( R H S ) ) )