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	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
	1stfpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
	1stfpropd.3	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
	1stfpropd.4	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
	1stfpropd.a	$$⊢\phi \to A\in \mathrm{Cat}$$
	1stfpropd.b	$$⊢\phi \to B\in \mathrm{Cat}$$
	1stfpropd.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	1stfpropd.d	$$⊢\phi \to D\in \mathrm{Cat}$$
Assertion	1stfpropd	$$⊢\phi \to A{1^{st}}_{F}C=B{1^{st}}_{F}D$$

Proof

Step	Hyp	Ref	Expression
1		1stfpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
2		1stfpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
3		1stfpropd.3	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
4		1stfpropd.4	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
5		1stfpropd.a	$$⊢\phi \to A\in \mathrm{Cat}$$
6		1stfpropd.b	$$⊢\phi \to B\in \mathrm{Cat}$$
7		1stfpropd.c	$$⊢\phi \to C\in \mathrm{Cat}$$
8		1stfpropd.d	$$⊢\phi \to D\in \mathrm{Cat}$$
9	1 2 3 4 5 6 7 8	xpcpropd	$$⊢\phi \to A{\times }_{c}C=B{\times }_{c}D$$
10	9	fveq2d	$$⊢\phi \to {\mathrm{Base}}_{\left(A{\times }_{c}C\right)}={\mathrm{Base}}_{\left(B{\times }_{c}D\right)}$$
11	10	reseq2d	$$⊢\phi \to {1^{st}\upharpoonright }_{{\mathrm{Base}}_{\left(A{\times }_{c}C\right)}}={1^{st}\upharpoonright }_{{\mathrm{Base}}_{\left(B{\times }_{c}D\right)}}$$
12	9	fveq2d	$$⊢\phi \to \mathrm{Hom}\left(A{\times }_{c}C\right)=\mathrm{Hom}\left(B{\times }_{c}D\right)$$
13	12	oveqd	$$⊢\phi \to x\mathrm{Hom}\left(A{\times }_{c}C\right)y=x\mathrm{Hom}\left(B{\times }_{c}D\right)y$$
14	13	reseq2d	$$⊢\phi \to {1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(A{\times }_{c}C\right)y\right)}={1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(B{\times }_{c}D\right)y\right)}$$
15	10 10 14	mpoeq123dv	$$⊢\phi \to \left(x\in {\mathrm{Base}}_{\left(A{\times }_{c}C\right)},y\in {\mathrm{Base}}_{\left(A{\times }_{c}C\right)}⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(A{\times }_{c}C\right)y\right)}\right)=\left(x\in {\mathrm{Base}}_{\left(B{\times }_{c}D\right)},y\in {\mathrm{Base}}_{\left(B{\times }_{c}D\right)}⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(B{\times }_{c}D\right)y\right)}\right)$$
16	11 15	opeq12d	$$⊢\phi \to ⟨{1^{st}\upharpoonright }_{{\mathrm{Base}}_{\left(A{\times }_{c}C\right)}},\left(x\in {\mathrm{Base}}_{\left(A{\times }_{c}C\right)},y\in {\mathrm{Base}}_{\left(A{\times }_{c}C\right)}⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(A{\times }_{c}C\right)y\right)}\right)⟩=⟨{1^{st}\upharpoonright }_{{\mathrm{Base}}_{\left(B{\times }_{c}D\right)}},\left(x\in {\mathrm{Base}}_{\left(B{\times }_{c}D\right)},y\in {\mathrm{Base}}_{\left(B{\times }_{c}D\right)}⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(B{\times }_{c}D\right)y\right)}\right)⟩$$
17		eqid	$$⊢A{\times }_{c}C=A{\times }_{c}C$$
18		eqid	$$⊢{\mathrm{Base}}_{\left(A{\times }_{c}C\right)}={\mathrm{Base}}_{\left(A{\times }_{c}C\right)}$$
19		eqid	$$⊢\mathrm{Hom}\left(A{\times }_{c}C\right)=\mathrm{Hom}\left(A{\times }_{c}C\right)$$
20		eqid	$$⊢A{1^{st}}_{F}C=A{1^{st}}_{F}C$$
21	17 18 19 5 7 20	1stfval	$$⊢\phi \to A{1^{st}}_{F}C=⟨{1^{st}\upharpoonright }_{{\mathrm{Base}}_{\left(A{\times }_{c}C\right)}},\left(x\in {\mathrm{Base}}_{\left(A{\times }_{c}C\right)},y\in {\mathrm{Base}}_{\left(A{\times }_{c}C\right)}⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(A{\times }_{c}C\right)y\right)}\right)⟩$$
22		eqid	$$⊢B{\times }_{c}D=B{\times }_{c}D$$
23		eqid	$$⊢{\mathrm{Base}}_{\left(B{\times }_{c}D\right)}={\mathrm{Base}}_{\left(B{\times }_{c}D\right)}$$
24		eqid	$$⊢\mathrm{Hom}\left(B{\times }_{c}D\right)=\mathrm{Hom}\left(B{\times }_{c}D\right)$$
25		eqid	$$⊢B{1^{st}}_{F}D=B{1^{st}}_{F}D$$
26	22 23 24 6 8 25	1stfval	$$⊢\phi \to B{1^{st}}_{F}D=⟨{1^{st}\upharpoonright }_{{\mathrm{Base}}_{\left(B{\times }_{c}D\right)}},\left(x\in {\mathrm{Base}}_{\left(B{\times }_{c}D\right)},y\in {\mathrm{Base}}_{\left(B{\times }_{c}D\right)}⟼{1^{st}\upharpoonright }_{\left(x\mathrm{Hom}\left(B{\times }_{c}D\right)y\right)}\right)⟩$$
27	16 21 26	3eqtr4d	$$⊢\phi \to A{1^{st}}_{F}C=B{1^{st}}_{F}D$$