Metamath Proof Explorer

Theorem xpcval

Description: Value of the binary product of categories. (Contributed by Mario Carneiro, 10-Jan-2017)

Ref Expression
Hypotheses xpcval.t ${⊢}{T}={C}{×}_{c}{D}$
xpcval.x ${⊢}{X}={\mathrm{Base}}_{{C}}$
xpcval.y ${⊢}{Y}={\mathrm{Base}}_{{D}}$
xpcval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
xpcval.j ${⊢}{J}=\mathrm{Hom}\left({D}\right)$
xpcval.o1
xpcval.o2
xpcval.c ${⊢}{\phi }\to {C}\in {V}$
xpcval.d ${⊢}{\phi }\to {D}\in {W}$
xpcval.b ${⊢}{\phi }\to {B}={X}×{Y}$
xpcval.k ${⊢}{\phi }\to {K}=\left({u}\in {B},{v}\in {B}⟼\left({1}^{st}\left({u}\right){H}{1}^{st}\left({v}\right)\right)×\left({2}^{nd}\left({u}\right){J}{2}^{nd}\left({v}\right)\right)\right)$
xpcval.o
Assertion xpcval ${⊢}{\phi }\to {T}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{K}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),{O}⟩\right\}$

Proof

Step Hyp Ref Expression
1 xpcval.t ${⊢}{T}={C}{×}_{c}{D}$
2 xpcval.x ${⊢}{X}={\mathrm{Base}}_{{C}}$
3 xpcval.y ${⊢}{Y}={\mathrm{Base}}_{{D}}$
4 xpcval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
5 xpcval.j ${⊢}{J}=\mathrm{Hom}\left({D}\right)$
6 xpcval.o1
7 xpcval.o2
8 xpcval.c ${⊢}{\phi }\to {C}\in {V}$
9 xpcval.d ${⊢}{\phi }\to {D}\in {W}$
10 xpcval.b ${⊢}{\phi }\to {B}={X}×{Y}$
11 xpcval.k ${⊢}{\phi }\to {K}=\left({u}\in {B},{v}\in {B}⟼\left({1}^{st}\left({u}\right){H}{1}^{st}\left({v}\right)\right)×\left({2}^{nd}\left({u}\right){J}{2}^{nd}\left({v}\right)\right)\right)$
12 xpcval.o
13 df-xpc
14 13 a1i
15 fvex ${⊢}{\mathrm{Base}}_{{r}}\in \mathrm{V}$
16 fvex ${⊢}{\mathrm{Base}}_{{s}}\in \mathrm{V}$
17 15 16 xpex ${⊢}{\mathrm{Base}}_{{r}}×{\mathrm{Base}}_{{s}}\in \mathrm{V}$
18 17 a1i ${⊢}\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\to {\mathrm{Base}}_{{r}}×{\mathrm{Base}}_{{s}}\in \mathrm{V}$
19 simprl ${⊢}\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\to {r}={C}$
20 19 fveq2d ${⊢}\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\to {\mathrm{Base}}_{{r}}={\mathrm{Base}}_{{C}}$
21 20 2 syl6eqr ${⊢}\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\to {\mathrm{Base}}_{{r}}={X}$
22 simprr ${⊢}\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\to {s}={D}$
23 22 fveq2d ${⊢}\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\to {\mathrm{Base}}_{{s}}={\mathrm{Base}}_{{D}}$
24 23 3 syl6eqr ${⊢}\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\to {\mathrm{Base}}_{{s}}={Y}$
25 21 24 xpeq12d ${⊢}\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\to {\mathrm{Base}}_{{r}}×{\mathrm{Base}}_{{s}}={X}×{Y}$
26 10 adantr ${⊢}\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\to {B}={X}×{Y}$
27 25 26 eqtr4d ${⊢}\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\to {\mathrm{Base}}_{{r}}×{\mathrm{Base}}_{{s}}={B}$
28 vex ${⊢}{b}\in \mathrm{V}$
29 28 28 mpoex ${⊢}\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)\in \mathrm{V}$
30 29 a1i ${⊢}\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\to \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)\in \mathrm{V}$
31 simpr ${⊢}\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\to {b}={B}$
32 simplrl ${⊢}\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\to {r}={C}$
33 32 fveq2d ${⊢}\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\to \mathrm{Hom}\left({r}\right)=\mathrm{Hom}\left({C}\right)$
34 33 4 syl6eqr ${⊢}\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\to \mathrm{Hom}\left({r}\right)={H}$
35 34 oveqd ${⊢}\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\to {1}^{st}\left({u}\right)\mathrm{Hom}\left({r}\right){1}^{st}\left({v}\right)={1}^{st}\left({u}\right){H}{1}^{st}\left({v}\right)$
36 simplrr ${⊢}\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\to {s}={D}$
37 36 fveq2d ${⊢}\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\to \mathrm{Hom}\left({s}\right)=\mathrm{Hom}\left({D}\right)$
38 37 5 syl6eqr ${⊢}\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\to \mathrm{Hom}\left({s}\right)={J}$
39 38 oveqd ${⊢}\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\to {2}^{nd}\left({u}\right)\mathrm{Hom}\left({s}\right){2}^{nd}\left({v}\right)={2}^{nd}\left({u}\right){J}{2}^{nd}\left({v}\right)$
40 35 39 xpeq12d ${⊢}\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\to \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)=\left({1}^{st}\left({u}\right){H}{1}^{st}\left({v}\right)\right)×\left({2}^{nd}\left({u}\right){J}{2}^{nd}\left({v}\right)\right)$
41 31 31 40 mpoeq123dv ${⊢}\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\to \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)=\left({u}\in {B},{v}\in {B}⟼\left({1}^{st}\left({u}\right){H}{1}^{st}\left({v}\right)\right)×\left({2}^{nd}\left({u}\right){J}{2}^{nd}\left({v}\right)\right)\right)$
42 11 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\to {K}=\left({u}\in {B},{v}\in {B}⟼\left({1}^{st}\left({u}\right){H}{1}^{st}\left({v}\right)\right)×\left({2}^{nd}\left({u}\right){J}{2}^{nd}\left({v}\right)\right)\right)$
43 41 42 eqtr4d ${⊢}\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\to \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)={K}$
44 simplr ${⊢}\left(\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\wedge {h}={K}\right)\to {b}={B}$
45 44 opeq2d ${⊢}\left(\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\wedge {h}={K}\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},{b}⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩$
46 simpr ${⊢}\left(\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\wedge {h}={K}\right)\to {h}={K}$
47 46 opeq2d ${⊢}\left(\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\wedge {h}={K}\right)\to ⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{h}⟩=⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{K}⟩$
48 44 44 xpeq12d ${⊢}\left(\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\wedge {h}={K}\right)\to {b}×{b}={B}×{B}$
49 46 oveqd ${⊢}\left(\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\wedge {h}={K}\right)\to {2}^{nd}\left({x}\right){h}{y}={2}^{nd}\left({x}\right){K}{y}$
50 46 fveq1d ${⊢}\left(\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\wedge {h}={K}\right)\to {h}\left({x}\right)={K}\left({x}\right)$
51 32 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\wedge {h}={K}\right)\to {r}={C}$
52 51 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\wedge {h}={K}\right)\to \mathrm{comp}\left({r}\right)=\mathrm{comp}\left({C}\right)$
53 52 6 syl6eqr
54 53 oveqd
55 54 oveqd
56 36 adantr ${⊢}\left(\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\wedge {h}={K}\right)\to {s}={D}$
57 56 fveq2d ${⊢}\left(\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\wedge {h}={K}\right)\to \mathrm{comp}\left({s}\right)=\mathrm{comp}\left({D}\right)$
58 57 7 syl6eqr
59 58 oveqd
60 59 oveqd
61 55 60 opeq12d
62 49 50 61 mpoeq123dv
63 48 44 62 mpoeq123dv
65 63 64 eqtr4d ${⊢}\left(\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\wedge {h}={K}\right)\to \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)={O}$
66 65 opeq2d ${⊢}\left(\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\wedge {h}={K}\right)\to ⟨\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)⟩=⟨\mathrm{comp}\left(\mathrm{ndx}\right),{O}⟩$
67 45 47 66 tpeq123d ${⊢}\left(\left(\left({\phi }\wedge \left({r}={C}\wedge {s}={D}\right)\right)\wedge {b}={B}\right)\wedge {h}={K}\right)\to \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\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{K}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),{O}⟩\right\}$
70 8 elexd ${⊢}{\phi }\to {C}\in \mathrm{V}$
71 9 elexd ${⊢}{\phi }\to {D}\in \mathrm{V}$
72 tpex ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{K}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),{O}⟩\right\}\in \mathrm{V}$
73 72 a1i ${⊢}{\phi }\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{K}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),{O}⟩\right\}\in \mathrm{V}$
74 14 69 70 71 73 ovmpod ${⊢}{\phi }\to {C}{×}_{c}{D}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{K}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),{O}⟩\right\}$
75 1 74 syl5eq ${⊢}{\phi }\to {T}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{B}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{K}⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),{O}⟩\right\}$