Metamath Proof Explorer

Theorem lanpropd

Description: If the categories have the same set of objects, morphisms, and compositions, then they have the same left 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 lanpropd ( 𝜑 → ( ⟨ 𝐴 , 𝐶 ⟩ Lan 𝐸 ) = ( ⟨ 𝐵 , 𝐷 ⟩ Lan 𝐹 ) )

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 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )
34 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( compf ‘ 𝐴 ) = ( compf ‘ 𝐵 ) )
35 21 simpld ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝐴 ∈ Cat )
36 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝐵 ∈ 𝑉 )
37 33 34 35 36 catpropd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( 𝐴 ∈ Cat ↔ 𝐵 ∈ Cat ) )
38 35 37 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝐵 ∈ Cat )
39 33 34 18 19 35 38 28 31 fucpropd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( 𝐴 FuncCat 𝐸 ) = ( 𝐵 FuncCat 𝐹 ) )
40 32 39 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( ( 𝐶 FuncCat 𝐸 ) UP ( 𝐴 FuncCat 𝐸 ) ) = ( ( 𝐷 FuncCat 𝐹 ) UP ( 𝐵 FuncCat 𝐹 ) ) )
41 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝑓 ∈ ( 𝐴 Func 𝐶 ) )
42 16 17 18 19 22 25 28 31 41 prcofpropd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( ⟨ 𝐶 , 𝐸 ⟩ −∘F 𝑓 ) = ( ⟨ 𝐷 , 𝐹 ⟩ −∘F 𝑓 ) )
43 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → 𝑥 = 𝑥 )
44 40 42 43 oveq123d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑥 ∈ ( 𝐴 Func 𝐸 ) ) ) → ( ( ⟨ 𝐶 , 𝐸 ⟩ −∘F 𝑓 ) ( ( 𝐶 FuncCat 𝐸 ) UP ( 𝐴 FuncCat 𝐸 ) ) 𝑥 ) = ( ( ⟨ 𝐷 , 𝐹 ⟩ −∘F 𝑓 ) ( ( 𝐷 FuncCat 𝐹 ) UP ( 𝐵 FuncCat 𝐹 ) ) 𝑥 ) )
45 13 15 44 mpoeq123dva ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) , 𝑥 ∈ ( 𝐴 Func 𝐸 ) ↦ ( ( ⟨ 𝐶 , 𝐸 ⟩ −∘F 𝑓 ) ( ( 𝐶 FuncCat 𝐸 ) UP ( 𝐴 FuncCat 𝐸 ) ) 𝑥 ) ) = ( 𝑓 ∈ ( 𝐵 Func 𝐷 ) , 𝑥 ∈ ( 𝐵 Func 𝐹 ) ↦ ( ( ⟨ 𝐷 , 𝐹 ⟩ −∘F 𝑓 ) ( ( 𝐷 FuncCat 𝐹 ) UP ( 𝐵 FuncCat 𝐹 ) ) 𝑥 ) ) )
46 eqid ⊢ ( 𝐶 FuncCat 𝐸 ) = ( 𝐶 FuncCat 𝐸 )
47 eqid ⊢ ( 𝐴 FuncCat 𝐸 ) = ( 𝐴 FuncCat 𝐸 )
48 46 47 7 9 11 lanfval ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐶 ⟩ Lan 𝐸 ) = ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) , 𝑥 ∈ ( 𝐴 Func 𝐸 ) ↦ ( ( ⟨ 𝐶 , 𝐸 ⟩ −∘F 𝑓 ) ( ( 𝐶 FuncCat 𝐸 ) UP ( 𝐴 FuncCat 𝐸 ) ) 𝑥 ) ) )
49 eqid ⊢ ( 𝐷 FuncCat 𝐹 ) = ( 𝐷 FuncCat 𝐹 )
50 eqid ⊢ ( 𝐵 FuncCat 𝐹 ) = ( 𝐵 FuncCat 𝐹 )
51 49 50 8 10 12 lanfval ⊢ ( 𝜑 → ( ⟨ 𝐵 , 𝐷 ⟩ Lan 𝐹 ) = ( 𝑓 ∈ ( 𝐵 Func 𝐷 ) , 𝑥 ∈ ( 𝐵 Func 𝐹 ) ↦ ( ( ⟨ 𝐷 , 𝐹 ⟩ −∘F 𝑓 ) ( ( 𝐷 FuncCat 𝐹 ) UP ( 𝐵 FuncCat 𝐹 ) ) 𝑥 ) ) )
52 45 48 51 3eqtr4d ⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐶 ⟩ Lan 𝐸 ) = ( ⟨ 𝐵 , 𝐷 ⟩ Lan 𝐹 ) )