Metamath Proof Explorer

Theorem fuco112

Description: The object part of the functor composition bifunctor maps two functors to their composition, expressed explicitly for the morphism part of the composed functor. (Contributed by Zhi Wang, 3-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⟩⟩$
		fuco11a.b	$⊢ B = {Base}_{C}$
	Assertion	fuco112	$⊢ φ \to 2^{nd} (O (U)) = (x \in B, y \in B ⟼ (F (x) L F (y)) \circ (x G y))$

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		fuco11a.b	$⊢ B = {Base}_{C}$
6	1 2 3 4 5	fuco11a	$⊢ φ \to O (U) = ⟨K \circ F, (x \in B, y \in B ⟼ (F (x) L F (y)) \circ (x G y))⟩$
7	6	fveq2d	$⊢ φ \to 2^{nd} (O (U)) = 2^{nd} (⟨K \circ F, (x \in B, y \in B ⟼ (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	5	fvexi	$⊢ B \in V$
16	15 15	mpoex	$⊢ (x \in B, y \in B ⟼ (F (x) L F (y)) \circ (x G y)) \in V$
17		op2ndg	$⊢ (K \circ F \in V \land (x \in B, y \in B ⟼ (F (x) L F (y)) \circ (x G y)) \in V) \to 2^{nd} (⟨K \circ F, (x \in B, y \in B ⟼ (F (x) L F (y)) \circ (x G y))⟩) = (x \in B, y \in B ⟼ (F (x) L F (y)) \circ (x G y))$
18	14 16 17	sylancl	$⊢ φ \to 2^{nd} (⟨K \circ F, (x \in B, y \in B ⟼ (F (x) L F (y)) \circ (x G y))⟩) = (x \in B, y \in B ⟼ (F (x) L F (y)) \circ (x G y))$
19	7 18	eqtrd	$⊢ φ \to 2^{nd} (O (U)) = (x \in B, y \in B ⟼ (F (x) L F (y)) \circ (x G y))$