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

Metamath Proof Explorer

Theorem natcl

Description: A component of a natural transformation is a morphism. (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 )
natcl.1 
|- ( ph -> X e. B )
Assertion natcl 
|- ( ph -> ( A ` X ) e. ( ( 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 natcl.1 
 |-  ( ph -> X e. B )
6 1 2 3 4 natixp 
 |-  ( ph -> A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) )
7 fveq2 
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
8 fveq2 
 |-  ( x = X -> ( K ` x ) = ( K ` X ) )
9 7 8 oveq12d 
 |-  ( x = X -> ( ( F ` x ) J ( K ` x ) ) = ( ( F ` X ) J ( K ` X ) ) )
10 9 fvixp 
 |-  ( ( A e. X_ x e. B ( ( F ` x ) J ( K ` x ) ) /\ X e. B ) -> ( A ` X ) e. ( ( F ` X ) J ( K ` X ) ) )
11 6 5 10 syl2anc 
 |-  ( ph -> ( A ` X ) e. ( ( F ` X ) J ( K ` X ) ) )