# Metamath Proof Explorer

## Theorem funcco

Description: A functor maps composition in the source category to composition in the target. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses funcco.b ${⊢}{B}={\mathrm{Base}}_{{D}}$
funcco.h ${⊢}{H}=\mathrm{Hom}\left({D}\right)$
funcco.o
funcco.O ${⊢}{O}=\mathrm{comp}\left({E}\right)$
funcco.f ${⊢}{\phi }\to {F}\left({D}\mathrm{Func}{E}\right){G}$
funcco.x ${⊢}{\phi }\to {X}\in {B}$
funcco.y ${⊢}{\phi }\to {Y}\in {B}$
funcco.z ${⊢}{\phi }\to {Z}\in {B}$
funcco.m ${⊢}{\phi }\to {M}\in \left({X}{H}{Y}\right)$
funcco.n ${⊢}{\phi }\to {N}\in \left({Y}{H}{Z}\right)$
Assertion funcco

### Proof

Step Hyp Ref Expression
1 funcco.b ${⊢}{B}={\mathrm{Base}}_{{D}}$
2 funcco.h ${⊢}{H}=\mathrm{Hom}\left({D}\right)$
3 funcco.o
4 funcco.O ${⊢}{O}=\mathrm{comp}\left({E}\right)$
5 funcco.f ${⊢}{\phi }\to {F}\left({D}\mathrm{Func}{E}\right){G}$
6 funcco.x ${⊢}{\phi }\to {X}\in {B}$
7 funcco.y ${⊢}{\phi }\to {Y}\in {B}$
8 funcco.z ${⊢}{\phi }\to {Z}\in {B}$
9 funcco.m ${⊢}{\phi }\to {M}\in \left({X}{H}{Y}\right)$
10 funcco.n ${⊢}{\phi }\to {N}\in \left({Y}{H}{Z}\right)$
11 eqid ${⊢}{\mathrm{Base}}_{{E}}={\mathrm{Base}}_{{E}}$
12 eqid ${⊢}\mathrm{Hom}\left({E}\right)=\mathrm{Hom}\left({E}\right)$
13 eqid ${⊢}\mathrm{Id}\left({D}\right)=\mathrm{Id}\left({D}\right)$
14 eqid ${⊢}\mathrm{Id}\left({E}\right)=\mathrm{Id}\left({E}\right)$
15 df-br ${⊢}{F}\left({D}\mathrm{Func}{E}\right){G}↔⟨{F},{G}⟩\in \left({D}\mathrm{Func}{E}\right)$
16 5 15 sylib ${⊢}{\phi }\to ⟨{F},{G}⟩\in \left({D}\mathrm{Func}{E}\right)$
17 funcrcl ${⊢}⟨{F},{G}⟩\in \left({D}\mathrm{Func}{E}\right)\to \left({D}\in \mathrm{Cat}\wedge {E}\in \mathrm{Cat}\right)$
18 16 17 syl ${⊢}{\phi }\to \left({D}\in \mathrm{Cat}\wedge {E}\in \mathrm{Cat}\right)$
19 18 simpld ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
20 18 simprd ${⊢}{\phi }\to {E}\in \mathrm{Cat}$
21 1 11 2 12 13 14 3 4 19 20 isfunc
22 5 21 mpbid
23 22 simp3d
24 7 adantr ${⊢}\left({\phi }\wedge {x}={X}\right)\to {Y}\in {B}$
25 8 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\to {Z}\in {B}$
26 9 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {M}\in \left({X}{H}{Y}\right)$
27 simpllr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {x}={X}$
28 simplr ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {y}={Y}$
29 27 28 oveq12d ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {x}{H}{y}={X}{H}{Y}$
30 26 29 eleqtrrd ${⊢}\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\to {M}\in \left({x}{H}{y}\right)$
31 10 ad4antr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\to {N}\in \left({Y}{H}{Z}\right)$
32 simpllr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\to {y}={Y}$
33 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\to {z}={Z}$
34 32 33 oveq12d ${⊢}\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\to {y}{H}{z}={Y}{H}{Z}$
35 31 34 eleqtrrd ${⊢}\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\to {N}\in \left({y}{H}{z}\right)$
36 simp-5r ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to {x}={X}$
37 simpllr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to {z}={Z}$
38 36 37 oveq12d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to {x}{G}{z}={X}{G}{Z}$
39 simp-4r ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to {y}={Y}$
40 36 39 opeq12d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to ⟨{x},{y}⟩=⟨{X},{Y}⟩$
41 40 37 oveq12d
42 simpr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to {n}={N}$
43 simplr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to {m}={M}$
44 41 42 43 oveq123d
45 38 44 fveq12d
46 36 fveq2d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to {F}\left({x}\right)={F}\left({X}\right)$
47 39 fveq2d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to {F}\left({y}\right)={F}\left({Y}\right)$
48 46 47 opeq12d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to ⟨{F}\left({x}\right),{F}\left({y}\right)⟩=⟨{F}\left({X}\right),{F}\left({Y}\right)⟩$
49 37 fveq2d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to {F}\left({z}\right)={F}\left({Z}\right)$
50 48 49 oveq12d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to ⟨{F}\left({x}\right),{F}\left({y}\right)⟩{O}{F}\left({z}\right)=⟨{F}\left({X}\right),{F}\left({Y}\right)⟩{O}{F}\left({Z}\right)$
51 39 37 oveq12d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to {y}{G}{z}={Y}{G}{Z}$
52 51 42 fveq12d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to \left({y}{G}{z}\right)\left({n}\right)=\left({Y}{G}{Z}\right)\left({N}\right)$
53 36 39 oveq12d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to {x}{G}{y}={X}{G}{Y}$
54 53 43 fveq12d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to \left({x}{G}{y}\right)\left({m}\right)=\left({X}{G}{Y}\right)\left({M}\right)$
55 50 52 54 oveq123d ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}={X}\right)\wedge {y}={Y}\right)\wedge {z}={Z}\right)\wedge {m}={M}\right)\wedge {n}={N}\right)\to \left({y}{G}{z}\right)\left({n}\right)\left(⟨{F}\left({x}\right),{F}\left({y}\right)⟩{O}{F}\left({z}\right)\right)\left({x}{G}{y}\right)\left({m}\right)=\left({Y}{G}{Z}\right)\left({N}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩{O}{F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({M}\right)$
56 45 55 eqeq12d
57 35 56 rspcdv
58 30 57 rspcimdv
59 25 58 rspcimdv
60 24 59 rspcimdv