fuco11cl

Description: The object part of the functor composition bifunctor maps into ( C Func E ) . (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	fuco11cl	$⊢ φ \to O (U) \in (C Func E)$

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	fucof1	$⊢ φ \to O : (D Func E) \times (C Func D) ⟶ C Func E$
10	8 4 3 2	fuco2eld	$⊢ φ \to U \in ((D Func E) \times (C Func D))$
11	9 10	ffvelcdmd	$⊢ φ \to O (U) \in (C Func E)$

Metamath Proof Explorer