cofu1st2nd

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

	Ref	Expression
Hypotheses	cofu1st2nd.f	$⊢ φ \to F \in (C Func D)$
	cofu1st2nd.g	$⊢ φ \to G \in (D Func E)$
Assertion	cofu1st2nd	$⊢ φ \to G \circ_{func} F = ⟨1^{st} (G), 2^{nd} (G)⟩ \circ_{func} ⟨1^{st} (F), 2^{nd} (F)⟩$

Step	Hyp	Ref	Expression
1		cofu1st2nd.f	$⊢ φ \to F \in (C Func D)$
2		cofu1st2nd.g	$⊢ φ \to G \in (D Func E)$
3		relfunc	$⊢ Rel (D Func E)$
4		1st2nd	$⊢ (Rel (D Func E) \land G \in (D Func E)) \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
5	3 2 4	sylancr	$⊢ φ \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
6		relfunc	$⊢ Rel (C Func D)$
7		1st2nd	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
8	6 1 7	sylancr	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
9	5 8	oveq12d	$⊢ φ \to G \circ_{func} F = ⟨1^{st} (G), 2^{nd} (G)⟩ \circ_{func} ⟨1^{st} (F), 2^{nd} (F)⟩$

Metamath Proof Explorer