# 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}=\mathrm{Hom}\left({C}\right)$
homfeq.j ${⊢}{J}=\mathrm{Hom}\left({D}\right)$
homfeq.1 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{C}}$
homfeq.2 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{D}}$
Assertion homfeq ${⊢}{\phi }\to \left({\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{H}{y}={x}{J}{y}\right)$

### Proof

Step Hyp Ref Expression
1 homfeq.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
2 homfeq.j ${⊢}{J}=\mathrm{Hom}\left({D}\right)$
3 homfeq.1 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{C}}$
4 homfeq.2 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{D}}$
5 eqidd ${⊢}{\phi }\to {x}{H}{y}={x}{H}{y}$
6 3 3 5 mpoeq123dv ${⊢}{\phi }\to \left({x}\in {B},{y}\in {B}⟼{x}{H}{y}\right)=\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼{x}{H}{y}\right)$
7 eqid ${⊢}{\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({C}\right)$
8 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
9 7 8 1 homffval ${⊢}{\mathrm{Hom}}_{𝑓}\left({C}\right)=\left({x}\in {\mathrm{Base}}_{{C}},{y}\in {\mathrm{Base}}_{{C}}⟼{x}{H}{y}\right)$
10 6 9 syl6reqr ${⊢}{\phi }\to {\mathrm{Hom}}_{𝑓}\left({C}\right)=\left({x}\in {B},{y}\in {B}⟼{x}{H}{y}\right)$
11 eqidd ${⊢}{\phi }\to {x}{J}{y}={x}{J}{y}$
12 4 4 11 mpoeq123dv ${⊢}{\phi }\to \left({x}\in {B},{y}\in {B}⟼{x}{J}{y}\right)=\left({x}\in {\mathrm{Base}}_{{D}},{y}\in {\mathrm{Base}}_{{D}}⟼{x}{J}{y}\right)$
13 eqid ${⊢}{\mathrm{Hom}}_{𝑓}\left({D}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)$
14 eqid ${⊢}{\mathrm{Base}}_{{D}}={\mathrm{Base}}_{{D}}$
15 13 14 2 homffval ${⊢}{\mathrm{Hom}}_{𝑓}\left({D}\right)=\left({x}\in {\mathrm{Base}}_{{D}},{y}\in {\mathrm{Base}}_{{D}}⟼{x}{J}{y}\right)$
16 12 15 syl6reqr ${⊢}{\phi }\to {\mathrm{Hom}}_{𝑓}\left({D}\right)=\left({x}\in {B},{y}\in {B}⟼{x}{J}{y}\right)$
17 10 16 eqeq12d ${⊢}{\phi }\to \left({\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)↔\left({x}\in {B},{y}\in {B}⟼{x}{H}{y}\right)=\left({x}\in {B},{y}\in {B}⟼{x}{J}{y}\right)\right)$
18 ovex ${⊢}{x}{H}{y}\in \mathrm{V}$
19 18 rgen2w ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \mathrm{V}$
20 mpo2eqb ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{H}{y}\in \mathrm{V}\to \left(\left({x}\in {B},{y}\in {B}⟼{x}{H}{y}\right)=\left({x}\in {B},{y}\in {B}⟼{x}{J}{y}\right)↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{H}{y}={x}{J}{y}\right)$
21 19 20 ax-mp ${⊢}\left({x}\in {B},{y}\in {B}⟼{x}{H}{y}\right)=\left({x}\in {B},{y}\in {B}⟼{x}{J}{y}\right)↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{H}{y}={x}{J}{y}$
22 17 21 syl6bb ${⊢}{\phi }\to \left({\mathrm{Hom}}_{𝑓}\left({C}\right)={\mathrm{Hom}}_{𝑓}\left({D}\right)↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{H}{y}={x}{J}{y}\right)$