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 ⊢ ( 𝜑 → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
lanpropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
lanpropd.3 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
lanpropd.4 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
lanpropd.5 ⊢ ( 𝜑 → ( Homf ‘ 𝐸 ) = ( Homf ‘ 𝐹 ) )
lanpropd.6 ⊢ ( 𝜑 → ( compf ‘ 𝐸 ) = ( compf ‘ 𝐹 ) )
lanpropd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
lanpropd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
lanpropd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
lanpropd.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
lanpropd.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
lanpropd.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
Assertion ranpropd ( 𝜑 → ( ⟨ 𝐴 , 𝐶 ⟩ Ran 𝐸 ) = ( ⟨ 𝐵 , 𝐷 ⟩ Ran 𝐹 ) )

Proof

Step Hyp Ref Expression
1 lanpropd.1 ⊢ ( 𝜑 → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
2 lanpropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
3 lanpropd.3 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
4 lanpropd.4 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
5 lanpropd.5 ⊢ ( 𝜑 → ( Homf ‘ 𝐸 ) = ( Homf ‘ 𝐹 ) )
6 lanpropd.6 ⊢ ( 𝜑 → ( compf ‘ 𝐸 ) = ( compf ‘ 𝐹 ) )
7 lanpropd.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
8 lanpropd.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
9 lanpropd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
10 lanpropd.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
11 lanpropd.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
12 lanpropd.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
13 1 2 3 4 7 8 9 10 funcpropd ⊢ ( 𝜑 → ( 𝐴 Func 𝐶 ) = ( 𝐵 Func 𝐷 ) )
14 1 2 5 6 7 8 11 12 funcpropd ⊢ ( 𝜑 → ( 𝐴 Func 𝐸 ) = ( 𝐵 Func 𝐹 ) )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 Func 𝐶 ) ) → ( 𝐴 Func 𝐸 ) = ( 𝐵 Func 𝐹 ) )
16 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
17 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
18 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( Homf ‘ 𝐸 ) = ( Homf ‘ 𝐹 ) )
19 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( compf ‘ 𝐸 ) = ( compf ‘ 𝐹 ) )
20 funcrcl ⊢ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) → ( 𝐴 ∈ Cat ∧ 𝐶 ∈ Cat ) )
21 20 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( 𝐴 ∈ Cat ∧ 𝐶 ∈ Cat ) )
22 21 simprd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝐶 ∈ Cat )
23 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝐷 ∈ 𝑉 )
24 16 17 22 23 catpropd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( 𝐶 ∈ Cat ↔ 𝐷 ∈ Cat ) )
25 22 24 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝐷 ∈ Cat )
26 funcrcl ⊢ ( 𝑥 ∈ ( 𝐴 Func 𝐸 ) → ( 𝐴 ∈ Cat ∧ 𝐸 ∈ Cat ) )
27 26 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( 𝐴 ∈ Cat ∧ 𝐸 ∈ Cat ) )
28 27 simprd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝐸 ∈ Cat )
29 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝐹 ∈ 𝑉 )
30 18 19 28 29 catpropd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( 𝐸 ∈ Cat ↔ 𝐹 ∈ Cat ) )
31 28 30 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝐹 ∈ Cat )
32 16 17 18 19 22 25 28 31 fucpropd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( 𝐶 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐹 ) )
33 32 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) ) = ( oppCat ‘ ( 𝐷 FuncCat 𝐹 ) ) )
34 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
35 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
36 21 simpld ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝐴 ∈ Cat )
37 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝐵 ∈ 𝑉 )
38 34 35 36 37 catpropd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( 𝐴 ∈ Cat ↔ 𝐵 ∈ Cat ) )
39 36 38 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝐵 ∈ Cat )
40 34 35 18 19 36 39 28 31 fucpropd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( 𝐴 FuncCat 𝐸 ) = ( 𝐵 FuncCat 𝐹 ) )
41 40 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( oppCat ‘ ( 𝐴 FuncCat 𝐸 ) ) = ( oppCat ‘ ( 𝐵 FuncCat 𝐹 ) ) )
42 33 41 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) ) UP ( oppCat ‘ ( 𝐴 FuncCat 𝐸 ) ) ) = ( ( oppCat ‘ ( 𝐷 FuncCat 𝐹 ) ) UP ( oppCat ‘ ( 𝐵 FuncCat 𝐹 ) ) ) )
43 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝑓 ∈ ( 𝐴 Func 𝐶 ) )
44 16 17 18 19 22 25 28 31 43 prcofpropd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( ⟨ 𝐶 , 𝐸 ⟩ −∘F 𝑓 ) = ( ⟨ 𝐷 , 𝐹 ⟩ −∘F 𝑓 ) )
45 44 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( oppFunc ‘ ( ⟨ 𝐶 , 𝐸 ⟩ −∘F 𝑓 ) ) = ( oppFunc ‘ ( ⟨ 𝐷 , 𝐹 ⟩ −∘F 𝑓 ) ) )
46 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝑥 = 𝑥 )
47 42 45 46 oveq123d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( ( oppFunc ‘ ( ⟨ 𝐶 , 𝐸 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) ) UP ( oppCat ‘ ( 𝐴 FuncCat 𝐸 ) ) ) 𝑥 ) = ( ( oppFunc ‘ ( ⟨ 𝐷 , 𝐹 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝐷 FuncCat 𝐹 ) ) UP ( oppCat ‘ ( 𝐵 FuncCat 𝐹 ) ) ) 𝑥 ) )
48 13 15 47 mpoeq123dva ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) , 𝑥 ∈ ( 𝐴 Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝐶 , 𝐸 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) ) UP ( oppCat ‘ ( 𝐴 FuncCat 𝐸 ) ) ) 𝑥 ) ) = ( 𝑓 ∈ ( 𝐵 Func 𝐷 ) , 𝑥 ∈ ( 𝐵 Func 𝐹 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝐷 , 𝐹 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝐷 FuncCat 𝐹 ) ) UP ( oppCat ‘ ( 𝐵 FuncCat 𝐹 ) ) ) 𝑥 ) ) )
49 eqid ⊢ ( 𝐶 FuncCat 𝐸 ) = ( 𝐶 FuncCat 𝐸 )
50 eqid ⊢ ( 𝐴 FuncCat 𝐸 ) = ( 𝐴 FuncCat 𝐸 )
51 eqid ⊢ ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) ) = ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) )
52 eqid ⊢ ( oppCat ‘ ( 𝐴 FuncCat 𝐸 ) ) = ( oppCat ‘ ( 𝐴 FuncCat 𝐸 ) )
53 49 50 7 9 11 51 52 ranfval ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐶 ⟩ Ran 𝐸 ) = ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) , 𝑥 ∈ ( 𝐴 Func 𝐸 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝐶 , 𝐸 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝐶 FuncCat 𝐸 ) ) UP ( oppCat ‘ ( 𝐴 FuncCat 𝐸 ) ) ) 𝑥 ) ) )
54 eqid ⊢ ( 𝐷 FuncCat 𝐹 ) = ( 𝐷 FuncCat 𝐹 )
55 eqid ⊢ ( 𝐵 FuncCat 𝐹 ) = ( 𝐵 FuncCat 𝐹 )
56 eqid ⊢ ( oppCat ‘ ( 𝐷 FuncCat 𝐹 ) ) = ( oppCat ‘ ( 𝐷 FuncCat 𝐹 ) )
57 eqid ⊢ ( oppCat ‘ ( 𝐵 FuncCat 𝐹 ) ) = ( oppCat ‘ ( 𝐵 FuncCat 𝐹 ) )
58 54 55 8 10 12 56 57 ranfval ⊢ ( 𝜑 → ( ⟨ 𝐵 , 𝐷 ⟩ Ran 𝐹 ) = ( 𝑓 ∈ ( 𝐵 Func 𝐷 ) , 𝑥 ∈ ( 𝐵 Func 𝐹 ) ↦ ( ( oppFunc ‘ ( ⟨ 𝐷 , 𝐹 ⟩ −∘F 𝑓 ) ) ( ( oppCat ‘ ( 𝐷 FuncCat 𝐹 ) ) UP ( oppCat ‘ ( 𝐵 FuncCat 𝐹 ) ) ) 𝑥 ) ) )
59 48 53 58 3eqtr4d ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐶 ⟩ Ran 𝐸 ) = ( ⟨ 𝐵 , 𝐷 ⟩ Ran 𝐹 ) )