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\mathrm{Nat}D$$
	natixp.2	$$⊢\phi \to A\in \left(⟨F,G⟩N⟨K,L⟩\right)$$
	natixp.b	$$⊢B={\mathrm{Base}}_C$$
	natixp.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	natcl.1	$$⊢\phi \to X\in B$$
Assertion	natcl	$$⊢\phi \to A\left(X\right)\in \left(F\left(X\right)JK\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		natrcl.1	$$⊢N=C\mathrm{Nat}D$$
2		natixp.2	$$⊢\phi \to A\in \left(⟨F,G⟩N⟨K,L⟩\right)$$
3		natixp.b	$$⊢B={\mathrm{Base}}_C$$
4		natixp.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
5		natcl.1	$$⊢\phi \to X\in B$$
6	1 2 3 4	natixp	$$⊢\phi \to A\in \underset{x\in B}{⨉}\left(F\left(x\right)JK\left(x\right)\right)$$
7		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
8		fveq2	$$⊢x=X\to K\left(x\right)=K\left(X\right)$$
9	7 8	oveq12d	$$⊢x=X\to F\left(x\right)JK\left(x\right)=F\left(X\right)JK\left(X\right)$$
10	9	fvixp	$$⊢\left(A\in \underset{x\in B}{⨉}\left(F\left(x\right)JK\left(x\right)\right)\wedge X\in B\right)\to A\left(X\right)\in \left(F\left(X\right)JK\left(X\right)\right)$$
11	6 5 10	syl2anc	$$⊢\phi \to A\left(X\right)\in \left(F\left(X\right)JK\left(X\right)\right)$$