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 ), and can be obtained from funcf2 , f002 , and ralrimivva . (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	bitrid	|- ( 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 ) )