# Metamath Proof Explorer

## Theorem comfeq

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 comfeq.1
comfeq.2
comfeq.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
comfeq.3 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{C}}$
comfeq.4 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{D}}$
comfeq.5 ${⊢}{\phi }\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
Assertion comfeq

### Proof

Step Hyp Ref Expression
1 comfeq.1
2 comfeq.2
3 comfeq.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
4 comfeq.3 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{C}}$
5 comfeq.4 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{D}}$
6 comfeq.5 ${⊢}{\phi }\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
7 4 sqxpeqd ${⊢}{\phi }\to {B}×{B}={\mathrm{Base}}_{{C}}×{\mathrm{Base}}_{{C}}$
8 eqidd
9 7 4 8 mpoeq123dv
10 eqid ${⊢}{\mathrm{comp}}_{𝑓}\left({C}\right)={\mathrm{comp}}_{𝑓}\left({C}\right)$
11 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
12 10 11 3 1 comfffval
13 9 12 syl6eqr
14 eqid ${⊢}\mathrm{Hom}\left({D}\right)=\mathrm{Hom}\left({D}\right)$
15 6 3ad2ant1 ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to {\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
16 xp2nd ${⊢}{u}\in \left({B}×{B}\right)\to {2}^{nd}\left({u}\right)\in {B}$
17 16 3ad2ant2 ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to {2}^{nd}\left({u}\right)\in {B}$
18 4 3ad2ant1 ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to {B}={\mathrm{Base}}_{{C}}$
19 17 18 eleqtrd ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to {2}^{nd}\left({u}\right)\in {\mathrm{Base}}_{{C}}$
20 simp3 ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to {z}\in {B}$
21 20 18 eleqtrd ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to {z}\in {\mathrm{Base}}_{{C}}$
22 11 3 14 15 19 21 homfeqval ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to {2}^{nd}\left({u}\right){H}{z}={2}^{nd}\left({u}\right)\mathrm{Hom}\left({D}\right){z}$
23 xp1st ${⊢}{u}\in \left({B}×{B}\right)\to {1}^{st}\left({u}\right)\in {B}$
24 23 3ad2ant2 ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to {1}^{st}\left({u}\right)\in {B}$
25 24 18 eleqtrd ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to {1}^{st}\left({u}\right)\in {\mathrm{Base}}_{{C}}$
26 11 3 14 15 25 19 homfeqval ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to {1}^{st}\left({u}\right){H}{2}^{nd}\left({u}\right)={1}^{st}\left({u}\right)\mathrm{Hom}\left({D}\right){2}^{nd}\left({u}\right)$
27 df-ov ${⊢}{1}^{st}\left({u}\right){H}{2}^{nd}\left({u}\right)={H}\left(⟨{1}^{st}\left({u}\right),{2}^{nd}\left({u}\right)⟩\right)$
28 df-ov ${⊢}{1}^{st}\left({u}\right)\mathrm{Hom}\left({D}\right){2}^{nd}\left({u}\right)=\mathrm{Hom}\left({D}\right)\left(⟨{1}^{st}\left({u}\right),{2}^{nd}\left({u}\right)⟩\right)$
29 26 27 28 3eqtr3g ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to {H}\left(⟨{1}^{st}\left({u}\right),{2}^{nd}\left({u}\right)⟩\right)=\mathrm{Hom}\left({D}\right)\left(⟨{1}^{st}\left({u}\right),{2}^{nd}\left({u}\right)⟩\right)$
30 1st2nd2 ${⊢}{u}\in \left({B}×{B}\right)\to {u}=⟨{1}^{st}\left({u}\right),{2}^{nd}\left({u}\right)⟩$
31 30 3ad2ant2 ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to {u}=⟨{1}^{st}\left({u}\right),{2}^{nd}\left({u}\right)⟩$
32 31 fveq2d ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to {H}\left({u}\right)={H}\left(⟨{1}^{st}\left({u}\right),{2}^{nd}\left({u}\right)⟩\right)$
33 31 fveq2d ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to \mathrm{Hom}\left({D}\right)\left({u}\right)=\mathrm{Hom}\left({D}\right)\left(⟨{1}^{st}\left({u}\right),{2}^{nd}\left({u}\right)⟩\right)$
34 29 32 33 3eqtr4d ${⊢}\left({\phi }\wedge {u}\in \left({B}×{B}\right)\wedge {z}\in {B}\right)\to {H}\left({u}\right)=\mathrm{Hom}\left({D}\right)\left({u}\right)$
35 eqidd
36 22 34 35 mpoeq123dv
37 36 mpoeq3dva
38 5 sqxpeqd ${⊢}{\phi }\to {B}×{B}={\mathrm{Base}}_{{D}}×{\mathrm{Base}}_{{D}}$
39 eqidd
40 38 5 39 mpoeq123dv
41 37 40 eqtrd
42 eqid ${⊢}{\mathrm{comp}}_{𝑓}\left({D}\right)={\mathrm{comp}}_{𝑓}\left({D}\right)$
43 eqid ${⊢}{\mathrm{Base}}_{{D}}={\mathrm{Base}}_{{D}}$
44 42 43 14 2 comfffval
45 41 44 syl6eqr
46 13 45 eqeq12d
47 ovex ${⊢}{2}^{nd}\left({u}\right){H}{z}\in \mathrm{V}$
48 fvex ${⊢}{H}\left({u}\right)\in \mathrm{V}$
49 47 48 mpoex
50 49 rgen2w
51 mpo2eqb
52 50 51 ax-mp
53 vex ${⊢}{x}\in \mathrm{V}$
54 vex ${⊢}{y}\in \mathrm{V}$
55 53 54 op2ndd ${⊢}{u}=⟨{x},{y}⟩\to {2}^{nd}\left({u}\right)={y}$
56 55 oveq1d ${⊢}{u}=⟨{x},{y}⟩\to {2}^{nd}\left({u}\right){H}{z}={y}{H}{z}$
57 fveq2 ${⊢}{u}=⟨{x},{y}⟩\to {H}\left({u}\right)={H}\left(⟨{x},{y}⟩\right)$
58 df-ov ${⊢}{x}{H}{y}={H}\left(⟨{x},{y}⟩\right)$
59 57 58 syl6eqr ${⊢}{u}=⟨{x},{y}⟩\to {H}\left({u}\right)={x}{H}{y}$
60 oveq1
61 60 oveqd
62 oveq1
63 62 oveqd
64 61 63 eqeq12d
65 59 64 raleqbidv
66 56 65 raleqbidv
67 ovex
68 67 rgen2w
69 mpo2eqb
70 68 69 ax-mp
71 ralcom
72 66 70 71 3bitr4g
73 72 ralbidv
74 73 ralxp
75 52 74 bitri
76 46 75 bitr3di