Metamath Proof Explorer

Theorem 2ndf1

Description: Value of the first projection on an object. (Contributed by Mario Carneiro, 11-Jan-2017)

Ref Expression
Hypotheses 1stfval.t ${⊢}{T}={C}{×}_{c}{D}$
1stfval.b ${⊢}{B}={\mathrm{Base}}_{{T}}$
1stfval.h ${⊢}{H}=\mathrm{Hom}\left({T}\right)$
1stfval.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
1stfval.d ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
2ndfval.p ${⊢}{Q}={C}{{2}^{nd}}_{F}{D}$
2ndf1.p ${⊢}{\phi }\to {R}\in {B}$
Assertion 2ndf1 ${⊢}{\phi }\to {1}^{st}\left({Q}\right)\left({R}\right)={2}^{nd}\left({R}\right)$

Proof

Step Hyp Ref Expression
1 1stfval.t ${⊢}{T}={C}{×}_{c}{D}$
2 1stfval.b ${⊢}{B}={\mathrm{Base}}_{{T}}$
3 1stfval.h ${⊢}{H}=\mathrm{Hom}\left({T}\right)$
4 1stfval.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
5 1stfval.d ${⊢}{\phi }\to {D}\in \mathrm{Cat}$
6 2ndfval.p ${⊢}{Q}={C}{{2}^{nd}}_{F}{D}$
7 2ndf1.p ${⊢}{\phi }\to {R}\in {B}$
8 1 2 3 4 5 6 2ndfval ${⊢}{\phi }\to {Q}=⟨{{2}^{nd}↾}_{{B}},\left({x}\in {B},{y}\in {B}⟼{{2}^{nd}↾}_{\left({x}{H}{y}\right)}\right)⟩$
9 fo2nd ${⊢}{2}^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$
10 fofun ${⊢}{2}^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to \mathrm{Fun}{2}^{nd}$
11 9 10 ax-mp ${⊢}\mathrm{Fun}{2}^{nd}$
12 2 fvexi ${⊢}{B}\in \mathrm{V}$
13 resfunexg ${⊢}\left(\mathrm{Fun}{2}^{nd}\wedge {B}\in \mathrm{V}\right)\to {{2}^{nd}↾}_{{B}}\in \mathrm{V}$
14 11 12 13 mp2an ${⊢}{{2}^{nd}↾}_{{B}}\in \mathrm{V}$
15 12 12 mpoex ${⊢}\left({x}\in {B},{y}\in {B}⟼{{2}^{nd}↾}_{\left({x}{H}{y}\right)}\right)\in \mathrm{V}$
16 14 15 op1std ${⊢}{Q}=⟨{{2}^{nd}↾}_{{B}},\left({x}\in {B},{y}\in {B}⟼{{2}^{nd}↾}_{\left({x}{H}{y}\right)}\right)⟩\to {1}^{st}\left({Q}\right)={{2}^{nd}↾}_{{B}}$
17 8 16 syl ${⊢}{\phi }\to {1}^{st}\left({Q}\right)={{2}^{nd}↾}_{{B}}$
18 17 fveq1d ${⊢}{\phi }\to {1}^{st}\left({Q}\right)\left({R}\right)=\left({{2}^{nd}↾}_{{B}}\right)\left({R}\right)$
19 7 fvresd ${⊢}{\phi }\to \left({{2}^{nd}↾}_{{B}}\right)\left({R}\right)={2}^{nd}\left({R}\right)$
20 18 19 eqtrd ${⊢}{\phi }\to {1}^{st}\left({Q}\right)\left({R}\right)={2}^{nd}\left({R}\right)$