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	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	natixp.2	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) )
	natixp.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion	natfn	⊢ ( 𝜑 → 𝐴 Fn 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		natrcl.1	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
2		natixp.2	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) )
3		natixp.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
5	1 2 3 4	natixp	⊢ ( 𝜑 → 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐾 ‘ 𝑥 ) ) )
6		ixpfn	⊢ ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐾 ‘ 𝑥 ) ) → 𝐴 Fn 𝐵 )
7	5 6	syl	⊢ ( 𝜑 → 𝐴 Fn 𝐵 )