Metamath Proof Explorer

Theorem functhincfun

Description: A functor to a thin category is determined entirely by the object part. (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Hypotheses functhincfun.d ⊢ φ → C ∈ Cat
functhincfun.e ⊢ φ → D ∈ ThinCat
Assertion functhincfun ⊢ φ → Fun ⁡ C Func D

Proof

Step Hyp Ref Expression
1 functhincfun.d ⊢ φ → C ∈ Cat
2 functhincfun.e ⊢ φ → D ∈ ThinCat
3 relfunc ⊢ Rel ⁡ C Func D
4 simprl ⊢ φ ∧ f C Func D g ∧ f C Func D h → f C Func D g
5 eqid ⊢ Base C = Base C
6 eqid ⊢ Base D = Base D
7 eqid ⊢ Hom ⁡ C = Hom ⁡ C
8 eqid ⊢ Hom ⁡ D = Hom ⁡ D
9 1 adantr ⊢ φ ∧ f C Func D g ∧ f C Func D h → C ∈ Cat
10 2 adantr ⊢ φ ∧ f C Func D g ∧ f C Func D h → D ∈ ThinCat
11 5 6 4 funcf1 ⊢ φ ∧ f C Func D g ∧ f C Func D h → f : Base C ⟶ Base D
12 eqid ⊢ x ∈ Base C , y ∈ Base C ⟼ x Hom ⁡ C y × f ⁡ x Hom ⁡ D f ⁡ y = x ∈ Base C , y ∈ Base C ⟼ x Hom ⁡ C y × f ⁡ x Hom ⁡ D f ⁡ y
13 simplrl ⊢ φ ∧ f C Func D g ∧ f C Func D h ∧ x ∈ Base C ∧ y ∈ Base C → f C Func D g
14 simprl ⊢ φ ∧ f C Func D g ∧ f C Func D h ∧ x ∈ Base C ∧ y ∈ Base C → x ∈ Base C
15 simprr ⊢ φ ∧ f C Func D g ∧ f C Func D h ∧ x ∈ Base C ∧ y ∈ Base C → y ∈ Base C
16 5 7 8 13 14 15 funcf2 ⊢ φ ∧ f C Func D g ∧ f C Func D h ∧ x ∈ Base C ∧ y ∈ Base C → x g y : x Hom ⁡ C y ⟶ f ⁡ x Hom ⁡ D f ⁡ y
17 16 f002 ⊢ φ ∧ f C Func D g ∧ f C Func D h ∧ x ∈ Base C ∧ y ∈ Base C → f ⁡ x Hom ⁡ D f ⁡ y = ∅ → x Hom ⁡ C y = ∅
18 17 ralrimivva ⊢ φ ∧ f C Func D g ∧ f C Func D h → ∀ x ∈ Base C ∀ y ∈ Base C f ⁡ x Hom ⁡ D f ⁡ y = ∅ → x Hom ⁡ C y = ∅
19 5 6 7 8 9 10 11 12 18 functhinc ⊢ φ ∧ f C Func D g ∧ f C Func D h → f C Func D g ↔ g = x ∈ Base C , y ∈ Base C ⟼ x Hom ⁡ C y × f ⁡ x Hom ⁡ D f ⁡ y
20 4 19 mpbid ⊢ φ ∧ f C Func D g ∧ f C Func D h → g = x ∈ Base C , y ∈ Base C ⟼ x Hom ⁡ C y × f ⁡ x Hom ⁡ D f ⁡ y
21 simprr ⊢ φ ∧ f C Func D g ∧ f C Func D h → f C Func D h
22 5 6 7 8 9 10 11 12 18 functhinc ⊢ φ ∧ f C Func D g ∧ f C Func D h → f C Func D h ↔ h = x ∈ Base C , y ∈ Base C ⟼ x Hom ⁡ C y × f ⁡ x Hom ⁡ D f ⁡ y
23 21 22 mpbid ⊢ φ ∧ f C Func D g ∧ f C Func D h → h = x ∈ Base C , y ∈ Base C ⟼ x Hom ⁡ C y × f ⁡ x Hom ⁡ D f ⁡ y
24 20 23 eqtr4d ⊢ φ ∧ f C Func D g ∧ f C Func D h → g = h
25 24 ex ⊢ φ → f C Func D g ∧ f C Func D h → g = h
26 25 alrimivv ⊢ φ → ∀ g ∀ h f C Func D g ∧ f C Func D h → g = h
27 26 alrimiv ⊢ φ → ∀ f ∀ g ∀ h f C Func D g ∧ f C Func D h → g = h
28 dffun2 ⊢ Fun ⁡ C Func D ↔ Rel ⁡ C Func D ∧ ∀ f ∀ g ∀ h f C Func D g ∧ f C Func D h → g = h
29 28 biimpri ⊢ Rel ⁡ C Func D ∧ ∀ f ∀ g ∀ h f C Func D g ∧ f C Func D h → g = h → Fun ⁡ C Func D
30 3 27 29 sylancr ⊢ φ → Fun ⁡ C Func D