Theorem funcf1

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

	Ref	Expression
Hypotheses	funcf1.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	funcf1.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
	funcf1.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
Assertion	funcf1	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )

Proof

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