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 ⊢ φ → F A Func C G
funchomf.2 ⊢ φ → F B Func D G
Assertion funchomf ⊢ φ → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B

Proof

Step Hyp Ref Expression
1 funchomf.1 ⊢ φ → F A Func C G
2 funchomf.2 ⊢ φ → 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 ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A → F A Func C G
7 simprl ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A → x ∈ Base A
8 simprr ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A → y ∈ Base A
9 3 4 5 6 7 8 funcf2 ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A → x G y : x Hom ⁡ A y ⟶ F ⁡ x Hom ⁡ C F ⁡ y
10 9 ffnd ⊢ φ ∧ x ∈ Base A ∧ y ∈ 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 ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A → F B Func D G
15 eqid ⊢ Base C = Base C
16 3 15 1 funcf1 ⊢ φ → F : Base A ⟶ Base C
17 16 ffnd ⊢ φ → F Fn Base A
18 eqid ⊢ Base D = Base D
19 11 18 2 funcf1 ⊢ φ → F : Base B ⟶ Base D
20 19 ffnd ⊢ φ → F Fn Base B
21 fndmu ⊢ F Fn Base A ∧ F Fn Base B → Base A = Base B
22 17 20 21 syl2anc ⊢ φ → Base A = Base B
23 22 adantr ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A → Base A = Base B
24 7 23 eleqtrd ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A → x ∈ Base B
25 8 23 eleqtrd ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A → y ∈ Base B
26 11 12 13 14 24 25 funcf2 ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A → x G y : x Hom ⁡ B y ⟶ F ⁡ x Hom ⁡ D F ⁡ y
27 26 ffnd ⊢ φ ∧ x ∈ Base A ∧ y ∈ 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 ⊢ φ ∧ x ∈ Base A ∧ y ∈ Base A → x Hom ⁡ A y = x Hom ⁡ B y
30 29 ralrimivva ⊢ φ → ∀ x ∈ Base A ∀ y ∈ Base A x Hom ⁡ A y = x Hom ⁡ B y
31 eqidd ⊢ φ → Base A = Base A
32 4 12 31 22 homfeq ⊢ φ → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B ↔ ∀ x ∈ Base A ∀ y ∈ Base A x Hom ⁡ A y = x Hom ⁡ B y
33 30 32 mpbird ⊢ φ → Hom 𝑓 ⁡ A = Hom 𝑓 ⁡ B