Theorem xpcfuccocl

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

	Ref	Expression
Hypotheses	xpcfuchom2.t	⊢ 𝑇 = ( ( 𝐵 FuncCat 𝐶 ) ×c ( 𝐷 FuncCat 𝐸 ) )
	xpcfucco2.o	⊢ 𝑂 = ( comp ‘ 𝑇 )
	xpcfucco2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 ( 𝐵 Nat 𝐶 ) 𝑃 ) )
	xpcfucco2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑁 ( 𝐷 Nat 𝐸 ) 𝑄 ) )
	xpcfucco2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 ( 𝐵 Nat 𝐶 ) 𝑅 ) )
	xpcfucco2.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝑄 ( 𝐷 Nat 𝐸 ) 𝑆 ) )
Assertion	xpcfuccocl	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ( ⟨ ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑃 , 𝑄 ⟩ ⟩ 𝑂 ⟨ 𝑅 , 𝑆 ⟩ ) ⟨ 𝐹 , 𝐺 ⟩ ) ∈ ( ( 𝑀 ( 𝐵 Nat 𝐶 ) 𝑅 ) × ( 𝑁 ( 𝐷 Nat 𝐸 ) 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpcfuchom2.t	⊢ 𝑇 = ( ( 𝐵 FuncCat 𝐶 ) ×c ( 𝐷 FuncCat 𝐸 ) )
2		xpcfucco2.o	⊢ 𝑂 = ( comp ‘ 𝑇 )
3		xpcfucco2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑀 ( 𝐵 Nat 𝐶 ) 𝑃 ) )
4		xpcfucco2.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑁 ( 𝐷 Nat 𝐸 ) 𝑄 ) )
5		xpcfucco2.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 ( 𝐵 Nat 𝐶 ) 𝑅 ) )
6		xpcfucco2.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝑄 ( 𝐷 Nat 𝐸 ) 𝑆 ) )
7	1 2 3 4 5 6	xpcfucco2	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ( ⟨ ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑃 , 𝑄 ⟩ ⟩ 𝑂 ⟨ 𝑅 , 𝑆 ⟩ ) ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ ( comp ‘ ( 𝐵 FuncCat 𝐶 ) ) 𝑅 ) 𝐹 ) , ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐸 ) ) 𝑆 ) 𝐺 ) ⟩ )
8		eqid	⊢ ( 𝐵 FuncCat 𝐶 ) = ( 𝐵 FuncCat 𝐶 )
9		eqid	⊢ ( 𝐵 Nat 𝐶 ) = ( 𝐵 Nat 𝐶 )
10		eqid	⊢ ( comp ‘ ( 𝐵 FuncCat 𝐶 ) ) = ( comp ‘ ( 𝐵 FuncCat 𝐶 ) )
11	8 9 10 3 5	fuccocl	⊢ ( 𝜑 → ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ ( comp ‘ ( 𝐵 FuncCat 𝐶 ) ) 𝑅 ) 𝐹 ) ∈ ( 𝑀 ( 𝐵 Nat 𝐶 ) 𝑅 ) )
12		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
13		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
14		eqid	⊢ ( comp ‘ ( 𝐷 FuncCat 𝐸 ) ) = ( comp ‘ ( 𝐷 FuncCat 𝐸 ) )
15	12 13 14 4 6	fuccocl	⊢ ( 𝜑 → ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐸 ) ) 𝑆 ) 𝐺 ) ∈ ( 𝑁 ( 𝐷 Nat 𝐸 ) 𝑆 ) )
16	11 15	opelxpd	⊢ ( 𝜑 → ⟨ ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ ( comp ‘ ( 𝐵 FuncCat 𝐶 ) ) 𝑅 ) 𝐹 ) , ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐸 ) ) 𝑆 ) 𝐺 ) ⟩ ∈ ( ( 𝑀 ( 𝐵 Nat 𝐶 ) 𝑅 ) × ( 𝑁 ( 𝐷 Nat 𝐸 ) 𝑆 ) ) )
17	7 16	eqeltrd	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ( ⟨ ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑃 , 𝑄 ⟩ ⟩ 𝑂 ⟨ 𝑅 , 𝑆 ⟩ ) ⟨ 𝐹 , 𝐺 ⟩ ) ∈ ( ( 𝑀 ( 𝐵 Nat 𝐶 ) 𝑅 ) × ( 𝑁 ( 𝐷 Nat 𝐸 ) 𝑆 ) ) )