Metamath Proof Explorer

Theorem funcf2

Description: The morphism part of a functor is a function on homsets. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses funcixp.b ${⊢}{B}={\mathrm{Base}}_{{D}}$
funcixp.h ${⊢}{H}=\mathrm{Hom}\left({D}\right)$
funcixp.j ${⊢}{J}=\mathrm{Hom}\left({E}\right)$
funcixp.f ${⊢}{\phi }\to {F}\left({D}\mathrm{Func}{E}\right){G}$
funcf2.x ${⊢}{\phi }\to {X}\in {B}$
funcf2.y ${⊢}{\phi }\to {Y}\in {B}$
Assertion funcf2 ${⊢}{\phi }\to \left({X}{G}{Y}\right):{X}{H}{Y}⟶{F}\left({X}\right){J}{F}\left({Y}\right)$

Proof

Step Hyp Ref Expression
1 funcixp.b ${⊢}{B}={\mathrm{Base}}_{{D}}$
2 funcixp.h ${⊢}{H}=\mathrm{Hom}\left({D}\right)$
3 funcixp.j ${⊢}{J}=\mathrm{Hom}\left({E}\right)$
4 funcixp.f ${⊢}{\phi }\to {F}\left({D}\mathrm{Func}{E}\right){G}$
5 funcf2.x ${⊢}{\phi }\to {X}\in {B}$
6 funcf2.y ${⊢}{\phi }\to {Y}\in {B}$
7 df-ov ${⊢}{X}{G}{Y}={G}\left(⟨{X},{Y}⟩\right)$
8 1 2 3 4 funcixp ${⊢}{\phi }\to {G}\in \underset{{z}\in {B}×{B}}{⨉}\left({\left({F}\left({1}^{st}\left({z}\right)\right){J}{F}\left({2}^{nd}\left({z}\right)\right)\right)}^{{H}\left({z}\right)}\right)$
9 5 6 opelxpd ${⊢}{\phi }\to ⟨{X},{Y}⟩\in \left({B}×{B}\right)$
10 2fveq3 ${⊢}{z}=⟨{X},{Y}⟩\to {F}\left({1}^{st}\left({z}\right)\right)={F}\left({1}^{st}\left(⟨{X},{Y}⟩\right)\right)$
11 2fveq3 ${⊢}{z}=⟨{X},{Y}⟩\to {F}\left({2}^{nd}\left({z}\right)\right)={F}\left({2}^{nd}\left(⟨{X},{Y}⟩\right)\right)$
12 10 11 oveq12d ${⊢}{z}=⟨{X},{Y}⟩\to {F}\left({1}^{st}\left({z}\right)\right){J}{F}\left({2}^{nd}\left({z}\right)\right)={F}\left({1}^{st}\left(⟨{X},{Y}⟩\right)\right){J}{F}\left({2}^{nd}\left(⟨{X},{Y}⟩\right)\right)$
13 fveq2 ${⊢}{z}=⟨{X},{Y}⟩\to {H}\left({z}\right)={H}\left(⟨{X},{Y}⟩\right)$
14 df-ov ${⊢}{X}{H}{Y}={H}\left(⟨{X},{Y}⟩\right)$
15 13 14 syl6eqr ${⊢}{z}=⟨{X},{Y}⟩\to {H}\left({z}\right)={X}{H}{Y}$
16 12 15 oveq12d ${⊢}{z}=⟨{X},{Y}⟩\to {\left({F}\left({1}^{st}\left({z}\right)\right){J}{F}\left({2}^{nd}\left({z}\right)\right)\right)}^{{H}\left({z}\right)}={\left({F}\left({1}^{st}\left(⟨{X},{Y}⟩\right)\right){J}{F}\left({2}^{nd}\left(⟨{X},{Y}⟩\right)\right)\right)}^{\left({X}{H}{Y}\right)}$
17 16 fvixp ${⊢}\left({G}\in \underset{{z}\in {B}×{B}}{⨉}\left({\left({F}\left({1}^{st}\left({z}\right)\right){J}{F}\left({2}^{nd}\left({z}\right)\right)\right)}^{{H}\left({z}\right)}\right)\wedge ⟨{X},{Y}⟩\in \left({B}×{B}\right)\right)\to {G}\left(⟨{X},{Y}⟩\right)\in \left({\left({F}\left({1}^{st}\left(⟨{X},{Y}⟩\right)\right){J}{F}\left({2}^{nd}\left(⟨{X},{Y}⟩\right)\right)\right)}^{\left({X}{H}{Y}\right)}\right)$
18 8 9 17 syl2anc ${⊢}{\phi }\to {G}\left(⟨{X},{Y}⟩\right)\in \left({\left({F}\left({1}^{st}\left(⟨{X},{Y}⟩\right)\right){J}{F}\left({2}^{nd}\left(⟨{X},{Y}⟩\right)\right)\right)}^{\left({X}{H}{Y}\right)}\right)$
19 7 18 eqeltrid ${⊢}{\phi }\to {X}{G}{Y}\in \left({\left({F}\left({1}^{st}\left(⟨{X},{Y}⟩\right)\right){J}{F}\left({2}^{nd}\left(⟨{X},{Y}⟩\right)\right)\right)}^{\left({X}{H}{Y}\right)}\right)$
20 op1stg ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {1}^{st}\left(⟨{X},{Y}⟩\right)={X}$
21 20 fveq2d ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {F}\left({1}^{st}\left(⟨{X},{Y}⟩\right)\right)={F}\left({X}\right)$
22 op2ndg ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {2}^{nd}\left(⟨{X},{Y}⟩\right)={Y}$
23 22 fveq2d ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {F}\left({2}^{nd}\left(⟨{X},{Y}⟩\right)\right)={F}\left({Y}\right)$
24 21 23 oveq12d ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {F}\left({1}^{st}\left(⟨{X},{Y}⟩\right)\right){J}{F}\left({2}^{nd}\left(⟨{X},{Y}⟩\right)\right)={F}\left({X}\right){J}{F}\left({Y}\right)$
25 5 6 24 syl2anc ${⊢}{\phi }\to {F}\left({1}^{st}\left(⟨{X},{Y}⟩\right)\right){J}{F}\left({2}^{nd}\left(⟨{X},{Y}⟩\right)\right)={F}\left({X}\right){J}{F}\left({Y}\right)$
26 25 oveq1d ${⊢}{\phi }\to {\left({F}\left({1}^{st}\left(⟨{X},{Y}⟩\right)\right){J}{F}\left({2}^{nd}\left(⟨{X},{Y}⟩\right)\right)\right)}^{\left({X}{H}{Y}\right)}={\left({F}\left({X}\right){J}{F}\left({Y}\right)\right)}^{\left({X}{H}{Y}\right)}$
27 19 26 eleqtrd ${⊢}{\phi }\to {X}{G}{Y}\in \left({\left({F}\left({X}\right){J}{F}\left({Y}\right)\right)}^{\left({X}{H}{Y}\right)}\right)$
28 elmapi ${⊢}{X}{G}{Y}\in \left({\left({F}\left({X}\right){J}{F}\left({Y}\right)\right)}^{\left({X}{H}{Y}\right)}\right)\to \left({X}{G}{Y}\right):{X}{H}{Y}⟶{F}\left({X}\right){J}{F}\left({Y}\right)$
29 27 28 syl ${⊢}{\phi }\to \left({X}{G}{Y}\right):{X}{H}{Y}⟶{F}\left({X}\right){J}{F}\left({Y}\right)$