Metamath Proof Explorer

Theorem funchomf

Description: Source categories of a functor have the same set of objects and morphisms. (Contributed by Zhi Wang, 10-Nov-2025)

Ref Expression
Hypotheses funchomf.1 
|- ( ph -> F ( A Func C ) G )
funchomf.2 
|- ( ph -> F ( B Func D ) G )
Assertion funchomf 
|- ( ph -> ( Homf ` A ) = ( Homf ` B ) )

Proof

Step Hyp Ref Expression
1 funchomf.1 
 |-  ( ph -> F ( A Func C ) G )
2 funchomf.2 
 |-  ( ph -> F ( B Func D ) G )
3 eqid 
 |-  ( Base ` A ) = ( Base ` A )
4 eqid 
 |-  ( Hom ` A ) = ( Hom ` A )
5 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
6 1 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> F ( A Func C ) G )
7 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> x e. ( Base ` A ) )
8 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> y e. ( Base ` A ) )
9 3 4 5 6 7 8 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> ( x G y ) : ( x ( Hom ` A ) y ) --> ( ( F ` x ) ( Hom ` C ) ( F ` y ) ) )
10 9 ffnd 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> ( x G y ) Fn ( x ( Hom ` A ) y ) )
11 eqid 
 |-  ( Base ` B ) = ( Base ` B )
12 eqid 
 |-  ( Hom ` B ) = ( Hom ` B )
13 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
14 2 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> F ( B Func D ) G )
15 eqid 
 |-  ( Base ` C ) = ( Base ` C )
16 3 15 1 funcf1 
 |-  ( ph -> F : ( Base ` A ) --> ( Base ` C ) )
17 16 ffnd 
 |-  ( ph -> F Fn ( Base ` A ) )
18 eqid 
 |-  ( Base ` D ) = ( Base ` D )
19 11 18 2 funcf1 
 |-  ( ph -> F : ( Base ` B ) --> ( Base ` D ) )
20 19 ffnd 
 |-  ( ph -> F Fn ( Base ` B ) )
21 fndmu 
 |-  ( ( F Fn ( Base ` A ) /\ F Fn ( Base ` B ) ) -> ( Base ` A ) = ( Base ` B ) )
22 17 20 21 syl2anc 
 |-  ( ph -> ( Base ` A ) = ( Base ` B ) )
23 22 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> ( Base ` A ) = ( Base ` B ) )
24 7 23 eleqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> x e. ( Base ` B ) )
25 8 23 eleqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> y e. ( Base ` B ) )
26 11 12 13 14 24 25 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> ( x G y ) : ( x ( Hom ` B ) y ) --> ( ( F ` x ) ( Hom ` D ) ( F ` y ) ) )
27 26 ffnd 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> ( x G y ) Fn ( x ( Hom ` B ) y ) )
28 fndmu 
 |-  ( ( ( x G y ) Fn ( x ( Hom ` A ) y ) /\ ( x G y ) Fn ( x ( Hom ` B ) y ) ) -> ( x ( Hom ` A ) y ) = ( x ( Hom ` B ) y ) )
29 10 27 28 syl2anc 
 |-  ( ( ph /\ ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) ) -> ( x ( Hom ` A ) y ) = ( x ( Hom ` B ) y ) )
30 29 ralrimivva 
 |-  ( ph -> A. x e. ( Base ` A ) A. y e. ( Base ` A ) ( x ( Hom ` A ) y ) = ( x ( Hom ` B ) y ) )
31 eqidd 
 |-  ( ph -> ( Base ` A ) = ( Base ` A ) )
32 4 12 31 22 homfeq 
 |-  ( ph -> ( ( Homf ` A ) = ( Homf ` B ) <-> A. x e. ( Base ` A ) A. y e. ( Base ` A ) ( x ( Hom ` A ) y ) = ( x ( Hom ` B ) y ) ) )
33 30 32 mpbird 
 |-  ( ph -> ( Homf ` A ) = ( Homf ` B ) )