Metamath Proof Explorer

Theorem 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 ⊢ T = B FuncCat C × c D FuncCat E
xpcfucco2.o ⊢ O = comp ⁡ T
xpcfucco2.f ⊢ φ → F ∈ M B Nat C P
xpcfucco2.g ⊢ φ → G ∈ N D Nat E Q
xpcfucco2.k ⊢ φ → K ∈ P B Nat C R
xpcfucco2.l ⊢ φ → L ∈ Q D Nat E S
Assertion xpcfucco2 ⊢ φ → 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

Proof

Step Hyp Ref Expression
1 xpcfuchom2.t ⊢ T = B FuncCat C × c D FuncCat E
2 xpcfucco2.o ⊢ O = comp ⁡ T
3 xpcfucco2.f ⊢ φ → F ∈ M B Nat C P
4 xpcfucco2.g ⊢ φ → G ∈ N D Nat E Q
5 xpcfucco2.k ⊢ φ → K ∈ P B Nat C R
6 xpcfucco2.l ⊢ φ → L ∈ Q D Nat E S
7 eqid ⊢ B FuncCat C = B FuncCat C
8 7 fucbas ⊢ B Func C = Base B FuncCat C
9 eqid ⊢ D FuncCat E = D FuncCat E
10 9 fucbas ⊢ D Func E = Base D FuncCat E
11 eqid ⊢ B Nat C = B Nat C
12 7 11 fuchom ⊢ B Nat C = Hom ⁡ B FuncCat C
13 eqid ⊢ D Nat E = D Nat E
14 9 13 fuchom ⊢ D Nat E = Hom ⁡ D FuncCat E
15 11 natrcl ⊢ F ∈ M B Nat C P → M ∈ B Func C ∧ P ∈ B Func C
16 3 15 syl ⊢ φ → M ∈ B Func C ∧ P ∈ B Func C
17 16 simpld ⊢ φ → M ∈ B Func C
18 13 natrcl ⊢ G ∈ N D Nat E Q → N ∈ D Func E ∧ Q ∈ D Func E
19 4 18 syl ⊢ φ → N ∈ D Func E ∧ Q ∈ D Func E
20 19 simpld ⊢ φ → N ∈ D Func E
21 16 simprd ⊢ φ → P ∈ B Func C
22 19 simprd ⊢ φ → Q ∈ D Func E
23 eqid ⊢ comp ⁡ B FuncCat C = comp ⁡ B FuncCat C
24 eqid ⊢ comp ⁡ D FuncCat E = comp ⁡ D FuncCat E
25 11 natrcl ⊢ K ∈ P B Nat C R → P ∈ B Func C ∧ R ∈ B Func C
26 5 25 syl ⊢ φ → P ∈ B Func C ∧ R ∈ B Func C
27 26 simprd ⊢ φ → R ∈ B Func C
28 13 natrcl ⊢ L ∈ Q D Nat E S → Q ∈ D Func E ∧ S ∈ D Func E
29 6 28 syl ⊢ φ → Q ∈ D Func E ∧ S ∈ D Func E
30 29 simprd ⊢ φ → S ∈ D Func E
31 1 8 10 12 14 17 20 21 22 23 24 2 27 30 3 4 5 6 xpcco2 ⊢ φ → 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