1stf2

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		1stfval.p	$⊢ P = C {1^{st}}_{F} D$
7		1stf1.p	$⊢ φ \to R \in B$
8		1stf2.p	$⊢ φ \to S \in B$
9	1 2 3 4 5 6	1stfval	$⊢ φ \to P = ⟨{1^{st} ↾}_{B}, (x \in B, y \in B ⟼ {1^{st} ↾}_{(x H y)})⟩$
10		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
11		fofun	$⊢ 1^{st} : V \underset{onto}{⟶} V \to Fun 1^{st}$
12	10 11	ax-mp	$⊢ Fun 1^{st}$
13	2	fvexi	$⊢ B \in V$
14		resfunexg	$⊢ (Fun 1^{st} \land B \in V) \to {1^{st} ↾}_{B} \in V$
15	12 13 14	mp2an	$⊢ {1^{st} ↾}_{B} \in V$
16	13 13	mpoex	$⊢ (x \in B, y \in B ⟼ {1^{st} ↾}_{(x H y)}) \in V$
17	15 16	op2ndd	$⊢ P = ⟨{1^{st} ↾}_{B}, (x \in B, y \in B ⟼ {1^{st} ↾}_{(x H y)})⟩ \to 2^{nd} (P) = (x \in B, y \in B ⟼ {1^{st} ↾}_{(x H y)})$
18	9 17	syl	$⊢ φ \to 2^{nd} (P) = (x \in B, y \in B ⟼ {1^{st} ↾}_{(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 {1^{st} ↾}_{(x H y)} = {1^{st} ↾}_{(R H S)}$
23		ovex	$⊢ R H S \in V$
24		resfunexg	$⊢ (Fun 1^{st} \land R H S \in V) \to {1^{st} ↾}_{(R H S)} \in V$
25	12 23 24	mp2an	$⊢ {1^{st} ↾}_{(R H S)} \in V$
26	25	a1i	$⊢ φ \to {1^{st} ↾}_{(R H S)} \in V$
27	18 22 7 8 26	ovmpod	$⊢ φ \to R 2^{nd} (P) S = {1^{st} ↾}_{(R H S)}$

Metamath Proof Explorer