1stfval

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

	Ref	Expression
Hypotheses	1stfval.t	$⊢ T = C \times_{c} D$
	1stfval.b	$⊢ B = {Base}_{T}$
	1stfval.h	$⊢ H = Hom (T)$
	1stfval.c	$⊢ φ \to C \in Cat$
	1stfval.d	$⊢ φ \to D \in Cat$
	1stfval.p	$⊢ P = C {1^{st}}_{F} D$
Assertion	1stfval	$⊢ φ \to P = ⟨{1^{st} ↾}_{B}, (x \in B, y \in B ⟼ {1^{st} ↾}_{(x H y)})⟩$

Proof

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		fvex	$⊢ {Base}_{c} \in V$
8		fvex	$⊢ {Base}_{d} \in V$
9	7 8	xpex	$⊢ {Base}_{c} \times {Base}_{d} \in V$
10	9	a1i	$⊢ (c = C \land d = D) \to {Base}_{c} \times {Base}_{d} \in V$
11		simpl	$⊢ (c = C \land d = D) \to c = C$
12	11	fveq2d	$⊢ (c = C \land d = D) \to {Base}_{c} = {Base}_{C}$
13		simpr	$⊢ (c = C \land d = D) \to d = D$
14	13	fveq2d	$⊢ (c = C \land d = D) \to {Base}_{d} = {Base}_{D}$
15	12 14	xpeq12d	$⊢ (c = C \land d = D) \to {Base}_{c} \times {Base}_{d} = {Base}_{C} \times {Base}_{D}$
16		eqid	$⊢ {Base}_{C} = {Base}_{C}$
17		eqid	$⊢ {Base}_{D} = {Base}_{D}$
18	1 16 17	xpcbas	$⊢ {Base}_{C} \times {Base}_{D} = {Base}_{T}$
19	18 2	eqtr4i	$⊢ {Base}_{C} \times {Base}_{D} = B$
20	15 19	eqtrdi	$⊢ (c = C \land d = D) \to {Base}_{c} \times {Base}_{d} = B$
21		simpr	$⊢ ((c = C \land d = D) \land b = B) \to b = B$
22	21	reseq2d	$⊢ ((c = C \land d = D) \land b = B) \to {1^{st} ↾}_{b} = {1^{st} ↾}_{B}$
23		simpll	$⊢ ((c = C \land d = D) \land b = B) \to c = C$
24		simplr	$⊢ ((c = C \land d = D) \land b = B) \to d = D$
25	23 24	oveq12d	$⊢ ((c = C \land d = D) \land b = B) \to c \times_{c} d = C \times_{c} D$
26	25 1	eqtr4di	$⊢ ((c = C \land d = D) \land b = B) \to c \times_{c} d = T$
27	26	fveq2d	$⊢ ((c = C \land d = D) \land b = B) \to Hom (c \times_{c} d) = Hom (T)$
28	27 3	eqtr4di	$⊢ ((c = C \land d = D) \land b = B) \to Hom (c \times_{c} d) = H$
29	28	oveqd	$⊢ ((c = C \land d = D) \land b = B) \to x Hom (c \times_{c} d) y = x H y$
30	29	reseq2d	$⊢ ((c = C \land d = D) \land b = B) \to {1^{st} ↾}_{(x Hom (c \times_{c} d) y)} = {1^{st} ↾}_{(x H y)}$
31	21 21 30	mpoeq123dv	$⊢ ((c = C \land d = D) \land b = B) \to (x \in b, y \in b ⟼ {1^{st} ↾}_{(x Hom (c \times_{c} d) y)}) = (x \in B, y \in B ⟼ {1^{st} ↾}_{(x H y)})$
32	22 31	opeq12d	$⊢ ((c = C \land d = D) \land b = B) \to ⟨{1^{st} ↾}_{b}, (x \in b, y \in b ⟼ {1^{st} ↾}_{(x Hom (c \times_{c} d) y)})⟩ = ⟨{1^{st} ↾}_{B}, (x \in B, y \in B ⟼ {1^{st} ↾}_{(x H y)})⟩$
33	10 20 32	csbied2	$⊢ (c = C \land d = D) \to ⦋ ({Base}_{c} \times {Base}_{d}) / b ⦌ ⟨{1^{st} ↾}_{b}, (x \in b, y \in b ⟼ {1^{st} ↾}_{(x Hom (c \times_{c} d) y)})⟩ = ⟨{1^{st} ↾}_{B}, (x \in B, y \in B ⟼ {1^{st} ↾}_{(x H y)})⟩$
34		df-1stf	$⊢ {1^{st}}_{F} = (c \in Cat, d \in Cat ⟼ ⦋ ({Base}_{c} \times {Base}_{d}) / b ⦌ ⟨{1^{st} ↾}_{b}, (x \in b, y \in b ⟼ {1^{st} ↾}_{(x Hom (c \times_{c} d) y)})⟩)$
35		opex	$⊢ ⟨{1^{st} ↾}_{B}, (x \in B, y \in B ⟼ {1^{st} ↾}_{(x H y)})⟩ \in V$
36	33 34 35	ovmpoa	$⊢ (C \in Cat \land D \in Cat) \to C {1^{st}}_{F} D = ⟨{1^{st} ↾}_{B}, (x \in B, y \in B ⟼ {1^{st} ↾}_{(x H y)})⟩$
37	4 5 36	syl2anc	$⊢ φ \to C {1^{st}}_{F} D = ⟨{1^{st} ↾}_{B}, (x \in B, y \in B ⟼ {1^{st} ↾}_{(x H y)})⟩$
38	6 37	eqtrid	$⊢ φ \to P = ⟨{1^{st} ↾}_{B}, (x \in B, y \in B ⟼ {1^{st} ↾}_{(x H y)})⟩$

Metamath Proof Explorer

Theorem 1stfval

Proof