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 eqidd φ x H y = x H y
6 3 3 5 mpoeq123dv φ x B , y B x H y = x Base C , y Base C x H y
7 eqid Hom 𝑓 C = Hom 𝑓 C
8 eqid Base C = Base C
9 7 8 1 homffval Hom 𝑓 C = x Base C , y Base C x H y
10 6 9 syl6reqr φ Hom 𝑓 C = x B , y B x H y
11 eqidd φ x J y = x J y
12 4 4 11 mpoeq123dv φ x B , y B x J y = x Base D , y Base D x J y
13 eqid Hom 𝑓 D = Hom 𝑓 D
14 eqid Base D = Base D
15 13 14 2 homffval Hom 𝑓 D = x Base D , y Base D x J y
16 12 15 syl6reqr φ 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 syl6bb φ Hom 𝑓 C = Hom 𝑓 D x B y B x H y = x J y