curfcl

Description: The curry functor of a functor F : C X. D --> E is a functor curryF ( F ) : C --> ( D --> E ) . (Contributed by Mario Carneiro, 13-Jan-2017)

	Ref	Expression
Hypotheses	curfcl.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
	curfcl.q	$⊢ Q = D FuncCat E$
	curfcl.c	$⊢ φ \to C \in Cat$
	curfcl.d	$⊢ φ \to D \in Cat$
	curfcl.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
Assertion	curfcl	$⊢ φ \to G \in (C Func Q)$

Proof

Step	Hyp	Ref	Expression
1		curfcl.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
2		curfcl.q	$⊢ Q = D FuncCat E$
3		curfcl.c	$⊢ φ \to C \in Cat$
4		curfcl.d	$⊢ φ \to D \in Cat$
5		curfcl.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7		eqid	$⊢ {Base}_{D} = {Base}_{D}$
8		eqid	$⊢ Hom (D) = Hom (D)$
9		eqid	$⊢ Id (C) = Id (C)$
10		eqid	$⊢ Hom (C) = Hom (C)$
11		eqid	$⊢ Id (D) = Id (D)$
12	1 6 3 4 5 7 8 9 10 11	curfval	$⊢ φ \to G = ⟨(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		fvex	$⊢ {Base}_{C} \in V$
14	13	mptex	$⊢ (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))⟩) \in V$
15	13 13	mpoex	$⊢ (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)))) \in V$
16	14 15	op1std	$⊢ G = ⟨(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))))⟩ \to 1^{st} (G) = (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))⟩)$
17	12 16	syl	$⊢ φ \to 1^{st} (G) = (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))⟩)$
18	14 15	op2ndd	$⊢ G = ⟨(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))))⟩ \to 2^{nd} (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))))$
19	12 18	syl	$⊢ φ \to 2^{nd} (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))))$
20	17 19	opeq12d	$⊢ φ \to ⟨1^{st} (G), 2^{nd} (G)⟩ = ⟨(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))))⟩$
21	12 20	eqtr4d	$⊢ φ \to G = ⟨1^{st} (G), 2^{nd} (G)⟩$
22	2	fucbas	$⊢ D Func E = {Base}_{Q}$
23		eqid	$⊢ D Nat E = D Nat E$
24	2 23	fuchom	$⊢ D Nat E = Hom (Q)$
25		eqid	$⊢ Id (Q) = Id (Q)$
26		eqid	$⊢ comp (C) = comp (C)$
27		eqid	$⊢ comp (Q) = comp (Q)$
28		funcrcl	$⊢ F \in ((C \times_{c} D) Func E) \to (C \times_{c} D \in Cat \land E \in Cat)$
29	5 28	syl	$⊢ φ \to (C \times_{c} D \in Cat \land E \in Cat)$
30	29	simprd	$⊢ φ \to E \in Cat$
31	2 4 30	fuccat	$⊢ φ \to Q \in Cat$
32		opex	$⊢ ⟨(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))⟩ \in V$
33	32	a1i	$⊢ (φ \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))⟩ \in V$
34	3	adantr	$⊢ (φ \land x \in {Base}_{C}) \to C \in Cat$
35	4	adantr	$⊢ (φ \land x \in {Base}_{C}) \to D \in Cat$
36	5	adantr	$⊢ (φ \land x \in {Base}_{C}) \to F \in ((C \times_{c} D) Func E)$
37		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
38		eqid	$⊢ 1^{st} (G) (x) = 1^{st} (G) (x)$
39	1 6 34 35 36 7 37 38	curf1cl	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G) (x) \in (D Func E)$
40	33 17 39	fmpt2d	$⊢ φ \to 1^{st} (G) : {Base}_{C} ⟶ D Func E$
41		eqid	$⊢ (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} ⟼ (g \in (x Hom (C) y) ⟼ (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z))))$
42		ovex	$⊢ x Hom (C) y \in V$
43	42	mptex	$⊢ (g \in (x Hom (C) y) ⟼ (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z))) \in V$
44	41 43	fnmpoi	$⊢ (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)))) Fn ({Base}_{C} \times {Base}_{C})$
45	19	fneq1d	$⊢ φ \to (2^{nd} (G) Fn ({Base}_{C} \times {Base}_{C}) \leftrightarrow (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)))) Fn ({Base}_{C} \times {Base}_{C}))$
46	44 45	mpbiri	$⊢ φ \to 2^{nd} (G) Fn ({Base}_{C} \times {Base}_{C})$
47		fvex	$⊢ {Base}_{D} \in V$
48	47	mptex	$⊢ (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z)) \in V$
49	48	a1i	$⊢ ((φ \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)) \in V$
50	19	oveqd	$⊢ φ \to x 2^{nd} (G) y = x (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)))) y$
51	41	ovmpt4g	$⊢ (x \in {Base}_{C} \land y \in {Base}_{C} \land (g \in (x Hom (C) y) ⟼ (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z))) \in V) \to x (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)))) y = (g \in (x Hom (C) y) ⟼ (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z)))$
52	43 51	mp3an3	$⊢ (x \in {Base}_{C} \land y \in {Base}_{C}) \to x (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)))) y = (g \in (x Hom (C) y) ⟼ (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z)))$
53	50 52	sylan9eq	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x 2^{nd} (G) y = (g \in (x Hom (C) y) ⟼ (z \in {Base}_{D} ⟼ g (⟨x, z⟩ 2^{nd} (F) ⟨y, z⟩) Id (D) (z)))$
54	3	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to C \in Cat$
55	4	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to D \in Cat$
56	5	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to F \in ((C \times_{c} D) Func E)$
57		simplrl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to x \in {Base}_{C}$
58		simplrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to y \in {Base}_{C}$
59		simpr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land g \in (x Hom (C) y)) \to g \in (x Hom (C) y)$
60		eqid	$⊢ (x 2^{nd} (G) y) (g) = (x 2^{nd} (G) y) (g)$
61	1 6 54 55 56 7 10 11 57 58 59 60 23	curf2cl	$⊢ ((φ \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))$
62	49 53 61	fmpt2d	$⊢ (φ \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)$
63		eqid	$⊢ C \times_{c} D = C \times_{c} D$
64	63 6 7	xpcbas	$⊢ {Base}_{C} \times {Base}_{D} = {Base}_{(C \times_{c} D)}$
65		eqid	$⊢ Id (C \times_{c} D) = Id (C \times_{c} D)$
66		eqid	$⊢ Id (E) = Id (E)$
67		relfunc	$⊢ Rel ((C \times_{c} D) Func E)$
68		1st2ndbr	$⊢ (Rel ((C \times_{c} D) Func E) \land F \in ((C \times_{c} D) Func E)) \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
69	67 5 68	sylancr	$⊢ φ \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
70	69	ad2antrr	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
71		opelxpi	$⊢ (x \in {Base}_{C} \land y \in {Base}_{D}) \to ⟨x, y⟩ \in ({Base}_{C} \times {Base}_{D})$
72	71	adantll	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to ⟨x, y⟩ \in ({Base}_{C} \times {Base}_{D})$
73	64 65 66 70 72	funcid	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to (⟨x, y⟩ 2^{nd} (F) ⟨x, y⟩) (Id (C \times_{c} D) (⟨x, y⟩)) = Id (E) (1^{st} (F) (⟨x, y⟩))$
74	3	ad2antrr	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to C \in Cat$
75	4	ad2antrr	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to D \in Cat$
76	37	adantr	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to x \in {Base}_{C}$
77		simpr	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to y \in {Base}_{D}$
78	63 74 75 6 7 9 11 65 76 77	xpcid	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to Id (C \times_{c} D) (⟨x, y⟩) = ⟨Id (C) (x), Id (D) (y)⟩$
79	78	fveq2d	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to (⟨x, y⟩ 2^{nd} (F) ⟨x, y⟩) (Id (C \times_{c} D) (⟨x, y⟩)) = (⟨x, y⟩ 2^{nd} (F) ⟨x, y⟩) (⟨Id (C) (x), Id (D) (y)⟩)$
80		df-ov	$⊢ Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, y⟩) Id (D) (y) = (⟨x, y⟩ 2^{nd} (F) ⟨x, y⟩) (⟨Id (C) (x), Id (D) (y)⟩)$
81	79 80	eqtr4di	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to (⟨x, y⟩ 2^{nd} (F) ⟨x, y⟩) (Id (C \times_{c} D) (⟨x, y⟩)) = Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, y⟩) Id (D) (y)$
82	5	ad2antrr	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to F \in ((C \times_{c} D) Func E)$
83	1 6 74 75 82 7 76 38 77	curf11	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to 1^{st} (1^{st} (G) (x)) (y) = x 1^{st} (F) y$
84		df-ov	$⊢ x 1^{st} (F) y = 1^{st} (F) (⟨x, y⟩)$
85	83 84	eqtr2di	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to 1^{st} (F) (⟨x, y⟩) = 1^{st} (1^{st} (G) (x)) (y)$
86	85	fveq2d	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to Id (E) (1^{st} (F) (⟨x, y⟩)) = Id (E) (1^{st} (1^{st} (G) (x)) (y))$
87	73 81 86	3eqtr3d	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, y⟩) Id (D) (y) = Id (E) (1^{st} (1^{st} (G) (x)) (y))$
88	87	mpteq2dva	$⊢ (φ \land x \in {Base}_{C}) \to (y \in {Base}_{D} ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, y⟩) Id (D) (y)) = (y \in {Base}_{D} ⟼ Id (E) (1^{st} (1^{st} (G) (x)) (y)))$
89	30	adantr	$⊢ (φ \land x \in {Base}_{C}) \to E \in Cat$
90		eqid	$⊢ {Base}_{E} = {Base}_{E}$
91	90 66	cidfn	$⊢ E \in Cat \to Id (E) Fn {Base}_{E}$
92	89 91	syl	$⊢ (φ \land x \in {Base}_{C}) \to Id (E) Fn {Base}_{E}$
93		dffn2	$⊢ Id (E) Fn {Base}_{E} \leftrightarrow Id (E) : {Base}_{E} ⟶ V$
94	92 93	sylib	$⊢ (φ \land x \in {Base}_{C}) \to Id (E) : {Base}_{E} ⟶ V$
95		relfunc	$⊢ Rel (D Func E)$
96		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))$
97	95 39 96	sylancr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (1^{st} (G) (x)) (D Func E) 2^{nd} (1^{st} (G) (x))$
98	7 90 97	funcf1	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (1^{st} (G) (x)) : {Base}_{D} ⟶ {Base}_{E}$
99		fcompt	$⊢ (Id (E) : {Base}_{E} ⟶ V \land 1^{st} (1^{st} (G) (x)) : {Base}_{D} ⟶ {Base}_{E}) \to Id (E) \circ 1^{st} (1^{st} (G) (x)) = (y \in {Base}_{D} ⟼ Id (E) (1^{st} (1^{st} (G) (x)) (y)))$
100	94 98 99	syl2anc	$⊢ (φ \land x \in {Base}_{C}) \to Id (E) \circ 1^{st} (1^{st} (G) (x)) = (y \in {Base}_{D} ⟼ Id (E) (1^{st} (1^{st} (G) (x)) (y)))$
101	88 100	eqtr4d	$⊢ (φ \land x \in {Base}_{C}) \to (y \in {Base}_{D} ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, y⟩) Id (D) (y)) = Id (E) \circ 1^{st} (1^{st} (G) (x))$
102	6 10 9 34 37	catidcl	$⊢ (φ \land x \in {Base}_{C}) \to Id (C) (x) \in (x Hom (C) x)$
103		eqid	$⊢ (x 2^{nd} (G) x) (Id (C) (x)) = (x 2^{nd} (G) x) (Id (C) (x))$
104	1 6 34 35 36 7 10 11 37 37 102 103	curf2	$⊢ (φ \land x \in {Base}_{C}) \to (x 2^{nd} (G) x) (Id (C) (x)) = (y \in {Base}_{D} ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, y⟩) Id (D) (y))$
105	2 25 66 39	fucid	$⊢ (φ \land x \in {Base}_{C}) \to Id (Q) (1^{st} (G) (x)) = Id (E) \circ 1^{st} (1^{st} (G) (x))$
106	101 104 105	3eqtr4d	$⊢ (φ \land x \in {Base}_{C}) \to (x 2^{nd} (G) x) (Id (C) (x)) = Id (Q) (1^{st} (G) (x))$
107	3	3ad2ant1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to C \in Cat$
108	107	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to C \in Cat$
109	4	3ad2ant1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to D \in Cat$
110	109	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to D \in Cat$
111	5	3ad2ant1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to F \in ((C \times_{c} D) Func E)$
112	111	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to F \in ((C \times_{c} D) Func E)$
113		simp21	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to x \in {Base}_{C}$
114	113	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to x \in {Base}_{C}$
115		simpr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to w \in {Base}_{D}$
116	1 6 108 110 112 7 114 38 115	curf11	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to 1^{st} (1^{st} (G) (x)) (w) = x 1^{st} (F) w$
117		df-ov	$⊢ x 1^{st} (F) w = 1^{st} (F) (⟨x, w⟩)$
118	116 117	eqtrdi	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to 1^{st} (1^{st} (G) (x)) (w) = 1^{st} (F) (⟨x, w⟩)$
119		simp22	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to y \in {Base}_{C}$
120	119	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to y \in {Base}_{C}$
121		eqid	$⊢ 1^{st} (G) (y) = 1^{st} (G) (y)$
122	1 6 108 110 112 7 120 121 115	curf11	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to 1^{st} (1^{st} (G) (y)) (w) = y 1^{st} (F) w$
123		df-ov	$⊢ y 1^{st} (F) w = 1^{st} (F) (⟨y, w⟩)$
124	122 123	eqtrdi	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to 1^{st} (1^{st} (G) (y)) (w) = 1^{st} (F) (⟨y, w⟩)$
125	118 124	opeq12d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to ⟨1^{st} (1^{st} (G) (x)) (w), 1^{st} (1^{st} (G) (y)) (w)⟩ = ⟨1^{st} (F) (⟨x, w⟩), 1^{st} (F) (⟨y, w⟩)⟩$
126		simp23	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to z \in {Base}_{C}$
127	126	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to z \in {Base}_{C}$
128		eqid	$⊢ 1^{st} (G) (z) = 1^{st} (G) (z)$
129	1 6 108 110 112 7 127 128 115	curf11	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to 1^{st} (1^{st} (G) (z)) (w) = z 1^{st} (F) w$
130		df-ov	$⊢ z 1^{st} (F) w = 1^{st} (F) (⟨z, w⟩)$
131	129 130	eqtrdi	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to 1^{st} (1^{st} (G) (z)) (w) = 1^{st} (F) (⟨z, w⟩)$
132	125 131	oveq12d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to ⟨1^{st} (1^{st} (G) (x)) (w), 1^{st} (1^{st} (G) (y)) (w)⟩ comp (E) 1^{st} (1^{st} (G) (z)) (w) = ⟨1^{st} (F) (⟨x, w⟩), 1^{st} (F) (⟨y, w⟩)⟩ comp (E) 1^{st} (F) (⟨z, w⟩)$
133		simp3r	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to g \in (y Hom (C) z)$
134	133	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to g \in (y Hom (C) z)$
135		eqid	$⊢ (y 2^{nd} (G) z) (g) = (y 2^{nd} (G) z) (g)$
136	1 6 108 110 112 7 10 11 120 127 134 135 115	curf2val	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to (y 2^{nd} (G) z) (g) (w) = g (⟨y, w⟩ 2^{nd} (F) ⟨z, w⟩) Id (D) (w)$
137		df-ov	$⊢ g (⟨y, w⟩ 2^{nd} (F) ⟨z, w⟩) Id (D) (w) = (⟨y, w⟩ 2^{nd} (F) ⟨z, w⟩) (⟨g, Id (D) (w)⟩)$
138	136 137	eqtrdi	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to (y 2^{nd} (G) z) (g) (w) = (⟨y, w⟩ 2^{nd} (F) ⟨z, w⟩) (⟨g, Id (D) (w)⟩)$
139		simp3l	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to f \in (x Hom (C) y)$
140	139	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to f \in (x Hom (C) y)$
141		eqid	$⊢ (x 2^{nd} (G) y) (f) = (x 2^{nd} (G) y) (f)$
142	1 6 108 110 112 7 10 11 114 120 140 141 115	curf2val	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to (x 2^{nd} (G) y) (f) (w) = f (⟨x, w⟩ 2^{nd} (F) ⟨y, w⟩) Id (D) (w)$
143		df-ov	$⊢ f (⟨x, w⟩ 2^{nd} (F) ⟨y, w⟩) Id (D) (w) = (⟨x, w⟩ 2^{nd} (F) ⟨y, w⟩) (⟨f, Id (D) (w)⟩)$
144	142 143	eqtrdi	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to (x 2^{nd} (G) y) (f) (w) = (⟨x, w⟩ 2^{nd} (F) ⟨y, w⟩) (⟨f, Id (D) (w)⟩)$
145	132 138 144	oveq123d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to (y 2^{nd} (G) z) (g) (w) (⟨1^{st} (1^{st} (G) (x)) (w), 1^{st} (1^{st} (G) (y)) (w)⟩ comp (E) 1^{st} (1^{st} (G) (z)) (w)) (x 2^{nd} (G) y) (f) (w) = (⟨y, w⟩ 2^{nd} (F) ⟨z, w⟩) (⟨g, Id (D) (w)⟩) (⟨1^{st} (F) (⟨x, w⟩), 1^{st} (F) (⟨y, w⟩)⟩ comp (E) 1^{st} (F) (⟨z, w⟩)) (⟨x, w⟩ 2^{nd} (F) ⟨y, w⟩) (⟨f, Id (D) (w)⟩)$
146		eqid	$⊢ Hom (C \times_{c} D) = Hom (C \times_{c} D)$
147		eqid	$⊢ comp (C \times_{c} D) = comp (C \times_{c} D)$
148		eqid	$⊢ comp (E) = comp (E)$
149	67 112 68	sylancr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
150		opelxpi	$⊢ (x \in {Base}_{C} \land w \in {Base}_{D}) \to ⟨x, w⟩ \in ({Base}_{C} \times {Base}_{D})$
151	113 150	sylan	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to ⟨x, w⟩ \in ({Base}_{C} \times {Base}_{D})$
152		opelxpi	$⊢ (y \in {Base}_{C} \land w \in {Base}_{D}) \to ⟨y, w⟩ \in ({Base}_{C} \times {Base}_{D})$
153	119 152	sylan	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to ⟨y, w⟩ \in ({Base}_{C} \times {Base}_{D})$
154		opelxpi	$⊢ (z \in {Base}_{C} \land w \in {Base}_{D}) \to ⟨z, w⟩ \in ({Base}_{C} \times {Base}_{D})$
155	126 154	sylan	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to ⟨z, w⟩ \in ({Base}_{C} \times {Base}_{D})$
156	7 8 11 110 115	catidcl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to Id (D) (w) \in (w Hom (D) w)$
157	140 156	opelxpd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to ⟨f, Id (D) (w)⟩ \in ((x Hom (C) y) \times (w Hom (D) w))$
158	63 6 7 10 8 114 115 120 115 146	xpchom2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to ⟨x, w⟩ Hom (C \times_{c} D) ⟨y, w⟩ = (x Hom (C) y) \times (w Hom (D) w)$
159	157 158	eleqtrrd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to ⟨f, Id (D) (w)⟩ \in (⟨x, w⟩ Hom (C \times_{c} D) ⟨y, w⟩)$
160	134 156	opelxpd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to ⟨g, Id (D) (w)⟩ \in ((y Hom (C) z) \times (w Hom (D) w))$
161	63 6 7 10 8 120 115 127 115 146	xpchom2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to ⟨y, w⟩ Hom (C \times_{c} D) ⟨z, w⟩ = (y Hom (C) z) \times (w Hom (D) w)$
162	160 161	eleqtrrd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to ⟨g, Id (D) (w)⟩ \in (⟨y, w⟩ Hom (C \times_{c} D) ⟨z, w⟩)$
163	64 146 147 148 149 151 153 155 159 162	funcco	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) (⟨g, Id (D) (w)⟩ (⟨⟨x, w⟩, ⟨y, w⟩⟩ comp (C \times_{c} D) ⟨z, w⟩) ⟨f, Id (D) (w)⟩) = (⟨y, w⟩ 2^{nd} (F) ⟨z, w⟩) (⟨g, Id (D) (w)⟩) (⟨1^{st} (F) (⟨x, w⟩), 1^{st} (F) (⟨y, w⟩)⟩ comp (E) 1^{st} (F) (⟨z, w⟩)) (⟨x, w⟩ 2^{nd} (F) ⟨y, w⟩) (⟨f, Id (D) (w)⟩)$
164		eqid	$⊢ comp (D) = comp (D)$
165	63 6 7 10 8 114 115 120 115 26 164 147 127 115 140 156 134 156	xpcco2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to ⟨g, Id (D) (w)⟩ (⟨⟨x, w⟩, ⟨y, w⟩⟩ comp (C \times_{c} D) ⟨z, w⟩) ⟨f, Id (D) (w)⟩ = ⟨g (⟨x, y⟩ comp (C) z) f, Id (D) (w) (⟨w, w⟩ comp (D) w) Id (D) (w)⟩$
166	7 8 11 110 115 164 115 156	catlid	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to Id (D) (w) (⟨w, w⟩ comp (D) w) Id (D) (w) = Id (D) (w)$
167	166	opeq2d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to ⟨g (⟨x, y⟩ comp (C) z) f, Id (D) (w) (⟨w, w⟩ comp (D) w) Id (D) (w)⟩ = ⟨g (⟨x, y⟩ comp (C) z) f, Id (D) (w)⟩$
168	165 167	eqtrd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to ⟨g, Id (D) (w)⟩ (⟨⟨x, w⟩, ⟨y, w⟩⟩ comp (C \times_{c} D) ⟨z, w⟩) ⟨f, Id (D) (w)⟩ = ⟨g (⟨x, y⟩ comp (C) z) f, Id (D) (w)⟩$
169	168	fveq2d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) (⟨g, Id (D) (w)⟩ (⟨⟨x, w⟩, ⟨y, w⟩⟩ comp (C \times_{c} D) ⟨z, w⟩) ⟨f, Id (D) (w)⟩) = (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) (⟨g (⟨x, y⟩ comp (C) z) f, Id (D) (w)⟩)$
170		df-ov	$⊢ (g (⟨x, y⟩ comp (C) z) f) (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) Id (D) (w) = (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) (⟨g (⟨x, y⟩ comp (C) z) f, Id (D) (w)⟩)$
171	169 170	eqtr4di	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) (⟨g, Id (D) (w)⟩ (⟨⟨x, w⟩, ⟨y, w⟩⟩ comp (C \times_{c} D) ⟨z, w⟩) ⟨f, Id (D) (w)⟩) = (g (⟨x, y⟩ comp (C) z) f) (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) Id (D) (w)$
172	145 163 171	3eqtr2rd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \land w \in {Base}_{D}) \to (g (⟨x, y⟩ comp (C) z) f) (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) Id (D) (w) = (y 2^{nd} (G) z) (g) (w) (⟨1^{st} (1^{st} (G) (x)) (w), 1^{st} (1^{st} (G) (y)) (w)⟩ comp (E) 1^{st} (1^{st} (G) (z)) (w)) (x 2^{nd} (G) y) (f) (w)$
173	172	mpteq2dva	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to (w \in {Base}_{D} ⟼ (g (⟨x, y⟩ comp (C) z) f) (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) Id (D) (w)) = (w \in {Base}_{D} ⟼ (y 2^{nd} (G) z) (g) (w) (⟨1^{st} (1^{st} (G) (x)) (w), 1^{st} (1^{st} (G) (y)) (w)⟩ comp (E) 1^{st} (1^{st} (G) (z)) (w)) (x 2^{nd} (G) y) (f) (w))$
174	6 10 26 107 113 119 126 139 133	catcocl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z)$
175		eqid	$⊢ (x 2^{nd} (G) z) (g (⟨x, y⟩ comp (C) z) f) = (x 2^{nd} (G) z) (g (⟨x, y⟩ comp (C) z) f)$
176	1 6 107 109 111 7 10 11 113 126 174 175	curf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to (x 2^{nd} (G) z) (g (⟨x, y⟩ comp (C) z) f) = (w \in {Base}_{D} ⟼ (g (⟨x, y⟩ comp (C) z) f) (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) Id (D) (w))$
177	1 6 107 109 111 7 10 11 113 119 139 141 23	curf2cl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to (x 2^{nd} (G) y) (f) \in (1^{st} (G) (x) (D Nat E) 1^{st} (G) (y))$
178	1 6 107 109 111 7 10 11 119 126 133 135 23	curf2cl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to (y 2^{nd} (G) z) (g) \in (1^{st} (G) (y) (D Nat E) 1^{st} (G) (z))$
179	2 23 7 148 27 177 178	fucco	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to (y 2^{nd} (G) z) (g) (⟨1^{st} (G) (x), 1^{st} (G) (y)⟩ comp (Q) 1^{st} (G) (z)) (x 2^{nd} (G) y) (f) = (w \in {Base}_{D} ⟼ (y 2^{nd} (G) z) (g) (w) (⟨1^{st} (1^{st} (G) (x)) (w), 1^{st} (1^{st} (G) (y)) (w)⟩ comp (E) 1^{st} (1^{st} (G) (z)) (w)) (x 2^{nd} (G) y) (f) (w))$
180	173 176 179	3eqtr4d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C} \land z \in {Base}_{C}) \land (f \in (x Hom (C) y) \land g \in (y Hom (C) z))) \to (x 2^{nd} (G) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (G) z) (g) (⟨1^{st} (G) (x), 1^{st} (G) (y)⟩ comp (Q) 1^{st} (G) (z)) (x 2^{nd} (G) y) (f)$
181	6 22 10 24 9 25 26 27 3 31 40 46 62 106 180	isfuncd	$⊢ φ \to 1^{st} (G) (C Func Q) 2^{nd} (G)$
182		df-br	$⊢ 1^{st} (G) (C Func Q) 2^{nd} (G) \leftrightarrow ⟨1^{st} (G), 2^{nd} (G)⟩ \in (C Func Q)$
183	181 182	sylib	$⊢ φ \to ⟨1^{st} (G), 2^{nd} (G)⟩ \in (C Func Q)$
184	21 183	eqeltrd	$⊢ φ \to G \in (C Func Q)$

Metamath Proof Explorer

Theorem curfcl

Proof