Theorem cofu1st2nd

Description: Rewrite the functor composition with separated functor parts. (Contributed by Zhi Wang, 15-Nov-2025)

	Ref	Expression
Hypotheses	cofu1st2nd.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	cofu1st2nd.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
Assertion	cofu1st2nd	⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) = ( ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ ∘func ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		cofu1st2nd.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
2		cofu1st2nd.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
3		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
4		1st2nd	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐷 Func 𝐸 ) ) → 𝐺 = ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ )
5	3 2 4	sylancr	⊢ ( 𝜑 → 𝐺 = ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ )
6		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
7		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 = ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
8	6 1 7	sylancr	⊢ ( 𝜑 → 𝐹 = ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ )
9	5 8	oveq12d	⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) = ( ⟨ ( 1st ‘ 𝐺 ) , ( 2nd ‘ 𝐺 ) ⟩ ∘func ⟨ ( 1st ‘ 𝐹 ) , ( 2nd ‘ 𝐹 ) ⟩ ) )