Theorem fuco11

Description: The object part of the functor composition bifunctor maps two functors to their composition. (Contributed by Zhi Wang, 30-Sep-2025)

	Ref	Expression
Hypotheses	fuco11.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	fuco11.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
	fuco11.k	⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
	fuco11.u	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
Assertion	fuco11	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑈 ) = ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		fuco11.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		fuco11.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
3		fuco11.k	⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
4		fuco11.u	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
5	2	funcrcl2	⊢ ( 𝜑 → 𝐶 ∈ Cat )
6	3	funcrcl2	⊢ ( 𝜑 → 𝐷 ∈ Cat )
7	3	funcrcl3	⊢ ( 𝜑 → 𝐸 ∈ Cat )
8		eqidd	⊢ ( 𝜑 → ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
9	5 6 7 1 8	fuco1	⊢ ( 𝜑 → 𝑂 = ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) )
10	9	fveq1d	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑈 ) = ( ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ‘ 𝑈 ) )
11	8 4 3 2	fuco2eld	⊢ ( 𝜑 → 𝑈 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
12	11	fvresd	⊢ ( 𝜑 → ( ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) ‘ 𝑈 ) = ( ∘func ‘ 𝑈 ) )
13	4	fveq2d	⊢ ( 𝜑 → ( ∘func ‘ 𝑈 ) = ( ∘func ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) )
14		df-ov	⊢ ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ( ∘func ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
15	13 14	eqtr4di	⊢ ( 𝜑 → ( ∘func ‘ 𝑈 ) = ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) )
16	10 12 15	3eqtrd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑈 ) = ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) )