Theorem 1stfpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have same first projection functors. (Contributed by Zhi Wang, 20-Nov-2025)

	Ref	Expression
Hypotheses	1stfpropd.1	|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )
	1stfpropd.2	|- ( ph -> ( comf ` A ) = ( comf ` B ) )
	1stfpropd.3	|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
	1stfpropd.4	|- ( ph -> ( comf ` C ) = ( comf ` D ) )
	1stfpropd.a	|- ( ph -> A e. Cat )
	1stfpropd.b	|- ( ph -> B e. Cat )
	1stfpropd.c	|- ( ph -> C e. Cat )
	1stfpropd.d	|- ( ph -> D e. Cat )
Assertion	1stfpropd	|- ( ph -> ( A 1stF C ) = ( B 1stF D ) )

Proof

Step	Hyp	Ref	Expression
1		1stfpropd.1	|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )
2		1stfpropd.2	|- ( ph -> ( comf ` A ) = ( comf ` B ) )
3		1stfpropd.3	|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
4		1stfpropd.4	|- ( ph -> ( comf ` C ) = ( comf ` D ) )
5		1stfpropd.a	|- ( ph -> A e. Cat )
6		1stfpropd.b	|- ( ph -> B e. Cat )
7		1stfpropd.c	|- ( ph -> C e. Cat )
8		1stfpropd.d	|- ( ph -> D e. Cat )
9	1 2 3 4 5 6 7 8	xpcpropd	|- ( ph -> ( A Xc. C ) = ( B Xc. D ) )
10	9	fveq2d	|- ( ph -> ( Base ` ( A Xc. C ) ) = ( Base ` ( B Xc. D ) ) )
11	10	reseq2d	|- ( ph -> ( 1st |` ( Base ` ( A Xc. C ) ) ) = ( 1st |` ( Base ` ( B Xc. D ) ) ) )
12	9	fveq2d	|- ( ph -> ( Hom ` ( A Xc. C ) ) = ( Hom ` ( B Xc. D ) ) )
13	12	oveqd	|- ( ph -> ( x ( Hom ` ( A Xc. C ) ) y ) = ( x ( Hom ` ( B Xc. D ) ) y ) )
14	13	reseq2d	|- ( ph -> ( 1st |` ( x ( Hom ` ( A Xc. C ) ) y ) ) = ( 1st |` ( x ( Hom ` ( B Xc. D ) ) y ) ) )
15	10 10 14	mpoeq123dv	|- ( ph -> ( x e. ( Base ` ( A Xc. C ) ) , y e. ( Base ` ( A Xc. C ) ) |-> ( 1st |` ( x ( Hom ` ( A Xc. C ) ) y ) ) ) = ( x e. ( Base ` ( B Xc. D ) ) , y e. ( Base ` ( B Xc. D ) ) |-> ( 1st |` ( x ( Hom ` ( B Xc. D ) ) y ) ) ) )
16	11 15	opeq12d	|- ( ph -> <. ( 1st |` ( Base ` ( A Xc. C ) ) ) , ( x e. ( Base ` ( A Xc. C ) ) , y e. ( Base ` ( A Xc. C ) ) |-> ( 1st |` ( x ( Hom ` ( A Xc. C ) ) y ) ) ) >. = <. ( 1st |` ( Base ` ( B Xc. D ) ) ) , ( x e. ( Base ` ( B Xc. D ) ) , y e. ( Base ` ( B Xc. D ) ) |-> ( 1st |` ( x ( Hom ` ( B Xc. D ) ) y ) ) ) >. )
17		eqid	|- ( A Xc. C ) = ( A Xc. C )
18		eqid	|- ( Base ` ( A Xc. C ) ) = ( Base ` ( A Xc. C ) )
19		eqid	|- ( Hom ` ( A Xc. C ) ) = ( Hom ` ( A Xc. C ) )
20		eqid	|- ( A 1stF C ) = ( A 1stF C )
21	17 18 19 5 7 20	1stfval	|- ( ph -> ( A 1stF C ) = <. ( 1st |` ( Base ` ( A Xc. C ) ) ) , ( x e. ( Base ` ( A Xc. C ) ) , y e. ( Base ` ( A Xc. C ) ) |-> ( 1st |` ( x ( Hom ` ( A Xc. C ) ) y ) ) ) >. )
22		eqid	|- ( B Xc. D ) = ( B Xc. D )
23		eqid	|- ( Base ` ( B Xc. D ) ) = ( Base ` ( B Xc. D ) )
24		eqid	|- ( Hom ` ( B Xc. D ) ) = ( Hom ` ( B Xc. D ) )
25		eqid	|- ( B 1stF D ) = ( B 1stF D )
26	22 23 24 6 8 25	1stfval	|- ( ph -> ( B 1stF D ) = <. ( 1st |` ( Base ` ( B Xc. D ) ) ) , ( x e. ( Base ` ( B Xc. D ) ) , y e. ( Base ` ( B Xc. D ) ) |-> ( 1st |` ( x ( Hom ` ( B Xc. D ) ) y ) ) ) >. )
27	16 21 26	3eqtr4d	|- ( ph -> ( A 1stF C ) = ( B 1stF D ) )