Theorem natfn

Description: A natural transformation is a function on the objects of C . (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$$
Assertion	natfn	$$⊢\phi \to AFnB$$

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		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
5	1 2 3 4	natixp	$$⊢\phi \to A\in \underset{x\in B}{⨉}\left(F\left(x\right)\mathrm{Hom}\left(D\right)K\left(x\right)\right)$$
6		ixpfn	$$⊢A\in \underset{x\in B}{⨉}\left(F\left(x\right)\mathrm{Hom}\left(D\right)K\left(x\right)\right)\to AFnB$$
7	5 6	syl	$$⊢\phi \to AFnB$$