Metamath Proof Explorer

Definition df-xpc

Description: Define the binary product of categories, which has objects for each pair of objects of the factors, and morphisms for each pair of morphisms of the factors. Composition is componentwise. (Contributed by Mario Carneiro, 10-Jan-2017)

Ref Expression
Assertion df-xpc

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxpc ${class}{×}_{c}$
1 vr ${setvar}{r}$
2 cvv ${class}\mathrm{V}$
3 vs ${setvar}{s}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{r}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{r}}$
7 3 cv ${setvar}{s}$
8 7 4 cfv ${class}{\mathrm{Base}}_{{s}}$
9 6 8 cxp ${class}\left({\mathrm{Base}}_{{r}}×{\mathrm{Base}}_{{s}}\right)$
10 vb ${setvar}{b}$
11 vu ${setvar}{u}$
12 10 cv ${setvar}{b}$
13 vv ${setvar}{v}$
14 c1st ${class}{1}^{st}$
15 11 cv ${setvar}{u}$
16 15 14 cfv ${class}{1}^{st}\left({u}\right)$
17 chom ${class}\mathrm{Hom}$
18 5 17 cfv ${class}\mathrm{Hom}\left({r}\right)$
19 13 cv ${setvar}{v}$
20 19 14 cfv ${class}{1}^{st}\left({v}\right)$
21 16 20 18 co ${class}\left({1}^{st}\left({u}\right)\mathrm{Hom}\left({r}\right){1}^{st}\left({v}\right)\right)$
22 c2nd ${class}{2}^{nd}$
23 15 22 cfv ${class}{2}^{nd}\left({u}\right)$
24 7 17 cfv ${class}\mathrm{Hom}\left({s}\right)$
25 19 22 cfv ${class}{2}^{nd}\left({v}\right)$
26 23 25 24 co ${class}\left({2}^{nd}\left({u}\right)\mathrm{Hom}\left({s}\right){2}^{nd}\left({v}\right)\right)$
27 21 26 cxp ${class}\left(\left({1}^{st}\left({u}\right)\mathrm{Hom}\left({r}\right){1}^{st}\left({v}\right)\right)×\left({2}^{nd}\left({u}\right)\mathrm{Hom}\left({s}\right){2}^{nd}\left({v}\right)\right)\right)$
28 11 13 12 12 27 cmpo ${class}\left({u}\in {b},{v}\in {b}⟼\left({1}^{st}\left({u}\right)\mathrm{Hom}\left({r}\right){1}^{st}\left({v}\right)\right)×\left({2}^{nd}\left({u}\right)\mathrm{Hom}\left({s}\right){2}^{nd}\left({v}\right)\right)\right)$
29 vh ${setvar}{h}$
30 cnx ${class}\mathrm{ndx}$
31 30 4 cfv ${class}{\mathrm{Base}}_{\mathrm{ndx}}$
32 31 12 cop ${class}⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩$
33 30 17 cfv ${class}\mathrm{Hom}\left(\mathrm{ndx}\right)$
34 29 cv ${setvar}{h}$
35 33 34 cop ${class}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{h}⟩$
36 cco ${class}\mathrm{comp}$
37 30 36 cfv ${class}\mathrm{comp}\left(\mathrm{ndx}\right)$
38 vx ${setvar}{x}$
39 12 12 cxp ${class}\left({b}×{b}\right)$
40 vy ${setvar}{y}$
41 vg ${setvar}{g}$
42 38 cv ${setvar}{x}$
43 42 22 cfv ${class}{2}^{nd}\left({x}\right)$
44 40 cv ${setvar}{y}$
45 43 44 34 co ${class}\left({2}^{nd}\left({x}\right){h}{y}\right)$
46 vf ${setvar}{f}$
47 42 34 cfv ${class}{h}\left({x}\right)$
48 41 cv ${setvar}{g}$
49 48 14 cfv ${class}{1}^{st}\left({g}\right)$
50 42 14 cfv ${class}{1}^{st}\left({x}\right)$
51 50 14 cfv ${class}{1}^{st}\left({1}^{st}\left({x}\right)\right)$
52 43 14 cfv ${class}{1}^{st}\left({2}^{nd}\left({x}\right)\right)$
53 51 52 cop ${class}⟨{1}^{st}\left({1}^{st}\left({x}\right)\right),{1}^{st}\left({2}^{nd}\left({x}\right)\right)⟩$
54 5 36 cfv ${class}\mathrm{comp}\left({r}\right)$
55 44 14 cfv ${class}{1}^{st}\left({y}\right)$
56 53 55 54 co ${class}\left(⟨{1}^{st}\left({1}^{st}\left({x}\right)\right),{1}^{st}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({r}\right){1}^{st}\left({y}\right)\right)$
57 46 cv ${setvar}{f}$
58 57 14 cfv ${class}{1}^{st}\left({f}\right)$
59 49 58 56 co ${class}\left({1}^{st}\left({g}\right)\left(⟨{1}^{st}\left({1}^{st}\left({x}\right)\right),{1}^{st}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({r}\right){1}^{st}\left({y}\right)\right){1}^{st}\left({f}\right)\right)$
60 48 22 cfv ${class}{2}^{nd}\left({g}\right)$
61 50 22 cfv ${class}{2}^{nd}\left({1}^{st}\left({x}\right)\right)$
62 43 22 cfv ${class}{2}^{nd}\left({2}^{nd}\left({x}\right)\right)$
63 61 62 cop ${class}⟨{2}^{nd}\left({1}^{st}\left({x}\right)\right),{2}^{nd}\left({2}^{nd}\left({x}\right)\right)⟩$
64 7 36 cfv ${class}\mathrm{comp}\left({s}\right)$
65 44 22 cfv ${class}{2}^{nd}\left({y}\right)$
66 63 65 64 co ${class}\left(⟨{2}^{nd}\left({1}^{st}\left({x}\right)\right),{2}^{nd}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({s}\right){2}^{nd}\left({y}\right)\right)$
67 57 22 cfv ${class}{2}^{nd}\left({f}\right)$
68 60 67 66 co ${class}\left({2}^{nd}\left({g}\right)\left(⟨{2}^{nd}\left({1}^{st}\left({x}\right)\right),{2}^{nd}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({s}\right){2}^{nd}\left({y}\right)\right){2}^{nd}\left({f}\right)\right)$
69 59 68 cop ${class}⟨{1}^{st}\left({g}\right)\left(⟨{1}^{st}\left({1}^{st}\left({x}\right)\right),{1}^{st}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({r}\right){1}^{st}\left({y}\right)\right){1}^{st}\left({f}\right),{2}^{nd}\left({g}\right)\left(⟨{2}^{nd}\left({1}^{st}\left({x}\right)\right),{2}^{nd}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({s}\right){2}^{nd}\left({y}\right)\right){2}^{nd}\left({f}\right)⟩$
70 41 46 45 47 69 cmpo ${class}\left({g}\in \left({2}^{nd}\left({x}\right){h}{y}\right),{f}\in {h}\left({x}\right)⟼⟨{1}^{st}\left({g}\right)\left(⟨{1}^{st}\left({1}^{st}\left({x}\right)\right),{1}^{st}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({r}\right){1}^{st}\left({y}\right)\right){1}^{st}\left({f}\right),{2}^{nd}\left({g}\right)\left(⟨{2}^{nd}\left({1}^{st}\left({x}\right)\right),{2}^{nd}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({s}\right){2}^{nd}\left({y}\right)\right){2}^{nd}\left({f}\right)⟩\right)$
71 38 40 39 12 70 cmpo ${class}\left({x}\in \left({b}×{b}\right),{y}\in {b}⟼\left({g}\in \left({2}^{nd}\left({x}\right){h}{y}\right),{f}\in {h}\left({x}\right)⟼⟨{1}^{st}\left({g}\right)\left(⟨{1}^{st}\left({1}^{st}\left({x}\right)\right),{1}^{st}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({r}\right){1}^{st}\left({y}\right)\right){1}^{st}\left({f}\right),{2}^{nd}\left({g}\right)\left(⟨{2}^{nd}\left({1}^{st}\left({x}\right)\right),{2}^{nd}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({s}\right){2}^{nd}\left({y}\right)\right){2}^{nd}\left({f}\right)⟩\right)\right)$
72 37 71 cop ${class}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({x}\in \left({b}×{b}\right),{y}\in {b}⟼\left({g}\in \left({2}^{nd}\left({x}\right){h}{y}\right),{f}\in {h}\left({x}\right)⟼⟨{1}^{st}\left({g}\right)\left(⟨{1}^{st}\left({1}^{st}\left({x}\right)\right),{1}^{st}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({r}\right){1}^{st}\left({y}\right)\right){1}^{st}\left({f}\right),{2}^{nd}\left({g}\right)\left(⟨{2}^{nd}\left({1}^{st}\left({x}\right)\right),{2}^{nd}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({s}\right){2}^{nd}\left({y}\right)\right){2}^{nd}\left({f}\right)⟩\right)\right)⟩$
73 32 35 72 ctp ${class}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{h}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left({x}\in \left({b}×{b}\right),{y}\in {b}⟼\left({g}\in \left({2}^{nd}\left({x}\right){h}{y}\right),{f}\in {h}\left({x}\right)⟼⟨{1}^{st}\left({g}\right)\left(⟨{1}^{st}\left({1}^{st}\left({x}\right)\right),{1}^{st}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({r}\right){1}^{st}\left({y}\right)\right){1}^{st}\left({f}\right),{2}^{nd}\left({g}\right)\left(⟨{2}^{nd}\left({1}^{st}\left({x}\right)\right),{2}^{nd}\left({2}^{nd}\left({x}\right)\right)⟩\mathrm{comp}\left({s}\right){2}^{nd}\left({y}\right)\right){2}^{nd}\left({f}\right)⟩\right)\right)⟩\right\}$
74 29 28 73 csb
75 10 9 74 csb
76 1 3 2 2 75 cmpo
77 0 76 wceq