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 ⊢ ( 𝜑 → 𝐶 ∈ Cat )
functhincfun.e ⊢ ( 𝜑 → 𝐷 ∈ ThinCat )
Assertion functhincfun ( 𝜑 → Fun ( 𝐶 Func 𝐷 ) )

Proof

Step Hyp Ref Expression
1 functhincfun.d ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 functhincfun.e ⊢ ( 𝜑 → 𝐷 ∈ ThinCat )
3 relfunc ⊢ Rel ( 𝐶 Func 𝐷 )
4 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) → 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 )
5 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
7 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
8 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
9 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) → 𝐶 ∈ Cat )
10 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) → 𝐷 ∈ ThinCat )
11 5 6 4 funcf1 ⊢ ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) → 𝑓 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
12 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) ) )
13 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 )
14 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
15 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
16 5 7 8 13 14 15 funcf2 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 𝑔 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) )
17 16 f002 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) = ∅ → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ∅ ) )
18 17 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) = ∅ → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ∅ ) )
19 5 6 7 8 9 10 11 12 18 functhinc ⊢ ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) → ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ↔ 𝑔 = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
20 4 19 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) → 𝑔 = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) ) ) )
21 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) → 𝑓 ( 𝐶 Func 𝐷 ) ℎ )
22 5 6 7 8 9 10 11 12 18 functhinc ⊢ ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) → ( 𝑓 ( 𝐶 Func 𝐷 ) ℎ ↔ ℎ = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
23 21 22 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) × ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑓 ‘ 𝑦 ) ) ) ) )
24 20 23 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) ) → 𝑔 = ℎ )
25 24 ex ⊢ ( 𝜑 → ( ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) → 𝑔 = ℎ ) )
26 25 alrimivv ⊢ ( 𝜑 → ∀ 𝑔 ∀ ℎ ( ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) → 𝑔 = ℎ ) )
27 26 alrimiv ⊢ ( 𝜑 → ∀ 𝑓 ∀ 𝑔 ∀ ℎ ( ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) → 𝑔 = ℎ ) )
28 dffun2 ⊢ ( Fun ( 𝐶 Func 𝐷 ) ↔ ( Rel ( 𝐶 Func 𝐷 ) ∧ ∀ 𝑓 ∀ 𝑔 ∀ ℎ ( ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) → 𝑔 = ℎ ) ) )
29 28 biimpri ⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ ∀ 𝑓 ∀ 𝑔 ∀ ℎ ( ( 𝑓 ( 𝐶 Func 𝐷 ) 𝑔 ∧ 𝑓 ( 𝐶 Func 𝐷 ) ℎ ) → 𝑔 = ℎ ) ) → Fun ( 𝐶 Func 𝐷 ) )
30 3 27 29 sylancr ⊢ ( 𝜑 → Fun ( 𝐶 Func 𝐷 ) )