This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐷 ) )