Metamath Proof Explorer

Theorem fucof1

Description: The object part of the functor composition bifunctor maps ( ( D Func E ) X. ( C Func D ) ) into ( C Func E ) . (Contributed by Zhi Wang, 29-Sep-2025)

		Ref	Expression
	Hypotheses	fucofval.c	$⊢ φ \to C \in T$
		fucofval.d	$⊢ φ \to D \in U$
		fucofval.e	$⊢ φ \to E \in V$
		fuco1.o	No typesetting found for \|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. ) with typecode \|-
		fuco1.w	$⊢ φ \to W = (D Func E) \times (C Func D)$
	Assertion	fucof1	$⊢ φ \to O : W ⟶ C Func E$

Proof

Step	Hyp	Ref	Expression
1		fucofval.c	$⊢ φ \to C \in T$
2		fucofval.d	$⊢ φ \to D \in U$
3		fucofval.e	$⊢ φ \to E \in V$
4		fuco1.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 \|-
5		fuco1.w	$⊢ φ \to W = (D Func E) \times (C Func D)$
6		rescofuf	$⊢ ({\circ_{func} ↾}_{((D Func E) \times (C Func D))}) : (D Func E) \times (C Func D) ⟶ C Func E$
7	1 2 3 4 5	fuco1	$⊢ φ \to O = {\circ_{func} ↾}_{W}$
8	5	reseq2d	$⊢ φ \to {\circ_{func} ↾}_{W} = {\circ_{func} ↾}_{((D Func E) \times (C Func D))}$
9	7 8	eqtrd	$⊢ φ \to O = {\circ_{func} ↾}_{((D Func E) \times (C Func D))}$
10	9 5	feq12d	$⊢ φ \to (O : W ⟶ C Func E \leftrightarrow ({\circ_{func} ↾}_{((D Func E) \times (C Func D))}) : (D Func E) \times (C Func D) ⟶ C Func E)$
11	6 10	mpbiri	$⊢ φ \to O : W ⟶ C Func E$