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 ⊢ φ → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B
lanpropd.2 ⊢ φ → comp 𝑓 ⁡ A = comp 𝑓 ⁡ B
lanpropd.3 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
lanpropd.4 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
lanpropd.5 ⊢ φ → Hom 𝑓 ⁡ E = Hom 𝑓 ⁡ F
lanpropd.6 ⊢ φ → comp 𝑓 ⁡ E = comp 𝑓 ⁡ F
lanpropd.a ⊢ φ → A ∈ V
lanpropd.b ⊢ φ → B ∈ V
lanpropd.c ⊢ φ → C ∈ V
lanpropd.d ⊢ φ → D ∈ V
lanpropd.e ⊢ φ → E ∈ V
lanpropd.f ⊢ φ → F ∈ V
Assertion lanpropd Could not format assertion : No typesetting found for |- ( ph -> ( <. A , C >. Lan E ) = ( <. B , D >. Lan F ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 lanpropd.1 ⊢ φ → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B
2 lanpropd.2 ⊢ φ → comp 𝑓 ⁡ A = comp 𝑓 ⁡ B
3 lanpropd.3 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
4 lanpropd.4 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
5 lanpropd.5 ⊢ φ → Hom 𝑓 ⁡ E = Hom 𝑓 ⁡ F
6 lanpropd.6 ⊢ φ → comp 𝑓 ⁡ E = comp 𝑓 ⁡ F
7 lanpropd.a ⊢ φ → A ∈ V
8 lanpropd.b ⊢ φ → B ∈ V
9 lanpropd.c ⊢ φ → C ∈ V
10 lanpropd.d ⊢ φ → D ∈ V
11 lanpropd.e ⊢ φ → E ∈ V
12 lanpropd.f ⊢ φ → F ∈ V
13 1 2 3 4 7 8 9 10 funcpropd ⊢ φ → A Func C = B Func D
14 1 2 5 6 7 8 11 12 funcpropd ⊢ φ → A Func E = B Func F
15 14 adantr ⊢ φ ∧ f ∈ A Func C → A Func E = B Func F
16 3 adantr ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
17 4 adantr ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
18 5 adantr ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → Hom 𝑓 ⁡ E = Hom 𝑓 ⁡ F
19 6 adantr ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → comp 𝑓 ⁡ E = comp 𝑓 ⁡ F
20 funcrcl ⊢ f ∈ A Func C → A ∈ Cat ∧ C ∈ Cat
21 20 ad2antrl ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → A ∈ Cat ∧ C ∈ Cat
22 21 simprd ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → C ∈ Cat
23 10 adantr ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → D ∈ V
24 16 17 22 23 catpropd ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → C ∈ Cat ↔ D ∈ Cat
25 22 24 mpbid ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → D ∈ Cat
26 funcrcl ⊢ x ∈ A Func E → A ∈ Cat ∧ E ∈ Cat
27 26 ad2antll ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → A ∈ Cat ∧ E ∈ Cat
28 27 simprd ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → E ∈ Cat
29 12 adantr ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → F ∈ V
30 18 19 28 29 catpropd ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → E ∈ Cat ↔ F ∈ Cat
31 28 30 mpbid ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → F ∈ Cat
32 16 17 18 19 22 25 28 31 fucpropd ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → C FuncCat E = D FuncCat F
33 1 adantr ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B
34 2 adantr ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → comp 𝑓 ⁡ A = comp 𝑓 ⁡ B
35 21 simpld ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → A ∈ Cat
36 8 adantr ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → B ∈ V
37 33 34 35 36 catpropd ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → A ∈ Cat ↔ B ∈ Cat
38 35 37 mpbid ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → B ∈ Cat
39 33 34 18 19 35 38 28 31 fucpropd ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → A FuncCat E = B FuncCat F
40 32 39 oveq12d Could not format ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( ( C FuncCat E ) UP ( A FuncCat E ) ) = ( ( D FuncCat F ) UP ( B FuncCat F ) ) ) : No typesetting found for |- ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( ( C FuncCat E ) UP ( A FuncCat E ) ) = ( ( D FuncCat F ) UP ( B FuncCat F ) ) ) with typecode |-
41 simprl ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → f ∈ A Func C
42 16 17 18 19 22 25 28 31 41 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 |-
43 eqidd ⊢ φ ∧ f ∈ A Func C ∧ x ∈ A Func E → x = x
44 40 42 43 oveq123d Could not format ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( ( <. C , E >. -o.F f ) ( ( C FuncCat E ) UP ( A FuncCat E ) ) x ) = ( ( <. D , F >. -o.F f ) ( ( D FuncCat F ) UP ( B FuncCat F ) ) x ) ) : No typesetting found for |- ( ( ph /\ ( f e. ( A Func C ) /\ x e. ( A Func E ) ) ) -> ( ( <. C , E >. -o.F f ) ( ( C FuncCat E ) UP ( A FuncCat E ) ) x ) = ( ( <. D , F >. -o.F f ) ( ( D FuncCat F ) UP ( B FuncCat F ) ) x ) ) with typecode |-
45 13 15 44 mpoeq123dva Could not format ( ph -> ( f e. ( A Func C ) , x e. ( A Func E ) |-> ( ( <. C , E >. -o.F f ) ( ( C FuncCat E ) UP ( A FuncCat E ) ) x ) ) = ( f e. ( B Func D ) , x e. ( B Func F ) |-> ( ( <. D , F >. -o.F f ) ( ( D FuncCat F ) UP ( B FuncCat F ) ) x ) ) ) : No typesetting found for |- ( ph -> ( f e. ( A Func C ) , x e. ( A Func E ) |-> ( ( <. C , E >. -o.F f ) ( ( C FuncCat E ) UP ( A FuncCat E ) ) x ) ) = ( f e. ( B Func D ) , x e. ( B Func F ) |-> ( ( <. D , F >. -o.F f ) ( ( D FuncCat F ) UP ( B FuncCat F ) ) x ) ) ) with typecode |-
46 eqid ⊢ C FuncCat E = C FuncCat E
47 eqid ⊢ A FuncCat E = A FuncCat E
48 46 47 7 9 11 lanfval Could not format ( ph -> ( <. A , C >. Lan E ) = ( f e. ( A Func C ) , x e. ( A Func E ) |-> ( ( <. C , E >. -o.F f ) ( ( C FuncCat E ) UP ( A FuncCat E ) ) x ) ) ) : No typesetting found for |- ( ph -> ( <. A , C >. Lan E ) = ( f e. ( A Func C ) , x e. ( A Func E ) |-> ( ( <. C , E >. -o.F f ) ( ( C FuncCat E ) UP ( A FuncCat E ) ) x ) ) ) with typecode |-
49 eqid ⊢ D FuncCat F = D FuncCat F
50 eqid ⊢ B FuncCat F = B FuncCat F
51 49 50 8 10 12 lanfval Could not format ( ph -> ( <. B , D >. Lan F ) = ( f e. ( B Func D ) , x e. ( B Func F ) |-> ( ( <. D , F >. -o.F f ) ( ( D FuncCat F ) UP ( B FuncCat F ) ) x ) ) ) : No typesetting found for |- ( ph -> ( <. B , D >. Lan F ) = ( f e. ( B Func D ) , x e. ( B Func F ) |-> ( ( <. D , F >. -o.F f ) ( ( D FuncCat F ) UP ( B FuncCat F ) ) x ) ) ) with typecode |-
52 45 48 51 3eqtr4d Could not format ( ph -> ( <. A , C >. Lan E ) = ( <. B , D >. Lan F ) ) : No typesetting found for |- ( ph -> ( <. A , C >. Lan E ) = ( <. B , D >. Lan F ) ) with typecode |-