Theorem natrcl

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

	Ref	Expression
Hypothesis	natrcl.1	|- N = ( C Nat D )
Assertion	natrcl	|- ( A e. ( F N G ) -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )

Proof

Step	Hyp	Ref	Expression
1		natrcl.1	|- N = ( C Nat D )
2		eqid	|- ( Base ` C ) = ( Base ` C )
3		eqid	|- ( Hom ` C ) = ( Hom ` C )
4		eqid	|- ( Hom ` D ) = ( Hom ` D )
5		eqid	|- ( comp ` D ) = ( comp ` D )
6	1 2 3 4 5	natfval	|- N = ( f e. ( C Func D ) , g e. ( C Func D ) |-> [_ ( 1st ` f ) / r ]_ [_ ( 1st ` g ) / s ]_ { a e. X_ x e. ( Base ` C ) ( ( r ` x ) ( Hom ` D ) ( s ` x ) ) | A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. h e. ( x ( Hom ` C ) y ) ( ( a ` y ) ( <. ( r ` x ) , ( r ` y ) >. ( comp ` D ) ( s ` y ) ) ( ( x ( 2nd ` f ) y ) ` h ) ) = ( ( ( x ( 2nd ` g ) y ) ` h ) ( <. ( r ` x ) , ( s ` x ) >. ( comp ` D ) ( s ` y ) ) ( a ` x ) ) } )
7	6	elmpocl	|- ( A e. ( F N G ) -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )