Theorem natcl

Description: A component of a natural transformation is a morphism. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	natrcl.1	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	natixp.2	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) )
	natixp.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	natixp.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	natcl.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	natcl	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐾 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		natrcl.1	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
2		natixp.2	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) )
3		natixp.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
4		natixp.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
5		natcl.1	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6	1 2 3 4	natixp	⊢ ( 𝜑 → 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) )
7		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
8		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐾 ‘ 𝑥 ) = ( 𝐾 ‘ 𝑋 ) )
9	7 8	oveq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐾 ‘ 𝑋 ) ) )
10	9	fvixp	⊢ ( ( 𝐴 ∈ X 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐾 ‘ 𝑥 ) ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑋 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐾 ‘ 𝑋 ) ) )
11	6 5 10	syl2anc	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) ∈ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐾 ‘ 𝑋 ) ) )