homfeqbas

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

		Ref	Expression
	Hypothesis	homfeqbas.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
	Assertion	homfeqbas	$⊢ φ \to {Base}_{C} = {Base}_{D}$

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

Metamath Proof Explorer