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

Metamath Proof Explorer

Theorem funcrcl

Description: Reverse closure for a functor. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion funcrcl 
|- ( F e. ( D Func E ) -> ( D e. Cat /\ E e. Cat ) )

Proof

Step Hyp Ref Expression
1 df-func 
 |-  Func = ( t e. Cat , u e. Cat |-> { <. f , g >. | [. ( Base ` t ) / b ]. ( f : b --> ( Base ` u ) /\ g e. X_ z e. ( b X. b ) ( ( ( f ` ( 1st ` z ) ) ( Hom ` u ) ( f ` ( 2nd ` z ) ) ) ^m ( ( Hom ` t ) ` z ) ) /\ A. x e. b ( ( ( x g x ) ` ( ( Id ` t ) ` x ) ) = ( ( Id ` u ) ` ( f ` x ) ) /\ A. y e. b A. z e. b A. m e. ( x ( Hom ` t ) y ) A. n e. ( y ( Hom ` t ) z ) ( ( x g z ) ` ( n ( <. x , y >. ( comp ` t ) z ) m ) ) = ( ( ( y g z ) ` n ) ( <. ( f ` x ) , ( f ` y ) >. ( comp ` u ) ( f ` z ) ) ( ( x g y ) ` m ) ) ) ) } )
2 1 elmpocl 
 |-  ( F e. ( D Func E ) -> ( D e. Cat /\ E e. Cat ) )