xpcfucco2

Description: Value of composition in the binary product of categories of functors. (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	xpcfucco2	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ( ⟨ ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑃 , 𝑄 ⟩ ⟩ 𝑂 ⟨ 𝑅 , 𝑆 ⟩ ) ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ ( comp ‘ ( 𝐵 FuncCat 𝐶 ) ) 𝑅 ) 𝐹 ) , ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐸 ) ) 𝑆 ) 𝐺 ) ⟩ )

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		eqid	⊢ ( 𝐵 FuncCat 𝐶 ) = ( 𝐵 FuncCat 𝐶 )
8	7	fucbas	⊢ ( 𝐵 Func 𝐶 ) = ( Base ‘ ( 𝐵 FuncCat 𝐶 ) )
9		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
10	9	fucbas	⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ ( 𝐷 FuncCat 𝐸 ) )
11		eqid	⊢ ( 𝐵 Nat 𝐶 ) = ( 𝐵 Nat 𝐶 )
12	7 11	fuchom	⊢ ( 𝐵 Nat 𝐶 ) = ( Hom ‘ ( 𝐵 FuncCat 𝐶 ) )
13		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
14	9 13	fuchom	⊢ ( 𝐷 Nat 𝐸 ) = ( Hom ‘ ( 𝐷 FuncCat 𝐸 ) )
15	11	natrcl	⊢ ( 𝐹 ∈ ( 𝑀 ( 𝐵 Nat 𝐶 ) 𝑃 ) → ( 𝑀 ∈ ( 𝐵 Func 𝐶 ) ∧ 𝑃 ∈ ( 𝐵 Func 𝐶 ) ) )
16	3 15	syl	⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝐵 Func 𝐶 ) ∧ 𝑃 ∈ ( 𝐵 Func 𝐶 ) ) )
17	16	simpld	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐵 Func 𝐶 ) )
18	13	natrcl	⊢ ( 𝐺 ∈ ( 𝑁 ( 𝐷 Nat 𝐸 ) 𝑄 ) → ( 𝑁 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑄 ∈ ( 𝐷 Func 𝐸 ) ) )
19	4 18	syl	⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑄 ∈ ( 𝐷 Func 𝐸 ) ) )
20	19	simpld	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐷 Func 𝐸 ) )
21	16	simprd	⊢ ( 𝜑 → 𝑃 ∈ ( 𝐵 Func 𝐶 ) )
22	19	simprd	⊢ ( 𝜑 → 𝑄 ∈ ( 𝐷 Func 𝐸 ) )
23		eqid	⊢ ( comp ‘ ( 𝐵 FuncCat 𝐶 ) ) = ( comp ‘ ( 𝐵 FuncCat 𝐶 ) )
24		eqid	⊢ ( comp ‘ ( 𝐷 FuncCat 𝐸 ) ) = ( comp ‘ ( 𝐷 FuncCat 𝐸 ) )
25	11	natrcl	⊢ ( 𝐾 ∈ ( 𝑃 ( 𝐵 Nat 𝐶 ) 𝑅 ) → ( 𝑃 ∈ ( 𝐵 Func 𝐶 ) ∧ 𝑅 ∈ ( 𝐵 Func 𝐶 ) ) )
26	5 25	syl	⊢ ( 𝜑 → ( 𝑃 ∈ ( 𝐵 Func 𝐶 ) ∧ 𝑅 ∈ ( 𝐵 Func 𝐶 ) ) )
27	26	simprd	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐵 Func 𝐶 ) )
28	13	natrcl	⊢ ( 𝐿 ∈ ( 𝑄 ( 𝐷 Nat 𝐸 ) 𝑆 ) → ( 𝑄 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑆 ∈ ( 𝐷 Func 𝐸 ) ) )
29	6 28	syl	⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑆 ∈ ( 𝐷 Func 𝐸 ) ) )
30	29	simprd	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐷 Func 𝐸 ) )
31	1 8 10 12 14 17 20 21 22 23 24 2 27 30 3 4 5 6	xpcco2	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ( ⟨ ⟨ 𝑀 , 𝑁 ⟩ , ⟨ 𝑃 , 𝑄 ⟩ ⟩ 𝑂 ⟨ 𝑅 , 𝑆 ⟩ ) ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( 𝐾 ( ⟨ 𝑀 , 𝑃 ⟩ ( comp ‘ ( 𝐵 FuncCat 𝐶 ) ) 𝑅 ) 𝐹 ) , ( 𝐿 ( ⟨ 𝑁 , 𝑄 ⟩ ( comp ‘ ( 𝐷 FuncCat 𝐸 ) ) 𝑆 ) 𝐺 ) ⟩ )

Metamath Proof Explorer

Theorem xpcfucco2

Proof