Theorem natfn2

Description: A natural transformation is a function on the objects of the source category. (Contributed by Zhi Wang, 14-Sep-2026)

	Ref	Expression
Hypotheses	isnat3.n	$$⊢N=C\mathrm{Nat}D$$
	isnat3.b	$$⊢B={\mathrm{Base}}_C$$
	natfn2.a	$$⊢\phi \to A\in \left(FNG\right)$$
Assertion	natfn2	$$⊢\phi \to AFnB$$

Proof

Step	Hyp	Ref	Expression
1		isnat3.n	$$⊢N=C\mathrm{Nat}D$$
2		isnat3.b	$$⊢B={\mathrm{Base}}_C$$
3		natfn2.a	$$⊢\phi \to A\in \left(FNG\right)$$
4	1 3	nat1st2nd	$$⊢\phi \to A\in \left(⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩N⟨1^{st}\left(G\right),2^{nd}\left(G\right)⟩\right)$$
5	1 4 2	natfn	$$⊢\phi \to AFnB$$