Theorem homfeqbas

Description: Deduce equality of base sets from equality of Hom-sets. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypothesis	homfeqbas.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
Assertion	homfeqbas	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_D$$

Proof

Step	Hyp	Ref	Expression
1		homfeqbas.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
2	1	dmeqd	$$⊢\phi \to \mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(C\right)=\mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(D\right)$$
3		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
4		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
5	3 4	homffn	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
6	5	fndmi	$$⊢\mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Base}}_C\times {\mathrm{Base}}_C$$
7		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(D\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
8		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
9	7 8	homffn	$$⊢{\mathrm{Hom}}_{𝑓}\left(D\right)Fn\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)$$
10	9	fndmi	$$⊢\mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(D\right)={\mathrm{Base}}_D\times {\mathrm{Base}}_D$$
11	2 6 10	3eqtr3g	$$⊢\phi \to {\mathrm{Base}}_C\times {\mathrm{Base}}_C={\mathrm{Base}}_D\times {\mathrm{Base}}_D$$
12	11	dmeqd	$$⊢\phi \to \mathrm{dom}\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)=\mathrm{dom}\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)$$
13		dmxpid	$$⊢\mathrm{dom}\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)={\mathrm{Base}}_C$$
14		dmxpid	$$⊢\mathrm{dom}\left({\mathrm{Base}}_D\times {\mathrm{Base}}_D\right)={\mathrm{Base}}_D$$
15	12 13 14	3eqtr3g	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_D$$