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	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
Assertion	homfeqbas	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		homfeqbas.1	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
2	1	dmeqd	⊢ ( 𝜑 → dom ( Homf ‘ 𝐶 ) = dom ( Homf ‘ 𝐷 ) )
3		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
4		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5	3 4	homffn	⊢ ( Homf ‘ 𝐶 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
6	5	fndmi	⊢ dom ( Homf ‘ 𝐶 ) = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) )
7		eqid	⊢ ( Homf ‘ 𝐷 ) = ( Homf ‘ 𝐷 )
8		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
9	7 8	homffn	⊢ ( Homf ‘ 𝐷 ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) )
10	9	fndmi	⊢ dom ( Homf ‘ 𝐷 ) = ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) )
11	2 6 10	3eqtr3g	⊢ ( 𝜑 → ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) = ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
12	11	dmeqd	⊢ ( 𝜑 → dom ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) = dom ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
13		dmxpid	⊢ dom ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) = ( Base ‘ 𝐶 )
14		dmxpid	⊢ dom ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝐷 )
15	12 13 14	3eqtr3g	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )