Metamath Proof Explorer

Theorem fuco111

Description: The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the object part of the composed functor. (Contributed by Zhi Wang, 2-Oct-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	fuco111	$⊢ φ \to 1^{st} (O (U)) = K \circ F$

Proof

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		eqid	$⊢ {Base}_{C} = {Base}_{C}$
6	1 2 3 4 5	fuco11a	$⊢ φ \to O (U) = ⟨K \circ F, (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (F (x) L F (y)) \circ (x G y))⟩$
7	6	fveq2d	$⊢ φ \to 1^{st} (O (U)) = 1^{st} (⟨K \circ F, (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (F (x) L F (y)) \circ (x G y))⟩)$
8		relfunc	$⊢ Rel (D Func E)$
9	8	brrelex1i	$⊢ K (D Func E) L \to K \in V$
10	3 9	syl	$⊢ φ \to K \in V$
11		relfunc	$⊢ Rel (C Func D)$
12	11	brrelex1i	$⊢ F (C Func D) G \to F \in V$
13	2 12	syl	$⊢ φ \to F \in V$
14	10 13	coexd	$⊢ φ \to K \circ F \in V$
15		fvex	$⊢ {Base}_{C} \in V$
16	15 15	mpoex	$⊢ (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (F (x) L F (y)) \circ (x G y)) \in V$
17		op1stg	$⊢ (K \circ F \in V \land (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (F (x) L F (y)) \circ (x G y)) \in V) \to 1^{st} (⟨K \circ F, (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (F (x) L F (y)) \circ (x G y))⟩) = K \circ F$
18	14 16 17	sylancl	$⊢ φ \to 1^{st} (⟨K \circ F, (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (F (x) L F (y)) \circ (x G y))⟩) = K \circ F$
19	7 18	eqtrd	$⊢ φ \to 1^{st} (O (U)) = K \circ F$