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 Nat D )
	isnat3.b	|- B = ( Base ` C )
	natfn2.a	|- ( ph -> A e. ( F N G ) )
Assertion	natfn2	|- ( ph -> A Fn B )

Proof

Step	Hyp	Ref	Expression
1		isnat3.n	|- N = ( C Nat D )
2		isnat3.b	|- B = ( Base ` C )
3		natfn2.a	|- ( ph -> A e. ( F N G ) )
4	1 3	nat1st2nd	|- ( ph -> A e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
5	1 4 2	natfn	|- ( ph -> A Fn B )