Metamath Proof Explorer

Theorem fuco112x

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⟩⟩$
		fuco111x.x	$⊢ φ \to X \in {Base}_{C}$
		fuco112x.y	$⊢ φ \to Y \in {Base}_{C}$
	Assertion	fuco112x	$⊢ φ \to X 2^{nd} (O (U)) Y = (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		fuco111x.x	$⊢ φ \to X \in {Base}_{C}$
6		fuco112x.y	$⊢ φ \to Y \in {Base}_{C}$
7		eqid	$⊢ {Base}_{C} = {Base}_{C}$
8	1 2 3 4 7	fuco112	$⊢ φ \to 2^{nd} (O (U)) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (F (x) L F (y)) \circ (x G y))$
9		simprl	$⊢ (φ \land (x = X \land y = Y)) \to x = X$
10	9	fveq2d	$⊢ (φ \land (x = X \land y = Y)) \to F (x) = F (X)$
11		simprr	$⊢ (φ \land (x = X \land y = Y)) \to y = Y$
12	11	fveq2d	$⊢ (φ \land (x = X \land y = Y)) \to F (y) = F (Y)$
13	10 12	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to F (x) L F (y) = F (X) L F (Y)$
14	9 11	oveq12d	$⊢ (φ \land (x = X \land y = Y)) \to x G y = X G Y$
15	13 14	coeq12d	$⊢ (φ \land (x = X \land y = Y)) \to (F (x) L F (y)) \circ (x G y) = (F (X) L F (Y)) \circ (X G Y)$
16		ovexd	$⊢ φ \to F (X) L F (Y) \in V$
17		ovexd	$⊢ φ \to X G Y \in V$
18	16 17	coexd	$⊢ φ \to (F (X) L F (Y)) \circ (X G Y) \in V$
19	8 15 5 6 18	ovmpod	$⊢ φ \to X 2^{nd} (O (U)) Y = (F (X) L F (Y)) \circ (X G Y)$