xpcfuccocl

Description: The composition of two natural transformations is a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025)

	Ref	Expression
Hypotheses	xpcfuchom2.t	$⊢ T = (B FuncCat C) \times_{c} (D FuncCat E)$
	xpcfucco2.o	$⊢ O = comp (T)$
	xpcfucco2.f	$⊢ φ \to F \in (M (B Nat C) P)$
	xpcfucco2.g	$⊢ φ \to G \in (N (D Nat E) Q)$
	xpcfucco2.k	$⊢ φ \to K \in (P (B Nat C) R)$
	xpcfucco2.l	$⊢ φ \to L \in (Q (D Nat E) S)$
Assertion	xpcfuccocl	$⊢ φ \to ⟨K, L⟩ (⟨⟨M, N⟩, ⟨P, Q⟩⟩ O ⟨R, S⟩) ⟨F, G⟩ \in ((M (B Nat C) R) \times (N (D Nat E) S))$

Step	Hyp	Ref	Expression
1		xpcfuchom2.t	$⊢ T = (B FuncCat C) \times_{c} (D FuncCat E)$
2		xpcfucco2.o	$⊢ O = comp (T)$
3		xpcfucco2.f	$⊢ φ \to F \in (M (B Nat C) P)$
4		xpcfucco2.g	$⊢ φ \to G \in (N (D Nat E) Q)$
5		xpcfucco2.k	$⊢ φ \to K \in (P (B Nat C) R)$
6		xpcfucco2.l	$⊢ φ \to L \in (Q (D Nat E) S)$
7	1 2 3 4 5 6	xpcfucco2	$⊢ φ \to ⟨K, L⟩ (⟨⟨M, N⟩, ⟨P, Q⟩⟩ O ⟨R, S⟩) ⟨F, G⟩ = ⟨K (⟨M, P⟩ comp (B FuncCat C) R) F, L (⟨N, Q⟩ comp (D FuncCat E) S) G⟩$
8		eqid	$⊢ B FuncCat C = B FuncCat C$
9		eqid	$⊢ B Nat C = B Nat C$
10		eqid	$⊢ comp (B FuncCat C) = comp (B FuncCat C)$
11	8 9 10 3 5	fuccocl	$⊢ φ \to K (⟨M, P⟩ comp (B FuncCat C) R) F \in (M (B Nat C) R)$
12		eqid	$⊢ D FuncCat E = D FuncCat E$
13		eqid	$⊢ D Nat E = D Nat E$
14		eqid	$⊢ comp (D FuncCat E) = comp (D FuncCat E)$
15	12 13 14 4 6	fuccocl	$⊢ φ \to L (⟨N, Q⟩ comp (D FuncCat E) S) G \in (N (D Nat E) S)$
16	11 15	opelxpd	$⊢ φ \to ⟨K (⟨M, P⟩ comp (B FuncCat C) R) F, L (⟨N, Q⟩ comp (D FuncCat E) S) G⟩ \in ((M (B Nat C) R) \times (N (D Nat E) S))$
17	7 16	eqeltrd	$⊢ φ \to ⟨K, L⟩ (⟨⟨M, N⟩, ⟨P, Q⟩⟩ O ⟨R, S⟩) ⟨F, G⟩ \in ((M (B Nat C) R) \times (N (D Nat E) S))$

Metamath Proof Explorer