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 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
Assertion homfeqbas 
|- ( ph -> ( Base ` C ) = ( Base ` D ) )

Proof

Step Hyp Ref Expression
1 homfeqbas.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
2 1 dmeqd 
 |-  ( ph -> dom ( Homf ` C ) = dom ( Homf ` D ) )
3 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 3 4 homffn 
 |-  ( Homf ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) )
6 5 fndmi 
 |-  dom ( Homf ` C ) = ( ( Base ` C ) X. ( Base ` C ) )
7 eqid 
 |-  ( Homf ` D ) = ( Homf ` D )
8 eqid 
 |-  ( Base ` D ) = ( Base ` D )
9 7 8 homffn 
 |-  ( Homf ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) )
10 9 fndmi 
 |-  dom ( Homf ` D ) = ( ( Base ` D ) X. ( Base ` D ) )
11 2 6 10 3eqtr3g 
 |-  ( ph -> ( ( Base ` C ) X. ( Base ` C ) ) = ( ( Base ` D ) X. ( Base ` D ) ) )
12 11 dmeqd 
 |-  ( ph -> dom ( ( Base ` C ) X. ( Base ` C ) ) = dom ( ( Base ` D ) X. ( Base ` D ) ) )
13 dmxpid 
 |-  dom ( ( Base ` C ) X. ( Base ` C ) ) = ( Base ` C )
14 dmxpid 
 |-  dom ( ( Base ` D ) X. ( Base ` D ) ) = ( Base ` D )
15 12 13 14 3eqtr3g 
 |-  ( ph -> ( Base ` C ) = ( Base ` D ) )