Theorem funcfn2

Description: The morphism part of a functor is a function. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	funcfn2.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	funcfn2.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
Assertion	funcfn2	⊢ ( 𝜑 → 𝐺 Fn ( 𝐵 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		funcfn2.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
2		funcfn2.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
3		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
4		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
5	1 3 4 2	funcixp	⊢ ( 𝜑 → 𝐺 ∈ X 𝑥 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) ) ↑m ( ( Hom ‘ 𝐷 ) ‘ 𝑥 ) ) )
6		ixpfn	⊢ ( 𝐺 ∈ X 𝑥 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) ) ↑m ( ( Hom ‘ 𝐷 ) ‘ 𝑥 ) ) → 𝐺 Fn ( 𝐵 × 𝐵 ) )
7	5 6	syl	⊢ ( 𝜑 → 𝐺 Fn ( 𝐵 × 𝐵 ) )