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	⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
	fucofval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
	fucofval.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
	fuco1.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	fuco1.w	⊢ ( 𝜑 → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
Assertion	fucof1	⊢ ( 𝜑 → 𝑂 : 𝑊 ⟶ ( 𝐶 Func 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		fucofval.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑇 )
2		fucofval.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
3		fucofval.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
4		fuco1.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
5		fuco1.w	⊢ ( 𝜑 → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
6		rescofuf	⊢ ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) : ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ⟶ ( 𝐶 Func 𝐸 )
7	1 2 3 4 5	fuco1	⊢ ( 𝜑 → 𝑂 = ( ∘func ↾ 𝑊 ) )
8	5	reseq2d	⊢ ( 𝜑 → ( ∘func ↾ 𝑊 ) = ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) )
9	7 8	eqtrd	⊢ ( 𝜑 → 𝑂 = ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) )
10	9 5	feq12d	⊢ ( 𝜑 → ( 𝑂 : 𝑊 ⟶ ( 𝐶 Func 𝐸 ) ↔ ( ∘func ↾ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ) : ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ⟶ ( 𝐶 Func 𝐸 ) ) )
11	6 10	mpbiri	⊢ ( 𝜑 → 𝑂 : 𝑊 ⟶ ( 𝐶 Func 𝐸 ) )