uncf1

Description: Value of the uncurry functor on an object. (Contributed by Mario Carneiro, 13-Jan-2017)

	Ref	Expression
Hypotheses	uncfval.g	$⊢ F = ⟨“ C D E ”⟩ {uncurry}_{F} G$
	uncfval.c	$⊢ φ \to D \in Cat$
	uncfval.d	$⊢ φ \to E \in Cat$
	uncfval.f	$⊢ φ \to G \in (C Func (D FuncCat E))$
	uncf1.a	$⊢ A = {Base}_{C}$
	uncf1.b	$⊢ B = {Base}_{D}$
	uncf1.x	$⊢ φ \to X \in A$
	uncf1.y	$⊢ φ \to Y \in B$
Assertion	uncf1	$⊢ φ \to X 1^{st} (F) Y = 1^{st} (1^{st} (G) (X)) (Y)$

Proof

Step	Hyp	Ref	Expression
1		uncfval.g	$⊢ F = ⟨“ C D E ”⟩ {uncurry}_{F} G$
2		uncfval.c	$⊢ φ \to D \in Cat$
3		uncfval.d	$⊢ φ \to E \in Cat$
4		uncfval.f	$⊢ φ \to G \in (C Func (D FuncCat E))$
5		uncf1.a	$⊢ A = {Base}_{C}$
6		uncf1.b	$⊢ B = {Base}_{D}$
7		uncf1.x	$⊢ φ \to X \in A$
8		uncf1.y	$⊢ φ \to Y \in B$
9	1 2 3 4	uncfval	$⊢ φ \to F = (D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))$
10	9	fveq2d	$⊢ φ \to 1^{st} (F) = 1^{st} ((D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)))$
11	10	oveqd	$⊢ φ \to X 1^{st} (F) Y = X 1^{st} ((D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))) Y$
12		df-ov	$⊢ X 1^{st} ((D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))) Y = 1^{st} ((D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))) (⟨X, Y⟩)$
13		eqid	$⊢ C \times_{c} D = C \times_{c} D$
14	13 5 6	xpcbas	$⊢ A \times B = {Base}_{(C \times_{c} D)}$
15		eqid	$⊢ (G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D) = (G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)$
16		eqid	$⊢ (D FuncCat E) \times_{c} D = (D FuncCat E) \times_{c} D$
17		funcrcl	$⊢ G \in (C Func (D FuncCat E)) \to (C \in Cat \land D FuncCat E \in Cat)$
18	4 17	syl	$⊢ φ \to (C \in Cat \land D FuncCat E \in Cat)$
19	18	simpld	$⊢ φ \to C \in Cat$
20		eqid	$⊢ C {1^{st}}_{F} D = C {1^{st}}_{F} D$
21	13 19 2 20	1stfcl	$⊢ φ \to C {1^{st}}_{F} D \in ((C \times_{c} D) Func C)$
22	21 4	cofucl	$⊢ φ \to G \circ_{func} (C {1^{st}}_{F} D) \in ((C \times_{c} D) Func (D FuncCat E))$
23		eqid	$⊢ C {2^{nd}}_{F} D = C {2^{nd}}_{F} D$
24	13 19 2 23	2ndfcl	$⊢ φ \to C {2^{nd}}_{F} D \in ((C \times_{c} D) Func D)$
25	15 16 22 24	prfcl	$⊢ φ \to (G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D) \in ((C \times_{c} D) Func ((D FuncCat E) \times_{c} D))$
26		eqid	$⊢ D {eval}_{F} E = D {eval}_{F} E$
27		eqid	$⊢ D FuncCat E = D FuncCat E$
28	26 27 2 3	evlfcl	$⊢ φ \to D {eval}_{F} E \in (((D FuncCat E) \times_{c} D) Func E)$
29	7 8	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (A \times B)$
30	14 25 28 29	cofu1	$⊢ φ \to 1^{st} ((D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))) (⟨X, Y⟩) = 1^{st} (D {eval}_{F} E) (1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨X, Y⟩))$
31	12 30	syl5eq	$⊢ φ \to X 1^{st} ((D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))) Y = 1^{st} (D {eval}_{F} E) (1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨X, Y⟩))$
32		eqid	$⊢ Hom (C \times_{c} D) = Hom (C \times_{c} D)$
33	15 14 32 22 24 29	prf1	$⊢ φ \to 1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨X, Y⟩) = ⟨1^{st} (G \circ_{func} (C {1^{st}}_{F} D)) (⟨X, Y⟩), 1^{st} (C {2^{nd}}_{F} D) (⟨X, Y⟩)⟩$
34	14 21 4 29	cofu1	$⊢ φ \to 1^{st} (G \circ_{func} (C {1^{st}}_{F} D)) (⟨X, Y⟩) = 1^{st} (G) (1^{st} (C {1^{st}}_{F} D) (⟨X, Y⟩))$
35	13 14 32 19 2 20 29	1stf1	$⊢ φ \to 1^{st} (C {1^{st}}_{F} D) (⟨X, Y⟩) = 1^{st} (⟨X, Y⟩)$
36		op1stg	$⊢ (X \in A \land Y \in B) \to 1^{st} (⟨X, Y⟩) = X$
37	7 8 36	syl2anc	$⊢ φ \to 1^{st} (⟨X, Y⟩) = X$
38	35 37	eqtrd	$⊢ φ \to 1^{st} (C {1^{st}}_{F} D) (⟨X, Y⟩) = X$
39	38	fveq2d	$⊢ φ \to 1^{st} (G) (1^{st} (C {1^{st}}_{F} D) (⟨X, Y⟩)) = 1^{st} (G) (X)$
40	34 39	eqtrd	$⊢ φ \to 1^{st} (G \circ_{func} (C {1^{st}}_{F} D)) (⟨X, Y⟩) = 1^{st} (G) (X)$
41	13 14 32 19 2 23 29	2ndf1	$⊢ φ \to 1^{st} (C {2^{nd}}_{F} D) (⟨X, Y⟩) = 2^{nd} (⟨X, Y⟩)$
42		op2ndg	$⊢ (X \in A \land Y \in B) \to 2^{nd} (⟨X, Y⟩) = Y$
43	7 8 42	syl2anc	$⊢ φ \to 2^{nd} (⟨X, Y⟩) = Y$
44	41 43	eqtrd	$⊢ φ \to 1^{st} (C {2^{nd}}_{F} D) (⟨X, Y⟩) = Y$
45	40 44	opeq12d	$⊢ φ \to ⟨1^{st} (G \circ_{func} (C {1^{st}}_{F} D)) (⟨X, Y⟩), 1^{st} (C {2^{nd}}_{F} D) (⟨X, Y⟩)⟩ = ⟨1^{st} (G) (X), Y⟩$
46	33 45	eqtrd	$⊢ φ \to 1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨X, Y⟩) = ⟨1^{st} (G) (X), Y⟩$
47	46	fveq2d	$⊢ φ \to 1^{st} (D {eval}_{F} E) (1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨X, Y⟩)) = 1^{st} (D {eval}_{F} E) (⟨1^{st} (G) (X), Y⟩)$
48		df-ov	$⊢ 1^{st} (G) (X) 1^{st} (D {eval}_{F} E) Y = 1^{st} (D {eval}_{F} E) (⟨1^{st} (G) (X), Y⟩)$
49	47 48	eqtr4di	$⊢ φ \to 1^{st} (D {eval}_{F} E) (1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨X, Y⟩)) = 1^{st} (G) (X) 1^{st} (D {eval}_{F} E) Y$
50	27	fucbas	$⊢ D Func E = {Base}_{(D FuncCat E)}$
51		relfunc	$⊢ Rel (C Func (D FuncCat E))$
52		1st2ndbr	$⊢ (Rel (C Func (D FuncCat E)) \land G \in (C Func (D FuncCat E))) \to 1^{st} (G) (C Func (D FuncCat E)) 2^{nd} (G)$
53	51 4 52	sylancr	$⊢ φ \to 1^{st} (G) (C Func (D FuncCat E)) 2^{nd} (G)$
54	5 50 53	funcf1	$⊢ φ \to 1^{st} (G) : A ⟶ D Func E$
55	54 7	ffvelrnd	$⊢ φ \to 1^{st} (G) (X) \in (D Func E)$
56	26 2 3 6 55 8	evlf1	$⊢ φ \to 1^{st} (G) (X) 1^{st} (D {eval}_{F} E) Y = 1^{st} (1^{st} (G) (X)) (Y)$
57	49 56	eqtrd	$⊢ φ \to 1^{st} (D {eval}_{F} E) (1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨X, Y⟩)) = 1^{st} (1^{st} (G) (X)) (Y)$
58	11 31 57	3eqtrd	$⊢ φ \to X 1^{st} (F) Y = 1^{st} (1^{st} (G) (X)) (Y)$

Metamath Proof Explorer

Theorem uncf1

Proof