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 ⊢ ( 𝜑 → 𝐹 ( 𝐴 Func 𝐶 ) 𝐺 )
funchomf.2 ⊢ ( 𝜑 → 𝐹 ( 𝐵 Func 𝐷 ) 𝐺 )
Assertion funchomf ( 𝜑 → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 funchomf.1 ⊢ ( 𝜑 → 𝐹 ( 𝐴 Func 𝐶 ) 𝐺 )
2 funchomf.2 ⊢ ( 𝜑 → 𝐹 ( 𝐵 Func 𝐷 ) 𝐺 )
3 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
4 eqid ⊢ ( Hom ‘ 𝐴 ) = ( Hom ‘ 𝐴 )
5 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
6 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → 𝐹 ( 𝐴 Func 𝐶 ) 𝐺 )
7 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
8 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
9 3 4 5 6 7 8 funcf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝐹 ‘ 𝑦 ) ) )
10 9 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑥 𝐺 𝑦 ) Fn ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) )
11 eqid ⊢ ( Base ‘ 𝐵 ) = ( Base ‘ 𝐵 )
12 eqid ⊢ ( Hom ‘ 𝐵 ) = ( Hom ‘ 𝐵 )
13 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
14 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → 𝐹 ( 𝐵 Func 𝐷 ) 𝐺 )
15 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
16 3 15 1 funcf1 ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) )
17 16 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( Base ‘ 𝐴 ) )
18 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
19 11 18 2 funcf1 ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐵 ) ⟶ ( Base ‘ 𝐷 ) )
20 19 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( Base ‘ 𝐵 ) )
21 fndmu ⊢ ( ( 𝐹 Fn ( Base ‘ 𝐴 ) ∧ 𝐹 Fn ( Base ‘ 𝐵 ) ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
22 17 20 21 syl2anc ⊢ ( 𝜑 → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
24 7 23 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐵 ) )
25 8 23 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐵 ) )
26 11 12 13 14 24 25 funcf2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) )
27 26 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑥 𝐺 𝑦 ) Fn ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) )
28 fndmu ⊢ ( ( ( 𝑥 𝐺 𝑦 ) Fn ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ∧ ( 𝑥 𝐺 𝑦 ) Fn ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ) → ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) )
29 10 27 28 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ) → ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) )
30 29 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) )
31 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 ) )
32 4 12 31 22 homfeq ⊢ ( 𝜑 → ( ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ) )
33 30 32 mpbird ⊢ ( 𝜑 → ( Homf ‘ 𝐴 ) = ( Homf ‘ 𝐵 ) )