Metamath Proof Explorer

Theorem prcofpropd

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

Ref Expression
Hypotheses prcofpropd.1 ⊢ φ → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B
prcofpropd.2 ⊢ φ → comp 𝑓 ⁡ A = comp 𝑓 ⁡ B
prcofpropd.3 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
prcofpropd.4 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
prcofpropd.a ⊢ φ → A ∈ V
prcofpropd.b ⊢ φ → B ∈ V
prcofpropd.c ⊢ φ → C ∈ V
prcofpropd.d ⊢ φ → D ∈ V
prcofpropd.f ⊢ φ → F ∈ W
Assertion prcofpropd Could not format assertion : No typesetting found for |- ( ph -> ( <. A , C >. -o.F F ) = ( <. B , D >. -o.F F ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 prcofpropd.1 ⊢ φ → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B
2 prcofpropd.2 ⊢ φ → comp 𝑓 ⁡ A = comp 𝑓 ⁡ B
3 prcofpropd.3 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
4 prcofpropd.4 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
5 prcofpropd.a ⊢ φ → A ∈ V
6 prcofpropd.b ⊢ φ → B ∈ V
7 prcofpropd.c ⊢ φ → C ∈ V
8 prcofpropd.d ⊢ φ → D ∈ V
9 prcofpropd.f ⊢ φ → F ∈ W
10 1 2 3 4 5 6 7 8 funcpropd ⊢ φ → A Func C = B Func D
11 10 mpteq1d ⊢ φ → k ∈ A Func C ⟼ k ∘ func F = k ∈ B Func D ⟼ k ∘ func F
12 10 adantr ⊢ φ ∧ k ∈ A Func C → A Func C = B Func D
13 1 adantr ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B
14 2 adantr ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → comp 𝑓 ⁡ A = comp 𝑓 ⁡ B
15 3 adantr ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
16 4 adantr ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
17 funcrcl ⊢ k ∈ A Func C → A ∈ Cat ∧ C ∈ Cat
18 17 ad2antrl ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → A ∈ Cat ∧ C ∈ Cat
19 18 simpld ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → A ∈ Cat
20 6 adantr ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → B ∈ V
21 13 14 19 20 catpropd ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → A ∈ Cat ↔ B ∈ Cat
22 19 21 mpbid ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → B ∈ Cat
23 18 simprd ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → C ∈ Cat
24 8 adantr ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → D ∈ V
25 15 16 23 24 catpropd ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → C ∈ Cat ↔ D ∈ Cat
26 23 25 mpbid ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → D ∈ Cat
27 13 14 15 16 19 22 23 26 natpropd ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → A Nat C = B Nat D
28 27 oveqd ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → k A Nat C l = k B Nat D l
29 28 mpteq1d ⊢ φ ∧ k ∈ A Func C ∧ l ∈ A Func C → a ∈ k A Nat C l ⟼ a ∘ 1 st ⁡ F = a ∈ k B Nat D l ⟼ a ∘ 1 st ⁡ F
30 10 12 29 mpoeq123dva ⊢ φ → k ∈ A Func C , l ∈ A Func C ⟼ a ∈ k A Nat C l ⟼ a ∘ 1 st ⁡ F = k ∈ B Func D , l ∈ B Func D ⟼ a ∈ k B Nat D l ⟼ a ∘ 1 st ⁡ F
31 11 30 opeq12d ⊢ φ → k ∈ A Func C ⟼ k ∘ func F k ∈ A Func C , l ∈ A Func C ⟼ a ∈ k A Nat C l ⟼ a ∘ 1 st ⁡ F = k ∈ B Func D ⟼ k ∘ func F k ∈ B Func D , l ∈ B Func D ⟼ a ∈ k B Nat D l ⟼ a ∘ 1 st ⁡ F
32 eqid ⊢ A Func C = A Func C
33 eqid ⊢ A Nat C = A Nat C
34 32 33 5 7 9 prcofvala Could not format ( ph -> ( <. A , C >. -o.F F ) = <. ( k e. ( A Func C ) |-> ( k o.func F ) ) , ( k e. ( A Func C ) , l e. ( A Func C ) |-> ( a e. ( k ( A Nat C ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) : No typesetting found for |- ( ph -> ( <. A , C >. -o.F F ) = <. ( k e. ( A Func C ) |-> ( k o.func F ) ) , ( k e. ( A Func C ) , l e. ( A Func C ) |-> ( a e. ( k ( A Nat C ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) with typecode |-
35 eqid ⊢ B Func D = B Func D
36 eqid ⊢ B Nat D = B Nat D
37 35 36 6 8 9 prcofvala Could not format ( ph -> ( <. B , D >. -o.F F ) = <. ( k e. ( B Func D ) |-> ( k o.func F ) ) , ( k e. ( B Func D ) , l e. ( B Func D ) |-> ( a e. ( k ( B Nat D ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) : No typesetting found for |- ( ph -> ( <. B , D >. -o.F F ) = <. ( k e. ( B Func D ) |-> ( k o.func F ) ) , ( k e. ( B Func D ) , l e. ( B Func D ) |-> ( a e. ( k ( B Nat D ) l ) |-> ( a o. ( 1st ` F ) ) ) ) >. ) with typecode |-
38 31 34 37 3eqtr4d Could not format ( ph -> ( <. A , C >. -o.F F ) = ( <. B , D >. -o.F F ) ) : No typesetting found for |- ( ph -> ( <. A , C >. -o.F F ) = ( <. B , D >. -o.F F ) ) with typecode |-