Theorem funcixp

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

	Ref	Expression
Hypotheses	funcixp.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	funcixp.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	funcixp.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
	funcixp.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
Assertion	funcixp	⊢ ( 𝜑 → 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		funcixp.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
2		funcixp.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
3		funcixp.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
4		funcixp.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
5		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
6		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
7		eqid	⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
8		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
9		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
10		df-br	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
11	4 10	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
12		funcrcl	⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
13	11 12	syl	⊢ ( 𝜑 → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
14	13	simpld	⊢ ( 𝜑 → 𝐷 ∈ Cat )
15	13	simprd	⊢ ( 𝜑 → 𝐸 ∈ Cat )
16	1 5 2 3 6 7 8 9 14 15	isfunc	⊢ ( 𝜑 → ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐸 ) ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
17	4 16	mpbid	⊢ ( 𝜑 → ( 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐸 ) ∧ 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑚 ∈ ( 𝑥 𝐻 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 𝐻 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐷 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) )
18	17	simp2d	⊢ ( 𝜑 → 𝐺 ∈ X 𝑧 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( 𝐻 ‘ 𝑧 ) ) )