Metamath Proof Explorer

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 
|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )
lanpropd.2 
|- ( ph -> ( comf ` A ) = ( comf ` B ) )
lanpropd.3 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
lanpropd.4 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
lanpropd.5 
|- ( ph -> ( Homf ` E ) = ( Homf ` F ) )
lanpropd.6 
|- ( ph -> ( comf ` E ) = ( comf ` F ) )
lanpropd.a 
|- ( ph -> A e. V )
lanpropd.b 
|- ( ph -> B e. V )
lanpropd.c 
|- ( ph -> C e. V )
lanpropd.d 
|- ( ph -> D e. V )
lanpropd.e 
|- ( ph -> E e. V )
lanpropd.f 
|- ( ph -> F e. V )
Assertion ranpropd 
|- ( ph -> ( <. A , C >. Ran E ) = ( <. B , D >. Ran F ) )

Proof

Step Hyp Ref Expression
1 lanpropd.1 
 |-  ( ph -> ( Homf ` A ) = ( Homf ` B ) )
2 lanpropd.2 
 |-  ( ph -> ( comf ` A ) = ( comf ` B ) )
3 lanpropd.3 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
4 lanpropd.4 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
5 lanpropd.5 
 |-  ( ph -> ( Homf ` E ) = ( Homf ` F ) )
6 lanpropd.6 
 |-  ( ph -> ( comf ` E ) = ( comf ` F ) )
7 lanpropd.a 
 |-  ( ph -> A e. V )
8 lanpropd.b 
 |-  ( ph -> B e. V )
9 lanpropd.c 
 |-  ( ph -> C e. V )
10 lanpropd.d 
 |-  ( ph -> D e. V )
11 lanpropd.e 
 |-  ( ph -> E e. V )
12 lanpropd.f 
 |-  ( ph -> F e. V )
13 1 2 3 4 7 8 9 10 funcpropd 
 |-  ( ph -> ( A Func C ) = ( B Func D ) )
14 1 2 5 6 7 8 11 12 funcpropd 
 |-  ( ph -> ( A Func E ) = ( B Func F ) )
15 14 adantr 
 |-  ( ( ph /\ f e. ( A Func C ) ) -> ( A Func E ) = ( B Func F ) )
16 3 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( Homf ` C ) = ( Homf ` D ) )
17 4 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( comf ` C ) = ( comf ` D ) )
18 5 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( Homf ` E ) = ( Homf ` F ) )
19 6 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( comf ` E ) = ( comf ` F ) )
20 funcrcl 
 |-  ( f e. ( A Func C ) -> ( A e. Cat /\ C e. Cat ) )
21 20 ad2antrl 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( A e. Cat /\ C e. Cat ) )
22 21 simprd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> C e. Cat )
23 10 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> D e. V )
24 16 17 22 23 catpropd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( C e. Cat <-> D e. Cat ) )
25 22 24 mpbid 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> D e. Cat )
26 funcrcl 
 |-  ( x e. ( A Func E ) -> ( A e. Cat /\ E e. Cat ) )
27 26 ad2antll 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( A e. Cat /\ E e. Cat ) )
28 27 simprd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> E e. Cat )
29 12 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> F e. V )
30 18 19 28 29 catpropd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( E e. Cat <-> F e. Cat ) )
31 28 30 mpbid 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> F e. Cat )
32 16 17 18 19 22 25 28 31 fucpropd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( C FuncCat E ) = ( D FuncCat F ) )
33 32 fveq2d 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( oppCat ` ( C FuncCat E ) ) = ( oppCat ` ( D FuncCat F ) ) )
34 1 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( Homf ` A ) = ( Homf ` B ) )
35 2 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( comf ` A ) = ( comf ` B ) )
36 21 simpld 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> A e. Cat )
37 8 adantr 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> B e. V )
38 34 35 36 37 catpropd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( A e. Cat <-> B e. Cat ) )
39 36 38 mpbid 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> B e. Cat )
40 34 35 18 19 36 39 28 31 fucpropd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( A FuncCat E ) = ( B FuncCat F ) )
41 40 fveq2d 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( oppCat ` ( A FuncCat E ) ) = ( oppCat ` ( B FuncCat F ) ) )
42 33 41 oveq12d 
 |-  ( ( 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 ) ) ) )
43 simprl 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> f e. ( A Func C ) )
44 16 17 18 19 22 25 28 31 43 prcofpropd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( <. C , E >. -o.F f ) = ( <. D , F >. -o.F f ) )
45 44 fveq2d 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( oppFunc ` ( <. C , E >. -o.F f ) ) = ( oppFunc ` ( <. D , F >. -o.F f ) ) )
46 eqidd 
 |-  ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> x = x )
47 42 45 46 oveq123d 
 |-  ( ( 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 ) )
48 13 15 47 mpoeq123dva 
 |-  ( 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 ) ) )
49 eqid 
 |-  ( C FuncCat E ) = ( C FuncCat E )
50 eqid 
 |-  ( A FuncCat E ) = ( A FuncCat E )
51 eqid 
 |-  ( oppCat ` ( C FuncCat E ) ) = ( oppCat ` ( C FuncCat E ) )
52 eqid 
 |-  ( oppCat ` ( A FuncCat E ) ) = ( oppCat ` ( A FuncCat E ) )
53 49 50 7 9 11 51 52 ranfval 
 |-  ( 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 ) ) )
54 eqid 
 |-  ( D FuncCat F ) = ( D FuncCat F )
55 eqid 
 |-  ( B FuncCat F ) = ( B FuncCat F )
56 eqid 
 |-  ( oppCat ` ( D FuncCat F ) ) = ( oppCat ` ( D FuncCat F ) )
57 eqid 
 |-  ( oppCat ` ( B FuncCat F ) ) = ( oppCat ` ( B FuncCat F ) )
58 54 55 8 10 12 56 57 ranfval 
 |-  ( 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 ) ) )
59 48 53 58 3eqtr4d 
 |-  ( ph -> ( <. A , C >. Ran E ) = ( <. B , D >. Ran F ) )