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	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
	fuco11.f	$⊢ φ \to F (C Func D) G$
	fuco11.k	$⊢ φ \to K (D Func E) L$
	fuco11.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
Assertion	fuco11	$⊢ φ \to O (U) = ⟨K, L⟩ \circ_{func} ⟨F, G⟩$

Step	Hyp	Ref	Expression
1		fuco11.o	Could not format ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) : No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
2		fuco11.f	$⊢ φ \to F (C Func D) G$
3		fuco11.k	$⊢ φ \to K (D Func E) L$
4		fuco11.u	$⊢ φ \to U = ⟨⟨K, L⟩, ⟨F, G⟩⟩$
5	2	funcrcl2	$⊢ φ \to C \in Cat$
6	3	funcrcl2	$⊢ φ \to D \in Cat$
7	3	funcrcl3	$⊢ φ \to E \in Cat$
8		eqidd	$⊢ φ \to (D Func E) \times (C Func D) = (D Func E) \times (C Func D)$
9	5 6 7 1 8	fuco1	$⊢ φ \to O = {\circ_{func} ↾}_{((D Func E) \times (C Func D))}$
10	9	fveq1d	$⊢ φ \to O (U) = ({\circ_{func} ↾}_{((D Func E) \times (C Func D))}) (U)$
11	8 4 3 2	fuco2eld	$⊢ φ \to U \in ((D Func E) \times (C Func D))$
12	11	fvresd	$⊢ φ \to ({\circ_{func} ↾}_{((D Func E) \times (C Func D))}) (U) = \circ_{func} (U)$
13	4	fveq2d	$⊢ φ \to \circ_{func} (U) = \circ_{func} (⟨⟨K, L⟩, ⟨F, G⟩⟩)$
14		df-ov	$⊢ ⟨K, L⟩ \circ_{func} ⟨F, G⟩ = \circ_{func} (⟨⟨K, L⟩, ⟨F, G⟩⟩)$
15	13 14	eqtr4di	$⊢ φ \to \circ_{func} (U) = ⟨K, L⟩ \circ_{func} ⟨F, G⟩$
16	10 12 15	3eqtrd	$⊢ φ \to O (U) = ⟨K, L⟩ \circ_{func} ⟨F, G⟩$

Metamath Proof Explorer