Metamath Proof Explorer


Theorem homfeq

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

Ref Expression
Hypotheses homfeq.h H = Hom C
homfeq.j J = Hom D
homfeq.1 φ B = Base C
homfeq.2 φ B = Base D
Assertion homfeq φ Hom 𝑓 C = Hom 𝑓 D x B y B x H y = x J y

Proof

Step Hyp Ref Expression
1 homfeq.h H = Hom C
2 homfeq.j J = Hom D
3 homfeq.1 φ B = Base C
4 homfeq.2 φ B = Base D
5 eqid Hom 𝑓 C = Hom 𝑓 C
6 eqid Base C = Base C
7 5 6 1 homffval Hom 𝑓 C = x Base C , y Base C x H y
8 eqidd φ x H y = x H y
9 3 3 8 mpoeq123dv φ x B , y B x H y = x Base C , y Base C x H y
10 7 9 eqtr4id φ Hom 𝑓 C = x B , y B x H y
11 eqid Hom 𝑓 D = Hom 𝑓 D
12 eqid Base D = Base D
13 11 12 2 homffval Hom 𝑓 D = x Base D , y Base D x J y
14 eqidd φ x J y = x J y
15 4 4 14 mpoeq123dv φ x B , y B x J y = x Base D , y Base D x J y
16 13 15 eqtr4id φ Hom 𝑓 D = x B , y B x J y
17 10 16 eqeq12d φ Hom 𝑓 C = Hom 𝑓 D x B , y B x H y = x B , y B x J y
18 ovex x H y V
19 18 rgen2w x B y B x H y V
20 mpo2eqb x B y B x H y V x B , y B x H y = x B , y B x J y x B y B x H y = x J y
21 19 20 ax-mp x B , y B x H y = x B , y B x J y x B y B x H y = x J y
22 17 21 bitrdi φ Hom 𝑓 C = Hom 𝑓 D x B y B x H y = x J y