This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )