2ndf2

Description: Value of the first projection on a morphism. (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		2ndf2.p	$⊢ φ \to S \in B$
9	1 2 3 4 5 6	2ndfval	$⊢ φ \to Q = ⟨{2^{nd} ↾}_{B}, (x \in B, y \in B ⟼ {2^{nd} ↾}_{(x H y)})⟩$
10		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
11		fofun	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to Fun 2^{nd}$
12	10 11	ax-mp	$⊢ Fun 2^{nd}$
13	2	fvexi	$⊢ B \in V$
14		resfunexg	$⊢ (Fun 2^{nd} \land B \in V) \to {2^{nd} ↾}_{B} \in V$
15	12 13 14	mp2an	$⊢ {2^{nd} ↾}_{B} \in V$
16	13 13	mpoex	$⊢ (x \in B, y \in B ⟼ {2^{nd} ↾}_{(x H y)}) \in V$
17	15 16	op2ndd	$⊢ Q = ⟨{2^{nd} ↾}_{B}, (x \in B, y \in B ⟼ {2^{nd} ↾}_{(x H y)})⟩ \to 2^{nd} (Q) = (x \in B, y \in B ⟼ {2^{nd} ↾}_{(x H y)})$
18	9 17	syl	$⊢ φ \to 2^{nd} (Q) = (x \in B, y \in B ⟼ {2^{nd} ↾}_{(x H y)})$
19		simprl	$⊢ (φ \land (x = R \land y = S)) \to x = R$
20		simprr	$⊢ (φ \land (x = R \land y = S)) \to y = S$
21	19 20	oveq12d	$⊢ (φ \land (x = R \land y = S)) \to x H y = R H S$
22	21	reseq2d	$⊢ (φ \land (x = R \land y = S)) \to {2^{nd} ↾}_{(x H y)} = {2^{nd} ↾}_{(R H S)}$
23		ovex	$⊢ R H S \in V$
24		resfunexg	$⊢ (Fun 2^{nd} \land R H S \in V) \to {2^{nd} ↾}_{(R H S)} \in V$
25	12 23 24	mp2an	$⊢ {2^{nd} ↾}_{(R H S)} \in V$
26	25	a1i	$⊢ φ \to {2^{nd} ↾}_{(R H S)} \in V$
27	18 22 7 8 26	ovmpod	$⊢ φ \to R 2^{nd} (Q) S = {2^{nd} ↾}_{(R H S)}$

Metamath Proof Explorer