Metamath Proof Explorer

Theorem functhinc

Description: A functor to a thin category is determined entirely by the object part. The hypothesis "functhinc.1" is related to a monotone function if preorders induced by the categories are considered ( catprs2 ). (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Hypotheses functhinc.b 
|- B = ( Base ` D )
functhinc.c 
|- C = ( Base ` E )
functhinc.h 
|- H = ( Hom ` D )
functhinc.j 
|- J = ( Hom ` E )
functhinc.d 
|- ( ph -> D e. Cat )
functhinc.e 
|- ( ph -> E e. ThinCat )
functhinc.f 
|- ( ph -> F : B --> C )
functhinc.k 
|- K = ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) )
functhinc.1 
|- ( ph -> A. z e. B A. w e. B ( ( ( F ` z ) J ( F ` w ) ) = (/) -> ( z H w ) = (/) ) )
Assertion functhinc 
|- ( ph -> ( F ( D Func E ) G <-> G = K ) )

Proof

Step Hyp Ref Expression
1 functhinc.b 
 |-  B = ( Base ` D )
2 functhinc.c 
 |-  C = ( Base ` E )
3 functhinc.h 
 |-  H = ( Hom ` D )
4 functhinc.j 
 |-  J = ( Hom ` E )
5 functhinc.d 
 |-  ( ph -> D e. Cat )
6 functhinc.e 
 |-  ( ph -> E e. ThinCat )
7 functhinc.f 
 |-  ( ph -> F : B --> C )
8 functhinc.k 
 |-  K = ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) )
9 functhinc.1 
 |-  ( ph -> A. z e. B A. w e. B ( ( ( F ` z ) J ( F ` w ) ) = (/) -> ( z H w ) = (/) ) )
10 eqid 
 |-  ( Id ` D ) = ( Id ` D )
11 eqid 
 |-  ( Id ` E ) = ( Id ` E )
12 eqid 
 |-  ( comp ` D ) = ( comp ` D )
13 eqid 
 |-  ( comp ` E ) = ( comp ` E )
14 6 thinccd 
 |-  ( ph -> E e. Cat )
15 1 2 3 4 10 11 12 13 5 14 isfunc 
 |-  ( ph -> ( F ( D Func E ) G <-> ( F : B --> C /\ G e. X_ c e. ( B X. B ) ( ( ( F ` ( 1st ` c ) ) J ( F ` ( 2nd ` c ) ) ) ^m ( H ` c ) ) /\ A. a e. B ( ( ( a G a ) ` ( ( Id ` D ) ` a ) ) = ( ( Id ` E ) ` ( F ` a ) ) /\ A. b e. B A. c e. B A. f e. ( a H b ) A. g e. ( b H c ) ( ( a G c ) ` ( g ( <. a , b >. ( comp ` D ) c ) f ) ) = ( ( ( b G c ) ` g ) ( <. ( F ` a ) , ( F ` b ) >. ( comp ` E ) ( F ` c ) ) ( ( a G b ) ` f ) ) ) ) ) )
16 3anass 
 |-  ( ( F : B --> C /\ G e. X_ c e. ( B X. B ) ( ( ( F ` ( 1st ` c ) ) J ( F ` ( 2nd ` c ) ) ) ^m ( H ` c ) ) /\ A. a e. B ( ( ( a G a ) ` ( ( Id ` D ) ` a ) ) = ( ( Id ` E ) ` ( F ` a ) ) /\ A. b e. B A. c e. B A. f e. ( a H b ) A. g e. ( b H c ) ( ( a G c ) ` ( g ( <. a , b >. ( comp ` D ) c ) f ) ) = ( ( ( b G c ) ` g ) ( <. ( F ` a ) , ( F ` b ) >. ( comp ` E ) ( F ` c ) ) ( ( a G b ) ` f ) ) ) ) <-> ( F : B --> C /\ ( G e. X_ c e. ( B X. B ) ( ( ( F ` ( 1st ` c ) ) J ( F ` ( 2nd ` c ) ) ) ^m ( H ` c ) ) /\ A. a e. B ( ( ( a G a ) ` ( ( Id ` D ) ` a ) ) = ( ( Id ` E ) ` ( F ` a ) ) /\ A. b e. B A. c e. B A. f e. ( a H b ) A. g e. ( b H c ) ( ( a G c ) ` ( g ( <. a , b >. ( comp ` D ) c ) f ) ) = ( ( ( b G c ) ` g ) ( <. ( F ` a ) , ( F ` b ) >. ( comp ` E ) ( F ` c ) ) ( ( a G b ) ` f ) ) ) ) ) )
17 15 16 bitrdi 
 |-  ( ph -> ( F ( D Func E ) G <-> ( F : B --> C /\ ( G e. X_ c e. ( B X. B ) ( ( ( F ` ( 1st ` c ) ) J ( F ` ( 2nd ` c ) ) ) ^m ( H ` c ) ) /\ A. a e. B ( ( ( a G a ) ` ( ( Id ` D ) ` a ) ) = ( ( Id ` E ) ` ( F ` a ) ) /\ A. b e. B A. c e. B A. f e. ( a H b ) A. g e. ( b H c ) ( ( a G c ) ` ( g ( <. a , b >. ( comp ` D ) c ) f ) ) = ( ( ( b G c ) ` g ) ( <. ( F ` a ) , ( F ` b ) >. ( comp ` E ) ( F ` c ) ) ( ( a G b ) ` f ) ) ) ) ) ) )
18 7 17 mpbirand 
 |-  ( ph -> ( F ( D Func E ) G <-> ( G e. X_ c e. ( B X. B ) ( ( ( F ` ( 1st ` c ) ) J ( F ` ( 2nd ` c ) ) ) ^m ( H ` c ) ) /\ A. a e. B ( ( ( a G a ) ` ( ( Id ` D ) ` a ) ) = ( ( Id ` E ) ` ( F ` a ) ) /\ A. b e. B A. c e. B A. f e. ( a H b ) A. g e. ( b H c ) ( ( a G c ) ` ( g ( <. a , b >. ( comp ` D ) c ) f ) ) = ( ( ( b G c ) ` g ) ( <. ( F ` a ) , ( F ` b ) >. ( comp ` E ) ( F ` c ) ) ( ( a G b ) ` f ) ) ) ) ) )
19 funcf2lem 
 |-  ( G e. X_ c e. ( B X. B ) ( ( ( F ` ( 1st ` c ) ) J ( F ` ( 2nd ` c ) ) ) ^m ( H ` c ) ) <-> ( G e. _V /\ G Fn ( B X. B ) /\ A. v e. B A. u e. B ( v G u ) : ( v H u ) --> ( ( F ` v ) J ( F ` u ) ) ) )
20 simprl 
 |-  ( ( ph /\ ( v e. B /\ u e. B ) ) -> v e. B )
21 simprr 
 |-  ( ( ph /\ ( v e. B /\ u e. B ) ) -> u e. B )
22 9 adantr 
 |-  ( ( ph /\ ( v e. B /\ u e. B ) ) -> A. z e. B A. w e. B ( ( ( F ` z ) J ( F ` w ) ) = (/) -> ( z H w ) = (/) ) )
23 20 21 22 functhinclem2 
 |-  ( ( ph /\ ( v e. B /\ u e. B ) ) -> ( ( ( F ` v ) J ( F ` u ) ) = (/) -> ( v H u ) = (/) ) )
24 1 2 3 4 6 7 8 23 functhinclem1 
 |-  ( ph -> ( ( G e. _V /\ G Fn ( B X. B ) /\ A. v e. B A. u e. B ( v G u ) : ( v H u ) --> ( ( F ` v ) J ( F ` u ) ) ) <-> G = K ) )
25 19 24 syl5bb 
 |-  ( ph -> ( G e. X_ c e. ( B X. B ) ( ( ( F ` ( 1st ` c ) ) J ( F ` ( 2nd ` c ) ) ) ^m ( H ` c ) ) <-> G = K ) )
26 25 anbi1d 
 |-  ( ph -> ( ( G e. X_ c e. ( B X. B ) ( ( ( F ` ( 1st ` c ) ) J ( F ` ( 2nd ` c ) ) ) ^m ( H ` c ) ) /\ A. a e. B ( ( ( a G a ) ` ( ( Id ` D ) ` a ) ) = ( ( Id ` E ) ` ( F ` a ) ) /\ A. b e. B A. c e. B A. f e. ( a H b ) A. g e. ( b H c ) ( ( a G c ) ` ( g ( <. a , b >. ( comp ` D ) c ) f ) ) = ( ( ( b G c ) ` g ) ( <. ( F ` a ) , ( F ` b ) >. ( comp ` E ) ( F ` c ) ) ( ( a G b ) ` f ) ) ) ) <-> ( G = K /\ A. a e. B ( ( ( a G a ) ` ( ( Id ` D ) ` a ) ) = ( ( Id ` E ) ` ( F ` a ) ) /\ A. b e. B A. c e. B A. f e. ( a H b ) A. g e. ( b H c ) ( ( a G c ) ` ( g ( <. a , b >. ( comp ` D ) c ) f ) ) = ( ( ( b G c ) ` g ) ( <. ( F ` a ) , ( F ` b ) >. ( comp ` E ) ( F ` c ) ) ( ( a G b ) ` f ) ) ) ) ) )
27 18 26 bitrd 
 |-  ( ph -> ( F ( D Func E ) G <-> ( G = K /\ A. a e. B ( ( ( a G a ) ` ( ( Id ` D ) ` a ) ) = ( ( Id ` E ) ` ( F ` a ) ) /\ A. b e. B A. c e. B A. f e. ( a H b ) A. g e. ( b H c ) ( ( a G c ) ` ( g ( <. a , b >. ( comp ` D ) c ) f ) ) = ( ( ( b G c ) ` g ) ( <. ( F ` a ) , ( F ` b ) >. ( comp ` E ) ( F ` c ) ) ( ( a G b ) ` f ) ) ) ) ) )
28 1 2 3 4 5 6 7 8 9 10 11 12 13 functhinclem4 
 |-  ( ( ph /\ G = K ) -> A. a e. B ( ( ( a G a ) ` ( ( Id ` D ) ` a ) ) = ( ( Id ` E ) ` ( F ` a ) ) /\ A. b e. B A. c e. B A. f e. ( a H b ) A. g e. ( b H c ) ( ( a G c ) ` ( g ( <. a , b >. ( comp ` D ) c ) f ) ) = ( ( ( b G c ) ` g ) ( <. ( F ` a ) , ( F ` b ) >. ( comp ` E ) ( F ` c ) ) ( ( a G b ) ` f ) ) ) )
29 27 28 mpbiran3d 
 |-  ( ph -> ( F ( D Func E ) G <-> G = K ) )