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 
|- ( ph -> C e. Cat )
functhincfun.e 
|- ( ph -> D e. ThinCat )
Assertion functhincfun 
|- ( ph -> Fun ( C Func D ) )

Proof

Step Hyp Ref Expression
1 functhincfun.d 
 |-  ( ph -> C e. Cat )
2 functhincfun.e 
 |-  ( ph -> D e. ThinCat )
3 relfunc 
 |-  Rel ( C Func D )
4 simprl 
 |-  ( ( ph /\ ( 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 
 |-  ( ( ph /\ ( f ( C Func D ) g /\ f ( C Func D ) h ) ) -> C e. Cat )
10 2 adantr 
 |-  ( ( ph /\ ( f ( C Func D ) g /\ f ( C Func D ) h ) ) -> D e. ThinCat )
11 5 6 4 funcf1 
 |-  ( ( ph /\ ( f ( C Func D ) g /\ f ( C Func D ) h ) ) -> f : ( Base ` C ) --> ( Base ` D ) )
12 eqid 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Hom ` C ) y ) X. ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) ) ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Hom ` C ) y ) X. ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) ) )
13 simplrl 
 |-  ( ( ( ph /\ ( f ( C Func D ) g /\ f ( C Func D ) h ) ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> f ( C Func D ) g )
14 simprl 
 |-  ( ( ( ph /\ ( f ( C Func D ) g /\ f ( C Func D ) h ) ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
15 simprr 
 |-  ( ( ( ph /\ ( f ( C Func D ) g /\ f ( C Func D ) h ) ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
16 5 7 8 13 14 15 funcf2 
 |-  ( ( ( ph /\ ( f ( C Func D ) g /\ f ( C Func D ) h ) ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x g y ) : ( x ( Hom ` C ) y ) --> ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) )
17 16 f002 
 |-  ( ( ( ph /\ ( f ( C Func D ) g /\ f ( C Func D ) h ) ) /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) = (/) -> ( x ( Hom ` C ) y ) = (/) ) )
18 17 ralrimivva 
 |-  ( ( ph /\ ( f ( C Func D ) g /\ f ( C Func D ) h ) ) -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) = (/) -> ( x ( Hom ` C ) y ) = (/) ) )
19 5 6 7 8 9 10 11 12 18 functhinc 
 |-  ( ( ph /\ ( f ( C Func D ) g /\ f ( C Func D ) h ) ) -> ( f ( C Func D ) g <-> g = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Hom ` C ) y ) X. ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) ) ) ) )
20 4 19 mpbid 
 |-  ( ( ph /\ ( f ( C Func D ) g /\ f ( C Func D ) h ) ) -> g = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Hom ` C ) y ) X. ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) ) ) )
21 simprr 
 |-  ( ( ph /\ ( 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 
 |-  ( ( ph /\ ( f ( C Func D ) g /\ f ( C Func D ) h ) ) -> ( f ( C Func D ) h <-> h = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Hom ` C ) y ) X. ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) ) ) ) )
23 21 22 mpbid 
 |-  ( ( ph /\ ( f ( C Func D ) g /\ f ( C Func D ) h ) ) -> h = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> ( ( x ( Hom ` C ) y ) X. ( ( f ` x ) ( Hom ` D ) ( f ` y ) ) ) ) )
24 20 23 eqtr4d 
 |-  ( ( ph /\ ( f ( C Func D ) g /\ f ( C Func D ) h ) ) -> g = h )
25 24 ex 
 |-  ( ph -> ( ( f ( C Func D ) g /\ f ( C Func D ) h ) -> g = h ) )
26 25 alrimivv 
 |-  ( ph -> A. g A. h ( ( f ( C Func D ) g /\ f ( C Func D ) h ) -> g = h ) )
27 26 alrimiv 
 |-  ( ph -> A. f A. g A. h ( ( f ( C Func D ) g /\ f ( C Func D ) h ) -> g = h ) )
28 dffun2 
 |-  ( Fun ( C Func D ) <-> ( Rel ( C Func D ) /\ A. f A. g A. h ( ( f ( C Func D ) g /\ f ( C Func D ) h ) -> g = h ) ) )
29 28 biimpri 
 |-  ( ( Rel ( C Func D ) /\ A. f A. g A. h ( ( f ( C Func D ) g /\ f ( C Func D ) h ) -> g = h ) ) -> Fun ( C Func D ) )
30 3 27 29 sylancr 
 |-  ( ph -> Fun ( C Func D ) )