curfuncf

Description: Cancellation of curry with uncurry. (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))$
Assertion	curfuncf	$⊢ φ \to ⟨C, D⟩ {curry}_{F} F = G$

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	2	ad2antrr	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to D \in Cat$
6	3	ad2antrr	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to E \in Cat$
7	4	ad2antrr	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to G \in (C Func (D FuncCat E))$
8		eqid	$⊢ {Base}_{C} = {Base}_{C}$
9		eqid	$⊢ {Base}_{D} = {Base}_{D}$
10		simplr	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to x \in {Base}_{C}$
11		simpr	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to y \in {Base}_{D}$
12	1 5 6 7 8 9 10 11	uncf1	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to x 1^{st} (F) y = 1^{st} (1^{st} (G) (x)) (y)$
13	12	mpteq2dva	$⊢ (φ \land x \in {Base}_{C}) \to (y \in {Base}_{D} ⟼ x 1^{st} (F) y) = (y \in {Base}_{D} ⟼ 1^{st} (1^{st} (G) (x)) (y))$
14		eqid	$⊢ {Base}_{E} = {Base}_{E}$
15		relfunc	$⊢ Rel (D Func E)$
16		eqid	$⊢ D FuncCat E = D FuncCat E$
17	16	fucbas	$⊢ D Func E = {Base}_{(D FuncCat E)}$
18		relfunc	$⊢ Rel (C Func (D FuncCat E))$
19		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)$
20	18 4 19	sylancr	$⊢ φ \to 1^{st} (G) (C Func (D FuncCat E)) 2^{nd} (G)$
21	8 17 20	funcf1	$⊢ φ \to 1^{st} (G) : {Base}_{C} ⟶ D Func E$
22	21	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G) (x) \in (D Func E)$
23		1st2ndbr	$⊢ (Rel (D Func E) \land 1^{st} (G) (x) \in (D Func E)) \to 1^{st} (1^{st} (G) (x)) (D Func E) 2^{nd} (1^{st} (G) (x))$
24	15 22 23	sylancr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (1^{st} (G) (x)) (D Func E) 2^{nd} (1^{st} (G) (x))$
25	9 14 24	funcf1	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (1^{st} (G) (x)) : {Base}_{D} ⟶ {Base}_{E}$
26	25	feqmptd	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (1^{st} (G) (x)) = (y \in {Base}_{D} ⟼ 1^{st} (1^{st} (G) (x)) (y))$
27	13 26	eqtr4d	$⊢ (φ \land x \in {Base}_{C}) \to (y \in {Base}_{D} ⟼ x 1^{st} (F) y) = 1^{st} (1^{st} (G) (x))$
28	2	ad3antrrr	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to D \in Cat$
29	3	ad3antrrr	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to E \in Cat$
30	4	ad3antrrr	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to G \in (C Func (D FuncCat E))$
31		simpllr	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to x \in {Base}_{C}$
32		simplrl	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to y \in {Base}_{D}$
33		eqid	$⊢ Hom (C) = Hom (C)$
34		eqid	$⊢ Hom (D) = Hom (D)$
35		simprr	$⊢ ((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to z \in {Base}_{D}$
36	35	adantr	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to z \in {Base}_{D}$
37		eqid	$⊢ Id (C) = Id (C)$
38		funcrcl	$⊢ G \in (C Func (D FuncCat E)) \to (C \in Cat \land D FuncCat E \in Cat)$
39	4 38	syl	$⊢ φ \to (C \in Cat \land D FuncCat E \in Cat)$
40	39	simpld	$⊢ φ \to C \in Cat$
41	40	ad3antrrr	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to C \in Cat$
42	8 33 37 41 31	catidcl	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to Id (C) (x) \in (x Hom (C) x)$
43		simpr	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to g \in (y Hom (D) z)$
44	1 28 29 30 8 9 31 32 33 34 31 36 42 43	uncf2	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g = (x 2^{nd} (G) x) (Id (C) (x)) (z) (⟨1^{st} (1^{st} (G) (x)) (y), 1^{st} (1^{st} (G) (x)) (z)⟩ comp (E) 1^{st} (1^{st} (G) (x)) (z)) (y 2^{nd} (1^{st} (G) (x)) z) (g)$
45		eqid	$⊢ Id (D FuncCat E) = Id (D FuncCat E)$
46	20	ad3antrrr	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to 1^{st} (G) (C Func (D FuncCat E)) 2^{nd} (G)$
47	8 37 45 46 31	funcid	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to (x 2^{nd} (G) x) (Id (C) (x)) = Id (D FuncCat E) (1^{st} (G) (x))$
48		eqid	$⊢ Id (E) = Id (E)$
49	22	ad2antrr	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to 1^{st} (G) (x) \in (D Func E)$
50	16 45 48 49	fucid	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to Id (D FuncCat E) (1^{st} (G) (x)) = Id (E) \circ 1^{st} (1^{st} (G) (x))$
51	47 50	eqtrd	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to (x 2^{nd} (G) x) (Id (C) (x)) = Id (E) \circ 1^{st} (1^{st} (G) (x))$
52	51	fveq1d	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to (x 2^{nd} (G) x) (Id (C) (x)) (z) = (Id (E) \circ 1^{st} (1^{st} (G) (x))) (z)$
53	25	ad2antrr	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to 1^{st} (1^{st} (G) (x)) : {Base}_{D} ⟶ {Base}_{E}$
54		fvco3	$⊢ (1^{st} (1^{st} (G) (x)) : {Base}_{D} ⟶ {Base}_{E} \land z \in {Base}_{D}) \to (Id (E) \circ 1^{st} (1^{st} (G) (x))) (z) = Id (E) (1^{st} (1^{st} (G) (x)) (z))$
55	53 36 54	syl2anc	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to (Id (E) \circ 1^{st} (1^{st} (G) (x))) (z) = Id (E) (1^{st} (1^{st} (G) (x)) (z))$
56	52 55	eqtrd	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to (x 2^{nd} (G) x) (Id (C) (x)) (z) = Id (E) (1^{st} (1^{st} (G) (x)) (z))$
57	56	oveq1d	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to (x 2^{nd} (G) x) (Id (C) (x)) (z) (⟨1^{st} (1^{st} (G) (x)) (y), 1^{st} (1^{st} (G) (x)) (z)⟩ comp (E) 1^{st} (1^{st} (G) (x)) (z)) (y 2^{nd} (1^{st} (G) (x)) z) (g) = Id (E) (1^{st} (1^{st} (G) (x)) (z)) (⟨1^{st} (1^{st} (G) (x)) (y), 1^{st} (1^{st} (G) (x)) (z)⟩ comp (E) 1^{st} (1^{st} (G) (x)) (z)) (y 2^{nd} (1^{st} (G) (x)) z) (g)$
58		eqid	$⊢ Hom (E) = Hom (E)$
59	53 32	ffvelcdmd	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to 1^{st} (1^{st} (G) (x)) (y) \in {Base}_{E}$
60		eqid	$⊢ comp (E) = comp (E)$
61	53 36	ffvelcdmd	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to 1^{st} (1^{st} (G) (x)) (z) \in {Base}_{E}$
62	24	adantr	$⊢ ((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to 1^{st} (1^{st} (G) (x)) (D Func E) 2^{nd} (1^{st} (G) (x))$
63		simprl	$⊢ ((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to y \in {Base}_{D}$
64	9 34 58 62 63 35	funcf2	$⊢ ((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to (y 2^{nd} (1^{st} (G) (x)) z) : y Hom (D) z ⟶ 1^{st} (1^{st} (G) (x)) (y) Hom (E) 1^{st} (1^{st} (G) (x)) (z)$
65	64	ffvelcdmda	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to (y 2^{nd} (1^{st} (G) (x)) z) (g) \in (1^{st} (1^{st} (G) (x)) (y) Hom (E) 1^{st} (1^{st} (G) (x)) (z))$
66	14 58 48 29 59 60 61 65	catlid	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to Id (E) (1^{st} (1^{st} (G) (x)) (z)) (⟨1^{st} (1^{st} (G) (x)) (y), 1^{st} (1^{st} (G) (x)) (z)⟩ comp (E) 1^{st} (1^{st} (G) (x)) (z)) (y 2^{nd} (1^{st} (G) (x)) z) (g) = (y 2^{nd} (1^{st} (G) (x)) z) (g)$
67	44 57 66	3eqtrd	$⊢ (((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \land g \in (y Hom (D) z)) \to Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g = (y 2^{nd} (1^{st} (G) (x)) z) (g)$
68	67	mpteq2dva	$⊢ ((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to (g \in (y Hom (D) z) ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g) = (g \in (y Hom (D) z) ⟼ (y 2^{nd} (1^{st} (G) (x)) z) (g))$
69	64	feqmptd	$⊢ ((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to y 2^{nd} (1^{st} (G) (x)) z = (g \in (y Hom (D) z) ⟼ (y 2^{nd} (1^{st} (G) (x)) z) (g))$
70	68 69	eqtr4d	$⊢ ((φ \land x \in {Base}_{C}) \land (y \in {Base}_{D} \land z \in {Base}_{D})) \to (g \in (y Hom (D) z) ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g) = y 2^{nd} (1^{st} (G) (x)) z$
71	70	3impb	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D} \land z \in {Base}_{D}) \to (g \in (y Hom (D) z) ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, z⟩) g) = y 2^{nd} (1^{st} (G) (x)) z$
72	71	mpoeq3dva	$⊢ (φ \land x \in {Base}_{C}) \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 {Base}_{D}, z \in {Base}_{D} ⟼ y 2^{nd} (1^{st} (G) (x)) z)$
73	9 24	funcfn2	$⊢ (φ \land x \in {Base}_{C}) \to 2^{nd} (1^{st} (G) (x)) Fn ({Base}_{D} \times {Base}_{D})$
74		fnov	$⊢ 2^{nd} (1^{st} (G) (x)) Fn ({Base}_{D} \times {Base}_{D}) \leftrightarrow 2^{nd} (1^{st} (G) (x)) = (y \in {Base}_{D}, z \in {Base}_{D} ⟼ y 2^{nd} (1^{st} (G) (x)) z)$
75	73 74	sylib	$⊢ (φ \land x \in {Base}_{C}) \to 2^{nd} (1^{st} (G) (x)) = (y \in {Base}_{D}, z \in {Base}_{D} ⟼ y 2^{nd} (1^{st} (G) (x)) z)$
76	72 75	eqtr4d	$⊢ (φ \land x \in {Base}_{C}) \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)) = 2^{nd} (1^{st} (G) (x))$
77	27 76	opeq12d	$⊢ (φ \land x \in {Base}_{C}) \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))⟩ = ⟨1^{st} (1^{st} (G) (x)), 2^{nd} (1^{st} (G) (x))⟩$
78		1st2nd	$⊢ (Rel (D Func E) \land 1^{st} (G) (x) \in (D Func E)) \to 1^{st} (G) (x) = ⟨1^{st} (1^{st} (G) (x)), 2^{nd} (1^{st} (G) (x))⟩$
79	15 22 78	sylancr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G) (x) = ⟨1^{st} (1^{st} (G) (x)), 2^{nd} (1^{st} (G) (x))⟩$
80	77 79	eqtr4d	$⊢ (φ \land x \in {Base}_{C}) \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))⟩ = 1^{st} (G) (x)$
81	80	mpteq2dva	$⊢ φ \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} ⟼ 1^{st} (G) (x))$
82	21	feqmptd	$⊢ φ \to 1^{st} (G) = (x \in {Base}_{C} ⟼ 1^{st} (G) (x))$
83	81 82	eqtr4d	$⊢ φ \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))⟩) = 1^{st} (G)$
84	2	ad3antrrr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to D \in Cat$
85	3	ad3antrrr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to E \in Cat$
86	4	ad3antrrr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to G \in (C Func (D FuncCat E))$
87		simprl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \in {Base}_{C}$
88	87	ad2antrr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to x \in {Base}_{C}$
89		simpr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to z \in {Base}_{D}$
90		simprr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to y \in {Base}_{C}$
91	90	ad2antrr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to y \in {Base}_{C}$
92		simplr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to g \in (x Hom (C) y)$
93		eqid	$⊢ Id (D) = Id (D)$
94	9 34 93 84 89	catidcl	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to Id (D) (z) \in (z Hom (D) z)$
95	1 84 85 86 8 9 88 89 33 34 91 89 92 94	uncf2	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z) = (x 2^{nd} (G) y) (g) (z) (⟨1^{st} (1^{st} (G) (x)) (z), 1^{st} (1^{st} (G) (x)) (z)⟩ comp (E) 1^{st} (1^{st} (G) (y)) (z)) (z 2^{nd} (1^{st} (G) (x)) z) (Id (D) (z))$
96	22	adantrr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (G) (x) \in (D Func E)$
97	96	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to 1^{st} (G) (x) \in (D Func E)$
98	15 97 23	sylancr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to 1^{st} (1^{st} (G) (x)) (D Func E) 2^{nd} (1^{st} (G) (x))$
99	98	adantr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to 1^{st} (1^{st} (G) (x)) (D Func E) 2^{nd} (1^{st} (G) (x))$
100	9 93 48 99 89	funcid	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to (z 2^{nd} (1^{st} (G) (x)) z) (Id (D) (z)) = Id (E) (1^{st} (1^{st} (G) (x)) (z))$
101	100	oveq2d	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to (x 2^{nd} (G) y) (g) (z) (⟨1^{st} (1^{st} (G) (x)) (z), 1^{st} (1^{st} (G) (x)) (z)⟩ comp (E) 1^{st} (1^{st} (G) (y)) (z)) (z 2^{nd} (1^{st} (G) (x)) z) (Id (D) (z)) = (x 2^{nd} (G) y) (g) (z) (⟨1^{st} (1^{st} (G) (x)) (z), 1^{st} (1^{st} (G) (x)) (z)⟩ comp (E) 1^{st} (1^{st} (G) (y)) (z)) Id (E) (1^{st} (1^{st} (G) (x)) (z))$
102	9 14 98	funcf1	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to 1^{st} (1^{st} (G) (x)) : {Base}_{D} ⟶ {Base}_{E}$
103	102	ffvelcdmda	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to 1^{st} (1^{st} (G) (x)) (z) \in {Base}_{E}$
104	21	ffvelcdmda	$⊢ (φ \land y \in {Base}_{C}) \to 1^{st} (G) (y) \in (D Func E)$
105	104	adantrl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (G) (y) \in (D Func E)$
106	105	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to 1^{st} (G) (y) \in (D Func E)$
107		1st2ndbr	$⊢ (Rel (D Func E) \land 1^{st} (G) (y) \in (D Func E)) \to 1^{st} (1^{st} (G) (y)) (D Func E) 2^{nd} (1^{st} (G) (y))$
108	15 106 107	sylancr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to 1^{st} (1^{st} (G) (y)) (D Func E) 2^{nd} (1^{st} (G) (y))$
109	9 14 108	funcf1	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to 1^{st} (1^{st} (G) (y)) : {Base}_{D} ⟶ {Base}_{E}$
110	109	ffvelcdmda	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to 1^{st} (1^{st} (G) (y)) (z) \in {Base}_{E}$
111		eqid	$⊢ D Nat E = D Nat E$
112	16 111	fuchom	$⊢ D Nat E = Hom (D FuncCat E)$
113	20	ad3antrrr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to 1^{st} (G) (C Func (D FuncCat E)) 2^{nd} (G)$
114	8 33 112 113 88 91	funcf2	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to (x 2^{nd} (G) y) : x Hom (C) y ⟶ 1^{st} (G) (x) (D Nat E) 1^{st} (G) (y)$
115	114 92	ffvelcdmd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to (x 2^{nd} (G) y) (g) \in (1^{st} (G) (x) (D Nat E) 1^{st} (G) (y))$
116	111 115	nat1st2nd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to (x 2^{nd} (G) y) (g) \in (⟨1^{st} (1^{st} (G) (x)), 2^{nd} (1^{st} (G) (x))⟩ (D Nat E) ⟨1^{st} (1^{st} (G) (y)), 2^{nd} (1^{st} (G) (y))⟩)$
117	111 116 9 58 89	natcl	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to (x 2^{nd} (G) y) (g) (z) \in (1^{st} (1^{st} (G) (x)) (z) Hom (E) 1^{st} (1^{st} (G) (y)) (z))$
118	14 58 48 85 103 60 110 117	catrid	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to (x 2^{nd} (G) y) (g) (z) (⟨1^{st} (1^{st} (G) (x)) (z), 1^{st} (1^{st} (G) (x)) (z)⟩ comp (E) 1^{st} (1^{st} (G) (y)) (z)) Id (E) (1^{st} (1^{st} (G) (x)) (z)) = (x 2^{nd} (G) y) (g) (z)$
119	95 101 118	3eqtrd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \land z \in {Base}_{D}) \to g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z) = (x 2^{nd} (G) y) (g) (z)$
120	119	mpteq2dva	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z)) = (z \in {Base}_{D} ⟼ (x 2^{nd} (G) y) (g) (z))$
121	20	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (G) (C Func (D FuncCat E)) 2^{nd} (G)$
122	8 33 112 121 87 90	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (G) y) : x Hom (C) y ⟶ 1^{st} (G) (x) (D Nat E) 1^{st} (G) (y)$
123	122	ffvelcdmda	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to (x 2^{nd} (G) y) (g) \in (1^{st} (G) (x) (D Nat E) 1^{st} (G) (y))$
124	111 123	nat1st2nd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to (x 2^{nd} (G) y) (g) \in (⟨1^{st} (1^{st} (G) (x)), 2^{nd} (1^{st} (G) (x))⟩ (D Nat E) ⟨1^{st} (1^{st} (G) (y)), 2^{nd} (1^{st} (G) (y))⟩)$
125	111 124 9	natfn	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to (x 2^{nd} (G) y) (g) Fn {Base}_{D}$
126		dffn5	$⊢ (x 2^{nd} (G) y) (g) Fn {Base}_{D} \leftrightarrow (x 2^{nd} (G) y) (g) = (z \in {Base}_{D} ⟼ (x 2^{nd} (G) y) (g) (z))$
127	125 126	sylib	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to (x 2^{nd} (G) y) (g) = (z \in {Base}_{D} ⟼ (x 2^{nd} (G) y) (g) (z))$
128	120 127	eqtr4d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z)) = (x 2^{nd} (G) y) (g)$
129	128	mpteq2dva	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \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 Hom (C) y) ⟼ (x 2^{nd} (G) y) (g))$
130	122	feqmptd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x 2^{nd} (G) y = (g \in (x Hom (C) y) ⟼ (x 2^{nd} (G) y) (g))$
131	129 130	eqtr4d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (g \in (x Hom (C) y) ⟼ (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z))) = x 2^{nd} (G) y$
132	131	3impb	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to (g \in (x Hom (C) y) ⟼ (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z))) = x 2^{nd} (G) y$
133	132	mpoeq3dva	$⊢ φ \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 {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (G) y)$
134	8 20	funcfn2	$⊢ φ \to 2^{nd} (G) Fn ({Base}_{C} \times {Base}_{C})$
135		fnov	$⊢ 2^{nd} (G) Fn ({Base}_{C} \times {Base}_{C}) \leftrightarrow 2^{nd} (G) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (G) y)$
136	134 135	sylib	$⊢ φ \to 2^{nd} (G) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (G) y)$
137	133 136	eqtr4d	$⊢ φ \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)))) = 2^{nd} (G)$
138	83 137	opeq12d	$⊢ φ \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))))⟩ = ⟨1^{st} (G), 2^{nd} (G)⟩$
139		eqid	$⊢ ⟨C, D⟩ {curry}_{F} F = ⟨C, D⟩ {curry}_{F} F$
140	1 2 3 4	uncfcl	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
141	139 8 40 2 140 9 34 37 33 93	curfval	$⊢ φ \to ⟨C, D⟩ {curry}_{F} F = ⟨(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))))⟩$
142		1st2nd	$⊢ (Rel (C Func (D FuncCat E)) \land G \in (C Func (D FuncCat E))) \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
143	18 4 142	sylancr	$⊢ φ \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
144	138 141 143	3eqtr4d	$⊢ φ \to ⟨C, D⟩ {curry}_{F} F = G$

Metamath Proof Explorer

Theorem curfuncf

Proof