Metamath Proof Explorer

Theorem xpcfuchom2

Description: Value of the set of morphisms 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
xpcfuchom2.m ⊢ φ → M ∈ B Func C
xpcfuchom2.n ⊢ φ → N ∈ D Func E
xpcfuchom2.p ⊢ φ → P ∈ B Func C
xpcfuchom2.q ⊢ φ → Q ∈ D Func E
xpcfuchom2.k ⊢ K = Hom ⁡ T
Assertion xpcfuchom2 ⊢ φ → M N K P Q = M B Nat C P × N D Nat E Q

Proof

Step Hyp Ref Expression
1 xpcfuchom2.t ⊢ T = B FuncCat C × c D FuncCat E
2 xpcfuchom2.m ⊢ φ → M ∈ B Func C
3 xpcfuchom2.n ⊢ φ → N ∈ D Func E
4 xpcfuchom2.p ⊢ φ → P ∈ B Func C
5 xpcfuchom2.q ⊢ φ → Q ∈ D Func E
6 xpcfuchom2.k ⊢ K = Hom ⁡ T
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 1 8 10 12 14 2 3 4 5 6 xpchom2 ⊢ φ → M N K P Q = M B Nat C P × N D Nat E Q