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)\leftrightarrow \forall x\in B\forall y\in BxHy=xJy\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		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
6		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
7	5 6 1	homffval	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼xHy\right)$$
8		eqidd	$$⊢\phi \to xHy=xHy$$
9	3 3 8	mpoeq123dv	$$⊢\phi \to \left(x\in B,y\in B⟼xHy\right)=\left(x\in {\mathrm{Base}}_C,y\in {\mathrm{Base}}_C⟼xHy\right)$$
10	7 9	eqtr4id	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)=\left(x\in B,y\in B⟼xHy\right)$$
11		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(D\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
12		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
13	11 12 2	homffval	$$⊢{\mathrm{Hom}}_{𝑓}\left(D\right)=\left(x\in {\mathrm{Base}}_D,y\in {\mathrm{Base}}_D⟼xJy\right)$$
14		eqidd	$$⊢\phi \to xJy=xJy$$
15	4 4 14	mpoeq123dv	$$⊢\phi \to \left(x\in B,y\in B⟼xJy\right)=\left(x\in {\mathrm{Base}}_D,y\in {\mathrm{Base}}_D⟼xJy\right)$$
16	13 15	eqtr4id	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(D\right)=\left(x\in B,y\in B⟼xJy\right)$$
17	10 16	eqeq12d	$$⊢\phi \to \left({\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)\leftrightarrow \left(x\in B,y\in B⟼xHy\right)=\left(x\in B,y\in B⟼xJy\right)\right)$$
18		ovex	$$⊢xHy\in \mathrm{V}$$
19	18	rgen2w	$$⊢\forall x\in B\forall y\in BxHy\in \mathrm{V}$$
20		mpo2eqb	$$⊢\forall x\in B\forall y\in BxHy\in \mathrm{V}\to \left(\left(x\in B,y\in B⟼xHy\right)=\left(x\in B,y\in B⟼xJy\right)\leftrightarrow \forall x\in B\forall y\in BxHy=xJy\right)$$
21	19 20	ax-mp	$$⊢\left(x\in B,y\in B⟼xHy\right)=\left(x\in B,y\in B⟼xJy\right)\leftrightarrow \forall x\in B\forall y\in BxHy=xJy$$
22	17 21	bitrdi	$$⊢\phi \to \left({\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)\leftrightarrow \forall x\in B\forall y\in BxHy=xJy\right)$$