Theorem ranpropd

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

	Ref	Expression
Hypotheses	lanpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
	lanpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
	lanpropd.3	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
	lanpropd.4	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
	lanpropd.5	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(E\right)={\mathrm{Hom}}_{𝑓}\left(F\right)$$
	lanpropd.6	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(E\right)={\mathrm{comp}}_{𝑓}\left(F\right)$$
	lanpropd.a	$$⊢\phi \to A\in V$$
	lanpropd.b	$$⊢\phi \to B\in V$$
	lanpropd.c	$$⊢\phi \to C\in V$$
	lanpropd.d	$$⊢\phi \to D\in V$$
	lanpropd.e	$$⊢\phi \to E\in V$$
	lanpropd.f	$$⊢\phi \to F\in V$$
Assertion	ranpropd	Could not format assertion : No typesetting found for |- ( ph -> ( <. A , C >. Ran E ) = ( <. B , D >. Ran F ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		lanpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
2		lanpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
3		lanpropd.3	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
4		lanpropd.4	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
5		lanpropd.5	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(E\right)={\mathrm{Hom}}_{𝑓}\left(F\right)$$
6		lanpropd.6	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(E\right)={\mathrm{comp}}_{𝑓}\left(F\right)$$
7		lanpropd.a	$$⊢\phi \to A\in V$$
8		lanpropd.b	$$⊢\phi \to B\in V$$
9		lanpropd.c	$$⊢\phi \to C\in V$$
10		lanpropd.d	$$⊢\phi \to D\in V$$
11		lanpropd.e	$$⊢\phi \to E\in V$$
12		lanpropd.f	$$⊢\phi \to F\in V$$
13	1 2 3 4 7 8 9 10	funcpropd	$$⊢\phi \to A\mathrm{Func}C=B\mathrm{Func}D$$
14	1 2 5 6 7 8 11 12	funcpropd	$$⊢\phi \to A\mathrm{Func}E=B\mathrm{Func}F$$
15	14	adantr	$$⊢\left(\phi \wedge f\in \left(A\mathrm{Func}C\right)\right)\to A\mathrm{Func}E=B\mathrm{Func}F$$
16	3	adantr	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
17	4	adantr	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
18	5	adantr	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to {\mathrm{Hom}}_{𝑓}\left(E\right)={\mathrm{Hom}}_{𝑓}\left(F\right)$$
19	6	adantr	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to {\mathrm{comp}}_{𝑓}\left(E\right)={\mathrm{comp}}_{𝑓}\left(F\right)$$
20		funcrcl	$$⊢f\in \left(A\mathrm{Func}C\right)\to \left(A\in \mathrm{Cat}\wedge C\in \mathrm{Cat}\right)$$
21	20	ad2antrl	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to \left(A\in \mathrm{Cat}\wedge C\in \mathrm{Cat}\right)$$
22	21	simprd	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to C\in \mathrm{Cat}$$
23	10	adantr	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to D\in V$$
24	16 17 22 23	catpropd	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to \left(C\in \mathrm{Cat}\leftrightarrow D\in \mathrm{Cat}\right)$$
25	22 24	mpbid	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to D\in \mathrm{Cat}$$
26		funcrcl	$$⊢x\in \left(A\mathrm{Func}E\right)\to \left(A\in \mathrm{Cat}\wedge E\in \mathrm{Cat}\right)$$
27	26	ad2antll	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to \left(A\in \mathrm{Cat}\wedge E\in \mathrm{Cat}\right)$$
28	27	simprd	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to E\in \mathrm{Cat}$$
29	12	adantr	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to F\in V$$
30	18 19 28 29	catpropd	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to \left(E\in \mathrm{Cat}\leftrightarrow F\in \mathrm{Cat}\right)$$
31	28 30	mpbid	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to F\in \mathrm{Cat}$$
32	16 17 18 19 22 25 28 31	fucpropd	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to C\mathrm{FuncCat}E=D\mathrm{FuncCat}F$$
33	32	fveq2d	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to \mathrm{oppCat}\left(C\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(D\mathrm{FuncCat}F\right)$$
34	1	adantr	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to {\mathrm{Hom}}_{𝑓}\left(A\right)={\mathrm{Hom}}_{𝑓}\left(B\right)$$
35	2	adantr	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to {\mathrm{comp}}_{𝑓}\left(A\right)={\mathrm{comp}}_{𝑓}\left(B\right)$$
36	21	simpld	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to A\in \mathrm{Cat}$$
37	8	adantr	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to B\in V$$
38	34 35 36 37	catpropd	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to \left(A\in \mathrm{Cat}\leftrightarrow B\in \mathrm{Cat}\right)$$
39	36 38	mpbid	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to B\in \mathrm{Cat}$$
40	34 35 18 19 36 39 28 31	fucpropd	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to A\mathrm{FuncCat}E=B\mathrm{FuncCat}F$$
41	40	fveq2d	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to \mathrm{oppCat}\left(A\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(B\mathrm{FuncCat}F\right)$$
42	33 41	oveq12d	Could not format ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( ( oppCat ` ( C FuncCat E ) ) UP ( oppCat ` ( A FuncCat E ) ) ) = ( ( oppCat ` ( D FuncCat F ) ) UP ( oppCat ` ( B FuncCat F ) ) ) ) : No typesetting found for |- ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( ( oppCat ` ( C FuncCat E ) ) UP ( oppCat ` ( A FuncCat E ) ) ) = ( ( oppCat ` ( D FuncCat F ) ) UP ( oppCat ` ( B FuncCat F ) ) ) ) with typecode |-
43		simprl	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to f\in \left(A\mathrm{Func}C\right)$$
44	16 17 18 19 22 25 28 31 43	prcofpropd	Could not format ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( <. C , E >. -o.F f ) = ( <. D , F >. -o.F f ) ) : No typesetting found for |- ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( <. C , E >. -o.F f ) = ( <. D , F >. -o.F f ) ) with typecode |-
45	44	fveq2d	Could not format ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( oppFunc ` ( <. C , E >. -o.F f ) ) = ( oppFunc ` ( <. D , F >. -o.F f ) ) ) : No typesetting found for |- ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( oppFunc ` ( <. C , E >. -o.F f ) ) = ( oppFunc ` ( <. D , F >. -o.F f ) ) ) with typecode |-
46		eqidd	$$⊢\left(\phi \wedge \left(f\in \left(A\mathrm{Func}C\right)\wedge x\in \left(A\mathrm{Func}E\right)\right)\right)\to x=x$$
47	42 45 46	oveq123d	Could not format ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( ( oppFunc ` ( <. C , E >. -o.F f ) ) ( ( oppCat ` ( C FuncCat E ) ) UP ( oppCat ` ( A FuncCat E ) ) ) x ) = ( ( oppFunc ` ( <. D , F >. -o.F f ) ) ( ( oppCat ` ( D FuncCat F ) ) UP ( oppCat ` ( B FuncCat F ) ) ) x ) ) : No typesetting found for |- ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( ( oppFunc ` ( <. C , E >. -o.F f ) ) ( ( oppCat ` ( C FuncCat E ) ) UP ( oppCat ` ( A FuncCat E ) ) ) x ) = ( ( oppFunc ` ( <. D , F >. -o.F f ) ) ( ( oppCat ` ( D FuncCat F ) ) UP ( oppCat ` ( B FuncCat F ) ) ) x ) ) with typecode |-
48	13 15 47	mpoeq123dva	Could not format ( ph -> ( f e. ( A Func C ) , x e. ( A Func E ) |-> ( ( oppFunc ` ( <. C , E >. -o.F f ) ) ( ( oppCat ` ( C FuncCat E ) ) UP ( oppCat ` ( A FuncCat E ) ) ) x ) ) = ( f e. ( B Func D ) , x e. ( B Func F ) |-> ( ( oppFunc ` ( <. D , F >. -o.F f ) ) ( ( oppCat ` ( D FuncCat F ) ) UP ( oppCat ` ( B FuncCat F ) ) ) x ) ) ) : No typesetting found for |- ( ph -> ( f e. ( A Func C ) , x e. ( A Func E ) |-> ( ( oppFunc ` ( <. C , E >. -o.F f ) ) ( ( oppCat ` ( C FuncCat E ) ) UP ( oppCat ` ( A FuncCat E ) ) ) x ) ) = ( f e. ( B Func D ) , x e. ( B Func F ) |-> ( ( oppFunc ` ( <. D , F >. -o.F f ) ) ( ( oppCat ` ( D FuncCat F ) ) UP ( oppCat ` ( B FuncCat F ) ) ) x ) ) ) with typecode |-
49		eqid	$$⊢C\mathrm{FuncCat}E=C\mathrm{FuncCat}E$$
50		eqid	$$⊢A\mathrm{FuncCat}E=A\mathrm{FuncCat}E$$
51		eqid	$$⊢\mathrm{oppCat}\left(C\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(C\mathrm{FuncCat}E\right)$$
52		eqid	$$⊢\mathrm{oppCat}\left(A\mathrm{FuncCat}E\right)=\mathrm{oppCat}\left(A\mathrm{FuncCat}E\right)$$
53	49 50 7 9 11 51 52	ranfval	Could not format ( ph -> ( <. A , C >. Ran E ) = ( f e. ( A Func C ) , x e. ( A Func E ) |-> ( ( oppFunc ` ( <. C , E >. -o.F f ) ) ( ( oppCat ` ( C FuncCat E ) ) UP ( oppCat ` ( A FuncCat E ) ) ) x ) ) ) : No typesetting found for |- ( ph -> ( <. A , C >. Ran E ) = ( f e. ( A Func C ) , x e. ( A Func E ) |-> ( ( oppFunc ` ( <. C , E >. -o.F f ) ) ( ( oppCat ` ( C FuncCat E ) ) UP ( oppCat ` ( A FuncCat E ) ) ) x ) ) ) with typecode |-
54		eqid	$$⊢D\mathrm{FuncCat}F=D\mathrm{FuncCat}F$$
55		eqid	$$⊢B\mathrm{FuncCat}F=B\mathrm{FuncCat}F$$
56		eqid	$$⊢\mathrm{oppCat}\left(D\mathrm{FuncCat}F\right)=\mathrm{oppCat}\left(D\mathrm{FuncCat}F\right)$$
57		eqid	$$⊢\mathrm{oppCat}\left(B\mathrm{FuncCat}F\right)=\mathrm{oppCat}\left(B\mathrm{FuncCat}F\right)$$
58	54 55 8 10 12 56 57	ranfval	Could not format ( ph -> ( <. B , D >. Ran F ) = ( f e. ( B Func D ) , x e. ( B Func F ) |-> ( ( oppFunc ` ( <. D , F >. -o.F f ) ) ( ( oppCat ` ( D FuncCat F ) ) UP ( oppCat ` ( B FuncCat F ) ) ) x ) ) ) : No typesetting found for |- ( ph -> ( <. B , D >. Ran F ) = ( f e. ( B Func D ) , x e. ( B Func F ) |-> ( ( oppFunc ` ( <. D , F >. -o.F f ) ) ( ( oppCat ` ( D FuncCat F ) ) UP ( oppCat ` ( B FuncCat F ) ) ) x ) ) ) with typecode |-
59	48 53 58	3eqtr4d	Could not format ( ph -> ( <. A , C >. Ran E ) = ( <. B , D >. Ran F ) ) : No typesetting found for |- ( ph -> ( <. A , C >. Ran E ) = ( <. B , D >. Ran F ) ) with typecode |-