Theorem funcf1

Description: The object part of a functor is a function on objects. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	funcf1.b	|- B = ( Base ` D )
	funcf1.c	|- C = ( Base ` E )
	funcf1.f	|- ( ph -> F ( D Func E ) G )
Assertion	funcf1	|- ( ph -> F : B --> C )

Proof

Step	Hyp	Ref	Expression
1		funcf1.b	|- B = ( Base ` D )
2		funcf1.c	|- C = ( Base ` E )
3		funcf1.f	|- ( ph -> F ( D Func E ) G )
4		eqid	|- ( Hom ` D ) = ( Hom ` D )
5		eqid	|- ( Hom ` E ) = ( Hom ` E )
6		eqid	|- ( Id ` D ) = ( Id ` D )
7		eqid	|- ( Id ` E ) = ( Id ` E )
8		eqid	|- ( comp ` D ) = ( comp ` D )
9		eqid	|- ( comp ` E ) = ( comp ` E )
10		df-br	|- ( F ( D Func E ) G <-> <. F , G >. e. ( D Func E ) )
11	3 10	sylib	|- ( ph -> <. F , G >. e. ( D Func E ) )
12		funcrcl	|- ( <. F , G >. e. ( D Func E ) -> ( D e. Cat /\ E e. Cat ) )
13	11 12	syl	|- ( ph -> ( D e. Cat /\ E e. Cat ) )
14	13	simpld	|- ( ph -> D e. Cat )
15	13	simprd	|- ( ph -> E e. Cat )
16	1 2 4 5 6 7 8 9 14 15	isfunc	|- ( ph -> ( F ( D Func E ) G <-> ( F : B --> C /\ G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` E ) ( F ` ( 2nd ` z ) ) ) ^m ( ( Hom ` D ) ` z ) ) /\ A. x e. B ( ( ( x G x ) ` ( ( Id ` D ) ` x ) ) = ( ( Id ` E ) ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x ( Hom ` D ) y ) A. n e. ( y ( Hom ` D ) z ) ( ( x G z ) ` ( n ( <. x , y >. ( comp ` D ) z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` E ) ( F ` z ) ) ( ( x G y ) ` m ) ) ) ) ) )
17	3 16	mpbid	|- ( ph -> ( F : B --> C /\ G e. X_ z e. ( B X. B ) ( ( ( F ` ( 1st ` z ) ) ( Hom ` E ) ( F ` ( 2nd ` z ) ) ) ^m ( ( Hom ` D ) ` z ) ) /\ A. x e. B ( ( ( x G x ) ` ( ( Id ` D ) ` x ) ) = ( ( Id ` E ) ` ( F ` x ) ) /\ A. y e. B A. z e. B A. m e. ( x ( Hom ` D ) y ) A. n e. ( y ( Hom ` D ) z ) ( ( x G z ) ` ( n ( <. x , y >. ( comp ` D ) z ) m ) ) = ( ( ( y G z ) ` n ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` E ) ( F ` z ) ) ( ( x G y ) ` m ) ) ) ) )
18	17	simp1d	|- ( ph -> F : B --> C )