2ndf1

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

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

Metamath Proof Explorer