Theorem lmdpropd

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

	Ref	Expression
Hypotheses	lmdpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
	lmdpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
	lmdpropd.3	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
	lmdpropd.4	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
	lmdpropd.a	$$⊢\phi \to A\in V$$
	lmdpropd.b	$$⊢\phi \to B\in V$$
	lmdpropd.c	$$⊢\phi \to C\in V$$
	lmdpropd.d	$$⊢\phi \to D\in V$$
Assertion	lmdpropd	Could not format assertion : No typesetting found for |- ( ph -> ( A Limit C ) = ( B Limit D ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		lmdpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
2		lmdpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
3		lmdpropd.3	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
4		lmdpropd.4	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
5		lmdpropd.a	$$⊢\phi \to A\in V$$
6		lmdpropd.b	$$⊢\phi \to B\in V$$
7		lmdpropd.c	$$⊢\phi \to C\in V$$
8		lmdpropd.d	$$⊢\phi \to D\in V$$
9	3 4 1 2 7 8 5 6	funcpropd	$$⊢\phi \to C\mathrm{Func}A=D\mathrm{Func}B$$
10	1	adantr	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
11	10	oppchomfpropd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(A\right)\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(B\right)\right)$$
12	2	adantr	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
13	10 12	oppccomfpropd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(A\right)\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(B\right)\right)$$
14	3	adantr	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
15	4	adantr	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
16		simpr	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to f\in \left(C\mathrm{Func}A\right)$$
17	16	func1st2nd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to 1^{st}\left(f\right)\left(C\mathrm{Func}A\right)2^{nd}\left(f\right)$$
18	17	funcrcl2	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to C\in \mathrm{Cat}$$
19	9	adantr	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to C\mathrm{Func}A=D\mathrm{Func}B$$
20	16 19	eleqtrd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to f\in \left(D\mathrm{Func}B\right)$$
21	20	func1st2nd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to 1^{st}\left(f\right)\left(D\mathrm{Func}B\right)2^{nd}\left(f\right)$$
22	21	funcrcl2	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to D\in \mathrm{Cat}$$
23	17	funcrcl3	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to A\in \mathrm{Cat}$$
24	21	funcrcl3	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to B\in \mathrm{Cat}$$
25	14 15 10 12 18 22 23 24	fucpropd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to C\mathrm{FuncCat}A=D\mathrm{FuncCat}B$$
26	25	fveq2d	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{Hom}}_{𝑓}\left(C\mathrm{FuncCat}A\right)={\mathrm{Hom}}_{𝑓}\left(D\mathrm{FuncCat}B\right)$$
27	26	oppchomfpropd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(C\mathrm{FuncCat}A\right)\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(D\mathrm{FuncCat}B\right)\right)$$
28	25	fveq2d	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{comp}}_{𝑓}\left(C\mathrm{FuncCat}A\right)={\mathrm{comp}}_{𝑓}\left(D\mathrm{FuncCat}B\right)$$
29	26 28	oppccomfpropd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to {\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(C\mathrm{FuncCat}A\right)\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(D\mathrm{FuncCat}B\right)\right)$$
30		fvexd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to \mathrm{oppCat}\left(A\right)\in \mathrm{V}$$
31		fvexd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to \mathrm{oppCat}\left(B\right)\in \mathrm{V}$$
32		fvexd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to \mathrm{oppCat}\left(C\mathrm{FuncCat}A\right)\in \mathrm{V}$$
33		fvexd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to \mathrm{oppCat}\left(D\mathrm{FuncCat}B\right)\in \mathrm{V}$$
34	11 13 27 29 30 31 32 33	uppropd	Could not format ( ( ph /\ f e. ( C Func A ) ) -> ( ( oppCat ` A ) UP ( oppCat ` ( C FuncCat A ) ) ) = ( ( oppCat ` B ) UP ( oppCat ` ( D FuncCat B ) ) ) ) : No typesetting found for |- ( ( ph /\ f e. ( C Func A ) ) -> ( ( oppCat ` A ) UP ( oppCat ` ( C FuncCat A ) ) ) = ( ( oppCat ` B ) UP ( oppCat ` ( D FuncCat B ) ) ) ) with typecode |-
35	10 12 14 15 23 24 18 22	diagpropd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to A{\Delta }_{\mathrm{func}}C=B{\Delta }_{\mathrm{func}}D$$
36	35	fveq2d	Could not format ( ( ph /\ f e. ( C Func A ) ) -> ( oppFunc ` ( A DiagFunc C ) ) = ( oppFunc ` ( B DiagFunc D ) ) ) : No typesetting found for |- ( ( ph /\ f e. ( C Func A ) ) -> ( oppFunc ` ( A DiagFunc C ) ) = ( oppFunc ` ( B DiagFunc D ) ) ) with typecode |-
37		eqidd	$$⊢\left(\phi \wedge f\in \left(C\mathrm{Func}A\right)\right)\to f=f$$
38	34 36 37	oveq123d	Could not format ( ( ph /\ f e. ( C Func A ) ) -> ( ( oppFunc ` ( A DiagFunc C ) ) ( ( oppCat ` A ) UP ( oppCat ` ( C FuncCat A ) ) ) f ) = ( ( oppFunc ` ( B DiagFunc D ) ) ( ( oppCat ` B ) UP ( oppCat ` ( D FuncCat B ) ) ) f ) ) : No typesetting found for |- ( ( ph /\ f e. ( C Func A ) ) -> ( ( oppFunc ` ( A DiagFunc C ) ) ( ( oppCat ` A ) UP ( oppCat ` ( C FuncCat A ) ) ) f ) = ( ( oppFunc ` ( B DiagFunc D ) ) ( ( oppCat ` B ) UP ( oppCat ` ( D FuncCat B ) ) ) f ) ) with typecode |-
39	9 38	mpteq12dva	Could not format ( ph -> ( f e. ( C Func A ) |-> ( ( oppFunc ` ( A DiagFunc C ) ) ( ( oppCat ` A ) UP ( oppCat ` ( C FuncCat A ) ) ) f ) ) = ( f e. ( D Func B ) |-> ( ( oppFunc ` ( B DiagFunc D ) ) ( ( oppCat ` B ) UP ( oppCat ` ( D FuncCat B ) ) ) f ) ) ) : No typesetting found for |- ( ph -> ( f e. ( C Func A ) |-> ( ( oppFunc ` ( A DiagFunc C ) ) ( ( oppCat ` A ) UP ( oppCat ` ( C FuncCat A ) ) ) f ) ) = ( f e. ( D Func B ) |-> ( ( oppFunc ` ( B DiagFunc D ) ) ( ( oppCat ` B ) UP ( oppCat ` ( D FuncCat B ) ) ) f ) ) ) with typecode |-
40		lmdfval	Could not format ( A Limit C ) = ( f e. ( C Func A ) |-> ( ( oppFunc ` ( A DiagFunc C ) ) ( ( oppCat ` A ) UP ( oppCat ` ( C FuncCat A ) ) ) f ) ) : No typesetting found for |- ( A Limit C ) = ( f e. ( C Func A ) |-> ( ( oppFunc ` ( A DiagFunc C ) ) ( ( oppCat ` A ) UP ( oppCat ` ( C FuncCat A ) ) ) f ) ) with typecode |-
41		lmdfval	Could not format ( B Limit D ) = ( f e. ( D Func B ) |-> ( ( oppFunc ` ( B DiagFunc D ) ) ( ( oppCat ` B ) UP ( oppCat ` ( D FuncCat B ) ) ) f ) ) : No typesetting found for |- ( B Limit D ) = ( f e. ( D Func B ) |-> ( ( oppFunc ` ( B DiagFunc D ) ) ( ( oppCat ` B ) UP ( oppCat ` ( D FuncCat B ) ) ) f ) ) with typecode |-
42	39 40 41	3eqtr4g	Could not format ( ph -> ( A Limit C ) = ( B Limit D ) ) : No typesetting found for |- ( ph -> ( A Limit C ) = ( B Limit D ) ) with typecode |-