curfval

Description: Value of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	curfval.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
	curfval.a	$⊢ A = {Base}_{C}$
	curfval.c	$⊢ φ \to C \in Cat$
	curfval.d	$⊢ φ \to D \in Cat$
	curfval.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
	curfval.b	$⊢ B = {Base}_{D}$
	curfval.j	$⊢ J = Hom (D)$
	curfval.1	$⊢ \underset{˙}{1} = Id (C)$
	curfval.h	$⊢ H = Hom (C)$
	curfval.i	$⊢ I = Id (D)$
Assertion	curfval	$⊢ φ \to G = ⟨(x \in A ⟼ ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩), (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))))⟩$

Proof

Step	Hyp	Ref	Expression
1		curfval.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
2		curfval.a	$⊢ A = {Base}_{C}$
3		curfval.c	$⊢ φ \to C \in Cat$
4		curfval.d	$⊢ φ \to D \in Cat$
5		curfval.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
6		curfval.b	$⊢ B = {Base}_{D}$
7		curfval.j	$⊢ J = Hom (D)$
8		curfval.1	$⊢ \underset{˙}{1} = Id (C)$
9		curfval.h	$⊢ H = Hom (C)$
10		curfval.i	$⊢ I = Id (D)$
11		df-curf	$⊢ {curry}_{F} = (e \in V, f \in V ⟼ ⦋ 1^{st} (e) / c ⦌ ⦋ 2^{nd} (e) / d ⦌ ⟨(x \in {Base}_{c} ⟼ ⟨(y \in {Base}_{d} ⟼ x 1^{st} (f) y), (y \in {Base}_{d}, z \in {Base}_{d} ⟼ (g \in (y Hom (d) z) ⟼ Id (c) (x) (⟨x, y⟩ 2^{nd} (f) ⟨x, z⟩) g))⟩), (x \in {Base}_{c}, y \in {Base}_{c} ⟼ (g \in (x Hom (c) y) ⟼ (z \in {Base}_{d} ⟼ g (⟨x, z⟩ 2^{nd} (f) ⟨y, z⟩) Id (d) (z))))⟩)$
12	11	a1i	$⊢ φ \to {curry}_{F} = (e \in V, f \in V ⟼ ⦋ 1^{st} (e) / c ⦌ ⦋ 2^{nd} (e) / d ⦌ ⟨(x \in {Base}_{c} ⟼ ⟨(y \in {Base}_{d} ⟼ x 1^{st} (f) y), (y \in {Base}_{d}, z \in {Base}_{d} ⟼ (g \in (y Hom (d) z) ⟼ Id (c) (x) (⟨x, y⟩ 2^{nd} (f) ⟨x, z⟩) g))⟩), (x \in {Base}_{c}, y \in {Base}_{c} ⟼ (g \in (x Hom (c) y) ⟼ (z \in {Base}_{d} ⟼ g (⟨x, z⟩ 2^{nd} (f) ⟨y, z⟩) Id (d) (z))))⟩)$
13		fvexd	$⊢ (φ \land (e = ⟨C, D⟩ \land f = F)) \to 1^{st} (e) \in V$
14		simprl	$⊢ (φ \land (e = ⟨C, D⟩ \land f = F)) \to e = ⟨C, D⟩$
15	14	fveq2d	$⊢ (φ \land (e = ⟨C, D⟩ \land f = F)) \to 1^{st} (e) = 1^{st} (⟨C, D⟩)$
16		op1stg	$⊢ (C \in Cat \land D \in Cat) \to 1^{st} (⟨C, D⟩) = C$
17	3 4 16	syl2anc	$⊢ φ \to 1^{st} (⟨C, D⟩) = C$
18	17	adantr	$⊢ (φ \land (e = ⟨C, D⟩ \land f = F)) \to 1^{st} (⟨C, D⟩) = C$
19	15 18	eqtrd	$⊢ (φ \land (e = ⟨C, D⟩ \land f = F)) \to 1^{st} (e) = C$
20		fvexd	$⊢ ((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \to 2^{nd} (e) \in V$
21	14	adantr	$⊢ ((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \to e = ⟨C, D⟩$
22	21	fveq2d	$⊢ ((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \to 2^{nd} (e) = 2^{nd} (⟨C, D⟩)$
23		op2ndg	$⊢ (C \in Cat \land D \in Cat) \to 2^{nd} (⟨C, D⟩) = D$
24	3 4 23	syl2anc	$⊢ φ \to 2^{nd} (⟨C, D⟩) = D$
25	24	ad2antrr	$⊢ ((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \to 2^{nd} (⟨C, D⟩) = D$
26	22 25	eqtrd	$⊢ ((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \to 2^{nd} (e) = D$
27		simplr	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to c = C$
28	27	fveq2d	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to {Base}_{c} = {Base}_{C}$
29	28 2	eqtr4di	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to {Base}_{c} = A$
30		simpr	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to d = D$
31	30	fveq2d	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to {Base}_{d} = {Base}_{D}$
32	31 6	eqtr4di	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to {Base}_{d} = B$
33		simprr	$⊢ (φ \land (e = ⟨C, D⟩ \land f = F)) \to f = F$
34	33	ad2antrr	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to f = F$
35	34	fveq2d	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to 1^{st} (f) = 1^{st} (F)$
36	35	oveqd	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to x 1^{st} (f) y = x 1^{st} (F) y$
37	32 36	mpteq12dv	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to (y \in {Base}_{d} ⟼ x 1^{st} (f) y) = (y \in B ⟼ x 1^{st} (F) y)$
38	30	fveq2d	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to Hom (d) = Hom (D)$
39	38 7	eqtr4di	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to Hom (d) = J$
40	39	oveqd	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to y Hom (d) z = y J z$
41	34	fveq2d	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to 2^{nd} (f) = 2^{nd} (F)$
42	41	oveqd	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to ⟨x, y⟩ 2^{nd} (f) ⟨x, z⟩ = ⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩$
43	27	fveq2d	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to Id (c) = Id (C)$
44	43 8	eqtr4di	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to Id (c) = \underset{˙}{1}$
45	44	fveq1d	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to Id (c) (x) = \underset{˙}{1} (x)$
46		eqidd	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to g = g$
47	42 45 46	oveq123d	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to Id (c) (x) (⟨x, y⟩ 2^{nd} (f) ⟨x, z⟩) g = \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g$
48	40 47	mpteq12dv	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to (g \in (y Hom (d) z) ⟼ Id (c) (x) (⟨x, y⟩ 2^{nd} (f) ⟨x, z⟩) g) = (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g)$
49	32 32 48	mpoeq123dv	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to (y \in {Base}_{d}, z \in {Base}_{d} ⟼ (g \in (y Hom (d) z) ⟼ Id (c) (x) (⟨x, y⟩ 2^{nd} (f) ⟨x, z⟩) g)) = (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))$
50	37 49	opeq12d	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to ⟨(y \in {Base}_{d} ⟼ x 1^{st} (f) y), (y \in {Base}_{d}, z \in {Base}_{d} ⟼ (g \in (y Hom (d) z) ⟼ Id (c) (x) (⟨x, y⟩ 2^{nd} (f) ⟨x, z⟩) g))⟩ = ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩$
51	29 50	mpteq12dv	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to (x \in {Base}_{c} ⟼ ⟨(y \in {Base}_{d} ⟼ x 1^{st} (f) y), (y \in {Base}_{d}, z \in {Base}_{d} ⟼ (g \in (y Hom (d) z) ⟼ Id (c) (x) (⟨x, y⟩ 2^{nd} (f) ⟨x, z⟩) g))⟩) = (x \in A ⟼ ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩)$
52	27	fveq2d	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to Hom (c) = Hom (C)$
53	52 9	eqtr4di	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to Hom (c) = H$
54	53	oveqd	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to x Hom (c) y = x H y$
55	41	oveqd	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to ⟨x, z⟩ 2^{nd} (f) ⟨y, z⟩ = ⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩$
56	30	fveq2d	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to Id (d) = Id (D)$
57	56 10	eqtr4di	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to Id (d) = I$
58	57	fveq1d	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to Id (d) (z) = I (z)$
59	55 46 58	oveq123d	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to g (⟨x, z⟩ 2^{nd} (f) ⟨y, z⟩) Id (d) (z) = g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z)$
60	32 59	mpteq12dv	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to (z \in {Base}_{d} ⟼ g (⟨x, z⟩ 2^{nd} (f) ⟨y, z⟩) Id (d) (z)) = (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))$
61	54 60	mpteq12dv	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to (g \in (x Hom (c) y) ⟼ (z \in {Base}_{d} ⟼ g (⟨x, z⟩ 2^{nd} (f) ⟨y, z⟩) Id (d) (z))) = (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z)))$
62	29 29 61	mpoeq123dv	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to (x \in {Base}_{c}, y \in {Base}_{c} ⟼ (g \in (x Hom (c) y) ⟼ (z \in {Base}_{d} ⟼ g (⟨x, z⟩ 2^{nd} (f) ⟨y, z⟩) Id (d) (z)))) = (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))))$
63	51 62	opeq12d	$⊢ (((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \land d = D) \to ⟨(x \in {Base}_{c} ⟼ ⟨(y \in {Base}_{d} ⟼ x 1^{st} (f) y), (y \in {Base}_{d}, z \in {Base}_{d} ⟼ (g \in (y Hom (d) z) ⟼ Id (c) (x) (⟨x, y⟩ 2^{nd} (f) ⟨x, z⟩) g))⟩), (x \in {Base}_{c}, y \in {Base}_{c} ⟼ (g \in (x Hom (c) y) ⟼ (z \in {Base}_{d} ⟼ g (⟨x, z⟩ 2^{nd} (f) ⟨y, z⟩) Id (d) (z))))⟩ = ⟨(x \in A ⟼ ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩), (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))))⟩$
64	20 26 63	csbied2	$⊢ ((φ \land (e = ⟨C, D⟩ \land f = F)) \land c = C) \to ⦋ 2^{nd} (e) / d ⦌ ⟨(x \in {Base}_{c} ⟼ ⟨(y \in {Base}_{d} ⟼ x 1^{st} (f) y), (y \in {Base}_{d}, z \in {Base}_{d} ⟼ (g \in (y Hom (d) z) ⟼ Id (c) (x) (⟨x, y⟩ 2^{nd} (f) ⟨x, z⟩) g))⟩), (x \in {Base}_{c}, y \in {Base}_{c} ⟼ (g \in (x Hom (c) y) ⟼ (z \in {Base}_{d} ⟼ g (⟨x, z⟩ 2^{nd} (f) ⟨y, z⟩) Id (d) (z))))⟩ = ⟨(x \in A ⟼ ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩), (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))))⟩$
65	13 19 64	csbied2	$⊢ (φ \land (e = ⟨C, D⟩ \land f = F)) \to ⦋ 1^{st} (e) / c ⦌ ⦋ 2^{nd} (e) / d ⦌ ⟨(x \in {Base}_{c} ⟼ ⟨(y \in {Base}_{d} ⟼ x 1^{st} (f) y), (y \in {Base}_{d}, z \in {Base}_{d} ⟼ (g \in (y Hom (d) z) ⟼ Id (c) (x) (⟨x, y⟩ 2^{nd} (f) ⟨x, z⟩) g))⟩), (x \in {Base}_{c}, y \in {Base}_{c} ⟼ (g \in (x Hom (c) y) ⟼ (z \in {Base}_{d} ⟼ g (⟨x, z⟩ 2^{nd} (f) ⟨y, z⟩) Id (d) (z))))⟩ = ⟨(x \in A ⟼ ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩), (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))))⟩$
66		opex	$⊢ ⟨C, D⟩ \in V$
67	66	a1i	$⊢ φ \to ⟨C, D⟩ \in V$
68	5	elexd	$⊢ φ \to F \in V$
69		opex	$⊢ ⟨(x \in A ⟼ ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩), (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))))⟩ \in V$
70	69	a1i	$⊢ φ \to ⟨(x \in A ⟼ ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩), (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))))⟩ \in V$
71	12 65 67 68 70	ovmpod	$⊢ φ \to ⟨C, D⟩ {curry}_{F} F = ⟨(x \in A ⟼ ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩), (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))))⟩$
72	1 71	syl5eq	$⊢ φ \to G = ⟨(x \in A ⟼ ⟨(y \in B ⟼ x 1^{st} (F) y), (y \in B, z \in B ⟼ (g \in (y J z) ⟼ \underset{˙}{1} (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g))⟩), (x \in A, y \in A ⟼ (g \in (x H y) ⟼ (z \in B ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) I (z))))⟩$

Metamath Proof Explorer

Theorem curfval

Proof