This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem comfeqd

Description: Condition for two categories with the same hom-sets to have the same composition. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses comfeqd.1 ⊢ φ → comp ⁡ C = comp ⁡ D
comfeqd.2 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
Assertion comfeqd ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D

Proof

Step Hyp Ref Expression
1 comfeqd.1 ⊢ φ → comp ⁡ C = comp ⁡ D
2 comfeqd.2 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
3 1 oveqd ⊢ φ → x y comp ⁡ C z = x y comp ⁡ D z
4 3 oveqd ⊢ φ → g x y comp ⁡ C z f = g x y comp ⁡ D z f
5 4 ralrimivw ⊢ φ → ∀ g ∈ y Hom ⁡ C z g x y comp ⁡ C z f = g x y comp ⁡ D z f
6 5 ralrimivw ⊢ φ → ∀ f ∈ x Hom ⁡ C y ∀ g ∈ y Hom ⁡ C z g x y comp ⁡ C z f = g x y comp ⁡ D z f
7 6 ralrimivw ⊢ φ → ∀ z ∈ Base C ∀ f ∈ x Hom ⁡ C y ∀ g ∈ y Hom ⁡ C z g x y comp ⁡ C z f = g x y comp ⁡ D z f
8 7 ralrimivw ⊢ φ → ∀ y ∈ Base C ∀ z ∈ Base C ∀ f ∈ x Hom ⁡ C y ∀ g ∈ y Hom ⁡ C z g x y comp ⁡ C z f = g x y comp ⁡ D z f
9 8 ralrimivw ⊢ φ → ∀ x ∈ Base C ∀ y ∈ Base C ∀ z ∈ Base C ∀ f ∈ x Hom ⁡ C y ∀ g ∈ y Hom ⁡ C z g x y comp ⁡ C z f = g x y comp ⁡ D z f
10 eqid ⊢ comp ⁡ C = comp ⁡ C
11 eqid ⊢ comp ⁡ D = comp ⁡ D
12 eqid ⊢ Hom ⁡ C = Hom ⁡ C
13 eqidd ⊢ φ → Base C = Base C
14 2 homfeqbas ⊢ φ → Base C = Base D
15 10 11 12 13 14 2 comfeq ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D ↔ ∀ x ∈ Base C ∀ y ∈ Base C ∀ z ∈ Base C ∀ f ∈ x Hom ⁡ C y ∀ g ∈ y Hom ⁡ C z g x y comp ⁡ C z f = g x y comp ⁡ D z f
16 9 15 mpbird ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D