Theorem natixp

Description: A natural transformation is a function from the objects of C to homomorphisms from F ( x ) to G ( x ) . (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	natrcl.1	|- N = ( C Nat D )
	natixp.2	|- ( ph -> A e. ( <. F , G >. N <. K , L >. ) )
	natixp.b	|- B = ( Base ` C )
	natixp.j	|- J = ( Hom ` D )
Assertion	natixp	|- ( ph -> A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		natrcl.1	|- N = ( C Nat D )
2		natixp.2	|- ( ph -> A e. ( <. F , G >. N <. K , L >. ) )
3		natixp.b	|- B = ( Base ` C )
4		natixp.j	|- J = ( Hom ` D )
5		eqid	|- ( Hom ` C ) = ( Hom ` C )
6		eqid	|- ( comp ` D ) = ( comp ` D )
7	1	natrcl	|- ( A e. ( <. F , G >. N <. K , L >. ) -> ( <. F , G >. e. ( C Func D ) /\ <. K , L >. e. ( C Func D ) ) )
8	2 7	syl	|- ( ph -> ( <. F , G >. e. ( C Func D ) /\ <. K , L >. e. ( C Func D ) ) )
9	8	simpld	|- ( ph -> <. F , G >. e. ( C Func D ) )
10		df-br	|- ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
11	9 10	sylibr	|- ( ph -> F ( C Func D ) G )
12	8	simprd	|- ( ph -> <. K , L >. e. ( C Func D ) )
13		df-br	|- ( K ( C Func D ) L <-> <. K , L >. e. ( C Func D ) )
14	12 13	sylibr	|- ( ph -> K ( C Func D ) L )
15	1 3 5 4 6 11 14	isnat	|- ( ph -> ( A e. ( <. F , G >. N <. K , L >. ) <-> ( A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) /\ A. x e. B A. y e. B A. z e. ( x ( Hom ` C ) y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( K ` y ) ) ( ( x G y ) ` z ) ) = ( ( ( x L y ) ` z ) ( <. ( F ` x ) , ( K ` x ) >. ( comp ` D ) ( K ` y ) ) ( A ` x ) ) ) ) )
16	2 15	mpbid	|- ( ph -> ( A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) /\ A. x e. B A. y e. B A. z e. ( x ( Hom ` C ) y ) ( ( A ` y ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` D ) ( K ` y ) ) ( ( x G y ) ` z ) ) = ( ( ( x L y ) ` z ) ( <. ( F ` x ) , ( K ` x ) >. ( comp ` D ) ( K ` y ) ) ( A ` x ) ) ) )
17	16	simpld	|- ( ph -> A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) )