# Metamath Proof Explorer

## Theorem xpcco

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

Ref Expression
Hypotheses xpccofval.t ${⊢}{T}={C}{×}_{c}{D}$
xpccofval.b ${⊢}{B}={\mathrm{Base}}_{{T}}$
xpccofval.k ${⊢}{K}=\mathrm{Hom}\left({T}\right)$
xpccofval.o1
xpccofval.o2
xpccofval.o ${⊢}{O}=\mathrm{comp}\left({T}\right)$
xpcco.x ${⊢}{\phi }\to {X}\in {B}$
xpcco.y ${⊢}{\phi }\to {Y}\in {B}$
xpcco.z ${⊢}{\phi }\to {Z}\in {B}$
xpcco.f ${⊢}{\phi }\to {F}\in \left({X}{K}{Y}\right)$
xpcco.g ${⊢}{\phi }\to {G}\in \left({Y}{K}{Z}\right)$
Assertion xpcco

### Proof

Step Hyp Ref Expression
1 xpccofval.t ${⊢}{T}={C}{×}_{c}{D}$
2 xpccofval.b ${⊢}{B}={\mathrm{Base}}_{{T}}$
3 xpccofval.k ${⊢}{K}=\mathrm{Hom}\left({T}\right)$
4 xpccofval.o1
5 xpccofval.o2
6 xpccofval.o ${⊢}{O}=\mathrm{comp}\left({T}\right)$
7 xpcco.x ${⊢}{\phi }\to {X}\in {B}$
8 xpcco.y ${⊢}{\phi }\to {Y}\in {B}$
9 xpcco.z ${⊢}{\phi }\to {Z}\in {B}$
10 xpcco.f ${⊢}{\phi }\to {F}\in \left({X}{K}{Y}\right)$
11 xpcco.g ${⊢}{\phi }\to {G}\in \left({Y}{K}{Z}\right)$
12 1 2 3 4 5 6 xpccofval
13 7 8 opelxpd ${⊢}{\phi }\to ⟨{X},{Y}⟩\in \left({B}×{B}\right)$
14 9 adantr ${⊢}\left({\phi }\wedge {x}=⟨{X},{Y}⟩\right)\to {Z}\in {B}$
15 ovex ${⊢}{2}^{nd}\left({x}\right){K}{y}\in \mathrm{V}$
16 fvex ${⊢}{K}\left({x}\right)\in \mathrm{V}$
17 15 16 mpoex
18 17 a1i
19 11 adantr ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {G}\in \left({Y}{K}{Z}\right)$
20 simprl ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {x}=⟨{X},{Y}⟩$
21 20 fveq2d ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {2}^{nd}\left({x}\right)={2}^{nd}\left(⟨{X},{Y}⟩\right)$
22 op2ndg ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {2}^{nd}\left(⟨{X},{Y}⟩\right)={Y}$
23 7 8 22 syl2anc ${⊢}{\phi }\to {2}^{nd}\left(⟨{X},{Y}⟩\right)={Y}$
24 23 adantr ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {2}^{nd}\left(⟨{X},{Y}⟩\right)={Y}$
25 21 24 eqtrd ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {2}^{nd}\left({x}\right)={Y}$
26 simprr ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {y}={Z}$
27 25 26 oveq12d ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {2}^{nd}\left({x}\right){K}{y}={Y}{K}{Z}$
28 19 27 eleqtrrd ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {G}\in \left({2}^{nd}\left({x}\right){K}{y}\right)$
29 10 adantr ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {F}\in \left({X}{K}{Y}\right)$
30 20 fveq2d ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {K}\left({x}\right)={K}\left(⟨{X},{Y}⟩\right)$
31 df-ov ${⊢}{X}{K}{Y}={K}\left(⟨{X},{Y}⟩\right)$
32 30 31 syl6eqr ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {K}\left({x}\right)={X}{K}{Y}$
33 29 32 eleqtrrd ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {F}\in {K}\left({x}\right)$
34 33 adantr ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge {g}={G}\right)\to {F}\in {K}\left({x}\right)$
35 opex
36 35 a1i
37 20 fveq2d ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {1}^{st}\left({x}\right)={1}^{st}\left(⟨{X},{Y}⟩\right)$
38 op1stg ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {1}^{st}\left(⟨{X},{Y}⟩\right)={X}$
39 7 8 38 syl2anc ${⊢}{\phi }\to {1}^{st}\left(⟨{X},{Y}⟩\right)={X}$
40 39 adantr ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {1}^{st}\left(⟨{X},{Y}⟩\right)={X}$
41 37 40 eqtrd ${⊢}\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\to {1}^{st}\left({x}\right)={X}$
42 41 adantr ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {1}^{st}\left({x}\right)={X}$
43 42 fveq2d ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {1}^{st}\left({1}^{st}\left({x}\right)\right)={1}^{st}\left({X}\right)$
44 25 adantr ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {2}^{nd}\left({x}\right)={Y}$
45 44 fveq2d ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {1}^{st}\left({2}^{nd}\left({x}\right)\right)={1}^{st}\left({Y}\right)$
46 43 45 opeq12d ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to ⟨{1}^{st}\left({1}^{st}\left({x}\right)\right),{1}^{st}\left({2}^{nd}\left({x}\right)\right)⟩=⟨{1}^{st}\left({X}\right),{1}^{st}\left({Y}\right)⟩$
47 simplrr ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {y}={Z}$
48 47 fveq2d ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {1}^{st}\left({y}\right)={1}^{st}\left({Z}\right)$
49 46 48 oveq12d
50 simprl ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {g}={G}$
51 50 fveq2d ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {1}^{st}\left({g}\right)={1}^{st}\left({G}\right)$
52 simprr ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {f}={F}$
53 52 fveq2d ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {1}^{st}\left({f}\right)={1}^{st}\left({F}\right)$
54 49 51 53 oveq123d
55 42 fveq2d ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {2}^{nd}\left({1}^{st}\left({x}\right)\right)={2}^{nd}\left({X}\right)$
56 44 fveq2d ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {2}^{nd}\left({2}^{nd}\left({x}\right)\right)={2}^{nd}\left({Y}\right)$
57 55 56 opeq12d ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to ⟨{2}^{nd}\left({1}^{st}\left({x}\right)\right),{2}^{nd}\left({2}^{nd}\left({x}\right)\right)⟩=⟨{2}^{nd}\left({X}\right),{2}^{nd}\left({Y}\right)⟩$
58 47 fveq2d ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {2}^{nd}\left({y}\right)={2}^{nd}\left({Z}\right)$
59 57 58 oveq12d
60 50 fveq2d ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {2}^{nd}\left({g}\right)={2}^{nd}\left({G}\right)$
61 52 fveq2d ${⊢}\left(\left({\phi }\wedge \left({x}=⟨{X},{Y}⟩\wedge {y}={Z}\right)\right)\wedge \left({g}={G}\wedge {f}={F}\right)\right)\to {2}^{nd}\left({f}\right)={2}^{nd}\left({F}\right)$
62 59 60 61 oveq123d
63 54 62 opeq12d
64 28 34 36 63 ovmpodv2
65 13 14 18 64 ovmpodv
66 12 65 mpi