cofucl

Description: The composition of two functors is a functor. Proposition 3.23 of Adamek p. 33. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	cofucl.f	$⊢ φ \to F \in (C Func D)$
	cofucl.g	$⊢ φ \to G \in (D Func E)$
Assertion	cofucl	$⊢ φ \to G \circ_{func} F \in (C Func E)$

Proof

Step	Hyp	Ref	Expression
1		cofucl.f	$⊢ φ \to F \in (C Func D)$
2		cofucl.g	$⊢ φ \to G \in (D Func E)$
3		eqid	$⊢ {Base}_{C} = {Base}_{C}$
4	3 1 2	cofuval	$⊢ φ \to G \circ_{func} F = ⟨1^{st} (G) \circ 1^{st} (F), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))⟩$
5	3 1 2	cofu1st	$⊢ φ \to 1^{st} (G \circ_{func} F) = 1^{st} (G) \circ 1^{st} (F)$
6	4	fveq2d	$⊢ φ \to 2^{nd} (G \circ_{func} F) = 2^{nd} (⟨1^{st} (G) \circ 1^{st} (F), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))⟩)$
7		fvex	$⊢ 1^{st} (G) \in V$
8		fvex	$⊢ 1^{st} (F) \in V$
9	7 8	coex	$⊢ 1^{st} (G) \circ 1^{st} (F) \in V$
10		fvex	$⊢ {Base}_{C} \in V$
11	10 10	mpoex	$⊢ (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)) \in V$
12	9 11	op2nd	$⊢ 2^{nd} (⟨1^{st} (G) \circ 1^{st} (F), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))⟩) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))$
13	6 12	eqtrdi	$⊢ φ \to 2^{nd} (G \circ_{func} F) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))$
14	5 13	opeq12d	$⊢ φ \to ⟨1^{st} (G \circ_{func} F), 2^{nd} (G \circ_{func} F)⟩ = ⟨1^{st} (G) \circ 1^{st} (F), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))⟩$
15	4 14	eqtr4d	$⊢ φ \to G \circ_{func} F = ⟨1^{st} (G \circ_{func} F), 2^{nd} (G \circ_{func} F)⟩$
16		eqid	$⊢ {Base}_{D} = {Base}_{D}$
17		eqid	$⊢ {Base}_{E} = {Base}_{E}$
18		relfunc	$⊢ Rel (D Func E)$
19		1st2ndbr	$⊢ (Rel (D Func E) \land G \in (D Func E)) \to 1^{st} (G) (D Func E) 2^{nd} (G)$
20	18 2 19	sylancr	$⊢ φ \to 1^{st} (G) (D Func E) 2^{nd} (G)$
21	16 17 20	funcf1	$⊢ φ \to 1^{st} (G) : {Base}_{D} ⟶ {Base}_{E}$
22		relfunc	$⊢ Rel (C Func D)$
23		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
24	22 1 23	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
25	3 16 24	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
26		fco	$⊢ (1^{st} (G) : {Base}_{D} ⟶ {Base}_{E} \land 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}) \to (1^{st} (G) \circ 1^{st} (F)) : {Base}_{C} ⟶ {Base}_{E}$
27	21 25 26	syl2anc	$⊢ φ \to (1^{st} (G) \circ 1^{st} (F)) : {Base}_{C} ⟶ {Base}_{E}$
28	5	feq1d	$⊢ φ \to (1^{st} (G \circ_{func} F) : {Base}_{C} ⟶ {Base}_{E} \leftrightarrow (1^{st} (G) \circ 1^{st} (F)) : {Base}_{C} ⟶ {Base}_{E})$
29	27 28	mpbird	$⊢ φ \to 1^{st} (G \circ_{func} F) : {Base}_{C} ⟶ {Base}_{E}$
30		eqid	$⊢ (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y))$
31		ovex	$⊢ 1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y) \in V$
32		ovex	$⊢ x 2^{nd} (F) y \in V$
33	31 32	coex	$⊢ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y) \in V$
34	30 33	fnmpoi	$⊢ (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)) Fn ({Base}_{C} \times {Base}_{C})$
35	13	fneq1d	$⊢ φ \to (2^{nd} (G \circ_{func} F) Fn ({Base}_{C} \times {Base}_{C}) \leftrightarrow (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)) Fn ({Base}_{C} \times {Base}_{C}))$
36	34 35	mpbiri	$⊢ φ \to 2^{nd} (G \circ_{func} F) Fn ({Base}_{C} \times {Base}_{C})$
37		eqid	$⊢ Hom (D) = Hom (D)$
38		eqid	$⊢ Hom (E) = Hom (E)$
39	20	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (G) (D Func E) 2^{nd} (G)$
40	25	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
41		simprl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \in {Base}_{C}$
42	40 41	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) (x) \in {Base}_{D}$
43		simprr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to y \in {Base}_{C}$
44	40 43	ffvelcdmd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) (y) \in {Base}_{D}$
45	16 37 38 39 42 44	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) : 1^{st} (F) (x) Hom (D) 1^{st} (F) (y) ⟶ 1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y))$
46		eqid	$⊢ Hom (C) = Hom (C)$
47	24	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
48	3 46 37 47 41 43	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (F) y) : x Hom (C) y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)$
49		fco	$⊢ ((1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) : 1^{st} (F) (x) Hom (D) 1^{st} (F) (y) ⟶ 1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y)) \land (x 2^{nd} (F) y) : x Hom (C) y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)) \to ((1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)) : x Hom (C) y ⟶ 1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y))$
50	45 48 49	syl2anc	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to ((1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)) : x Hom (C) y ⟶ 1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y))$
51		ovex	$⊢ 1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y)) \in V$
52		ovex	$⊢ x Hom (C) y \in V$
53	51 52	elmap	$⊢ (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y) \in ({(1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y)))}^{(x Hom (C) y)}) \leftrightarrow ((1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)) : x Hom (C) y ⟶ 1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y))$
54	50 53	sylibr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y) \in ({(1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y)))}^{(x Hom (C) y)})$
55	1	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to F \in (C Func D)$
56	2	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to G \in (D Func E)$
57	3 55 56 41 43	cofu2nd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x 2^{nd} (G \circ_{func} F) y = (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)$
58	3 55 56 41	cofu1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (G \circ_{func} F) (x) = 1^{st} (G) (1^{st} (F) (x))$
59	3 55 56 43	cofu1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (G \circ_{func} F) (y) = 1^{st} (G) (1^{st} (F) (y))$
60	58 59	oveq12d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (G \circ_{func} F) (x) Hom (E) 1^{st} (G \circ_{func} F) (y) = 1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y))$
61	60	oveq1d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to {(1^{st} (G \circ_{func} F) (x) Hom (E) 1^{st} (G \circ_{func} F) (y))}^{(x Hom (C) y)} = {(1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y)))}^{(x Hom (C) y)}$
62	54 57 61	3eltr4d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x 2^{nd} (G \circ_{func} F) y \in ({(1^{st} (G \circ_{func} F) (x) Hom (E) 1^{st} (G \circ_{func} F) (y))}^{(x Hom (C) y)})$
63	62	ralrimivva	$⊢ φ \to \forall x \in {Base}_{C} \forall y \in {Base}_{C} x 2^{nd} (G \circ_{func} F) y \in ({(1^{st} (G \circ_{func} F) (x) Hom (E) 1^{st} (G \circ_{func} F) (y))}^{(x Hom (C) y)})$
64		fveq2	$⊢ z = ⟨x, y⟩ \to 2^{nd} (G \circ_{func} F) (z) = 2^{nd} (G \circ_{func} F) (⟨x, y⟩)$
65		df-ov	$⊢ x 2^{nd} (G \circ_{func} F) y = 2^{nd} (G \circ_{func} F) (⟨x, y⟩)$
66	64 65	eqtr4di	$⊢ z = ⟨x, y⟩ \to 2^{nd} (G \circ_{func} F) (z) = x 2^{nd} (G \circ_{func} F) y$
67		vex	$⊢ x \in V$
68		vex	$⊢ y \in V$
69	67 68	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
70	69	fveq2d	$⊢ z = ⟨x, y⟩ \to 1^{st} (G \circ_{func} F) (1^{st} (z)) = 1^{st} (G \circ_{func} F) (x)$
71	67 68	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
72	71	fveq2d	$⊢ z = ⟨x, y⟩ \to 1^{st} (G \circ_{func} F) (2^{nd} (z)) = 1^{st} (G \circ_{func} F) (y)$
73	70 72	oveq12d	$⊢ z = ⟨x, y⟩ \to 1^{st} (G \circ_{func} F) (1^{st} (z)) Hom (E) 1^{st} (G \circ_{func} F) (2^{nd} (z)) = 1^{st} (G \circ_{func} F) (x) Hom (E) 1^{st} (G \circ_{func} F) (y)$
74		fveq2	$⊢ z = ⟨x, y⟩ \to Hom (C) (z) = Hom (C) (⟨x, y⟩)$
75		df-ov	$⊢ x Hom (C) y = Hom (C) (⟨x, y⟩)$
76	74 75	eqtr4di	$⊢ z = ⟨x, y⟩ \to Hom (C) (z) = x Hom (C) y$
77	73 76	oveq12d	$⊢ z = ⟨x, y⟩ \to {(1^{st} (G \circ_{func} F) (1^{st} (z)) Hom (E) 1^{st} (G \circ_{func} F) (2^{nd} (z)))}^{Hom (C) (z)} = {(1^{st} (G \circ_{func} F) (x) Hom (E) 1^{st} (G \circ_{func} F) (y))}^{(x Hom (C) y)}$
78	66 77	eleq12d	$⊢ z = ⟨x, y⟩ \to (2^{nd} (G \circ_{func} F) (z) \in ({(1^{st} (G \circ_{func} F) (1^{st} (z)) Hom (E) 1^{st} (G \circ_{func} F) (2^{nd} (z)))}^{Hom (C) (z)}) \leftrightarrow x 2^{nd} (G \circ_{func} F) y \in ({(1^{st} (G \circ_{func} F) (x) Hom (E) 1^{st} (G \circ_{func} F) (y))}^{(x Hom (C) y)}))$
79	78	ralxp	$⊢ \forall z \in ({Base}_{C} \times {Base}_{C}) 2^{nd} (G \circ_{func} F) (z) \in ({(1^{st} (G \circ_{func} F) (1^{st} (z)) Hom (E) 1^{st} (G \circ_{func} F) (2^{nd} (z)))}^{Hom (C) (z)}) \leftrightarrow \forall x \in {Base}_{C} \forall y \in {Base}_{C} x 2^{nd} (G \circ_{func} F) y \in ({(1^{st} (G \circ_{func} F) (x) Hom (E) 1^{st} (G \circ_{func} F) (y))}^{(x Hom (C) y)})$
80	63 79	sylibr	$⊢ φ \to \forall z \in ({Base}_{C} \times {Base}_{C}) 2^{nd} (G \circ_{func} F) (z) \in ({(1^{st} (G \circ_{func} F) (1^{st} (z)) Hom (E) 1^{st} (G \circ_{func} F) (2^{nd} (z)))}^{Hom (C) (z)})$
81		fvex	$⊢ 2^{nd} (G \circ_{func} F) \in V$
82	81	elixp	$⊢ 2^{nd} (G \circ_{func} F) \in \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} ({(1^{st} (G \circ_{func} F) (1^{st} (z)) Hom (E) 1^{st} (G \circ_{func} F) (2^{nd} (z)))}^{Hom (C) (z)}) \leftrightarrow (2^{nd} (G \circ_{func} F) Fn ({Base}_{C} \times {Base}_{C}) \land \forall z \in ({Base}_{C} \times {Base}_{C}) 2^{nd} (G \circ_{func} F) (z) \in ({(1^{st} (G \circ_{func} F) (1^{st} (z)) Hom (E) 1^{st} (G \circ_{func} F) (2^{nd} (z)))}^{Hom (C) (z)}))$
83	36 80 82	sylanbrc	$⊢ φ \to 2^{nd} (G \circ_{func} F) \in \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} ({(1^{st} (G \circ_{func} F) (1^{st} (z)) Hom (E) 1^{st} (G \circ_{func} F) (2^{nd} (z)))}^{Hom (C) (z)})$
84		eqid	$⊢ Id (C) = Id (C)$
85		eqid	$⊢ Id (D) = Id (D)$
86	24	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
87		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
88	3 84 85 86 87	funcid	$⊢ (φ \land x \in {Base}_{C}) \to (x 2^{nd} (F) x) (Id (C) (x)) = Id (D) (1^{st} (F) (x))$
89	88	fveq2d	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (x)) ((x 2^{nd} (F) x) (Id (C) (x))) = (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (x)) (Id (D) (1^{st} (F) (x)))$
90		eqid	$⊢ Id (E) = Id (E)$
91	20	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G) (D Func E) 2^{nd} (G)$
92	25	ffvelcdmda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (x) \in {Base}_{D}$
93	16 85 90 91 92	funcid	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (x)) (Id (D) (1^{st} (F) (x))) = Id (E) (1^{st} (G) (1^{st} (F) (x)))$
94	89 93	eqtrd	$⊢ (φ \land x \in {Base}_{C}) \to (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (x)) ((x 2^{nd} (F) x) (Id (C) (x))) = Id (E) (1^{st} (G) (1^{st} (F) (x)))$
95	1	adantr	$⊢ (φ \land x \in {Base}_{C}) \to F \in (C Func D)$
96	2	adantr	$⊢ (φ \land x \in {Base}_{C}) \to G \in (D Func E)$
97		funcrcl	$⊢ F \in (C Func D) \to (C \in Cat \land D \in Cat)$
98	1 97	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
99	98	simpld	$⊢ φ \to C \in Cat$
100	99	adantr	$⊢ (φ \land x \in {Base}_{C}) \to C \in Cat$
101	3 46 84 100 87	catidcl	$⊢ (φ \land x \in {Base}_{C}) \to Id (C) (x) \in (x Hom (C) x)$
102	3 95 96 87 87 46 101	cofu2	$⊢ (φ \land x \in {Base}_{C}) \to (x 2^{nd} (G \circ_{func} F) x) (Id (C) (x)) = (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (x)) ((x 2^{nd} (F) x) (Id (C) (x)))$
103	3 95 96 87	cofu1	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G \circ_{func} F) (x) = 1^{st} (G) (1^{st} (F) (x))$
104	103	fveq2d	$⊢ (φ \land x \in {Base}_{C}) \to Id (E) (1^{st} (G \circ_{func} F) (x)) = Id (E) (1^{st} (G) (1^{st} (F) (x)))$
105	94 102 104	3eqtr4d	$⊢ (φ \land x \in {Base}_{C}) \to (x 2^{nd} (G \circ_{func} F) x) (Id (C) (x)) = Id (E) (1^{st} (G \circ_{func} F) (x))$
106	86	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)))) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
107		simplr	$⊢ ((φ \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}$
108		simprlr	$⊢ ((φ \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}$
109	3 46 37 106 107 108	funcf2	$⊢ ((φ \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} (F) z) : x Hom (C) z ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (z)$
110		eqid	$⊢ comp (C) = comp (C)$
111	100	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)))) \to C \in Cat$
112		simprll	$⊢ ((φ \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}$
113		simprrl	$⊢ ((φ \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)$
114		simprrr	$⊢ ((φ \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)$
115	3 46 110 111 107 112 108 113 114	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)$
116		fvco3	$⊢ ((x 2^{nd} (F) z) : x Hom (C) z ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (z) \land g (⟨x, y⟩ comp (C) z) f \in (x Hom (C) z)) \to ((1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (z)) \circ (x 2^{nd} (F) z)) (g (⟨x, y⟩ comp (C) z) f) = (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (z)) ((x 2^{nd} (F) z) (g (⟨x, y⟩ comp (C) z) f))$
117	109 115 116	syl2anc	$⊢ ((φ \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 ((1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (z)) \circ (x 2^{nd} (F) z)) (g (⟨x, y⟩ comp (C) z) f) = (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (z)) ((x 2^{nd} (F) z) (g (⟨x, y⟩ comp (C) z) f))$
118		eqid	$⊢ comp (D) = comp (D)$
119	3 46 110 118 106 107 112 108 113 114	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)))) \to (x 2^{nd} (F) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (F) z) (g) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (z)) (x 2^{nd} (F) y) (f)$
120	119	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)))) \to (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (z)) ((x 2^{nd} (F) z) (g (⟨x, y⟩ comp (C) z) f)) = (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (z)) ((y 2^{nd} (F) z) (g) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (z)) (x 2^{nd} (F) y) (f))$
121		eqid	$⊢ comp (E) = comp (E)$
122	91	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)))) \to 1^{st} (G) (D Func E) 2^{nd} (G)$
123	92	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)))) \to 1^{st} (F) (x) \in {Base}_{D}$
124	25	adantr	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
125	124	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)))) \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
126	125 112	ffvelcdmd	$⊢ ((φ \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 1^{st} (F) (y) \in {Base}_{D}$
127	125 108	ffvelcdmd	$⊢ ((φ \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 1^{st} (F) (z) \in {Base}_{D}$
128	3 46 37 106 107 112	funcf2	$⊢ ((φ \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} (F) y) : x Hom (C) y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)$
129	128 113	ffvelcdmd	$⊢ ((φ \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} (F) y) (f) \in (1^{st} (F) (x) Hom (D) 1^{st} (F) (y))$
130	3 46 37 106 112 108	funcf2	$⊢ ((φ \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} (F) z) : y Hom (C) z ⟶ 1^{st} (F) (y) Hom (D) 1^{st} (F) (z)$
131	130 114	ffvelcdmd	$⊢ ((φ \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} (F) z) (g) \in (1^{st} (F) (y) Hom (D) 1^{st} (F) (z))$
132	16 37 118 121 122 123 126 127 129 131	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)))) \to (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (z)) ((y 2^{nd} (F) z) (g) (⟨1^{st} (F) (x), 1^{st} (F) (y)⟩ comp (D) 1^{st} (F) (z)) (x 2^{nd} (F) y) (f)) = (1^{st} (F) (y) 2^{nd} (G) 1^{st} (F) (z)) ((y 2^{nd} (F) z) (g)) (⟨1^{st} (G) (1^{st} (F) (x)), 1^{st} (G) (1^{st} (F) (y))⟩ comp (E) 1^{st} (G) (1^{st} (F) (z))) (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) ((x 2^{nd} (F) y) (f))$
133	117 120 132	3eqtrd	$⊢ ((φ \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 ((1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (z)) \circ (x 2^{nd} (F) z)) (g (⟨x, y⟩ comp (C) z) f) = (1^{st} (F) (y) 2^{nd} (G) 1^{st} (F) (z)) ((y 2^{nd} (F) z) (g)) (⟨1^{st} (G) (1^{st} (F) (x)), 1^{st} (G) (1^{st} (F) (y))⟩ comp (E) 1^{st} (G) (1^{st} (F) (z))) (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) ((x 2^{nd} (F) y) (f))$
134	95	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)))) \to F \in (C Func D)$
135	96	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)))) \to G \in (D Func E)$
136	3 134 135 107 108	cofu2nd	$⊢ ((φ \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 \circ_{func} F) z = (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (z)) \circ (x 2^{nd} (F) z)$
137	136	fveq1d	$⊢ ((φ \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 \circ_{func} F) z) (g (⟨x, y⟩ comp (C) z) f) = ((1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (z)) \circ (x 2^{nd} (F) z)) (g (⟨x, y⟩ comp (C) z) f)$
138	103	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)))) \to 1^{st} (G \circ_{func} F) (x) = 1^{st} (G) (1^{st} (F) (x))$
139	3 134 135 112	cofu1	$⊢ ((φ \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 1^{st} (G \circ_{func} F) (y) = 1^{st} (G) (1^{st} (F) (y))$
140	138 139	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)))) \to ⟨1^{st} (G \circ_{func} F) (x), 1^{st} (G \circ_{func} F) (y)⟩ = ⟨1^{st} (G) (1^{st} (F) (x)), 1^{st} (G) (1^{st} (F) (y))⟩$
141	3 134 135 108	cofu1	$⊢ ((φ \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 1^{st} (G \circ_{func} F) (z) = 1^{st} (G) (1^{st} (F) (z))$
142	140 141	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)))) \to ⟨1^{st} (G \circ_{func} F) (x), 1^{st} (G \circ_{func} F) (y)⟩ comp (E) 1^{st} (G \circ_{func} F) (z) = ⟨1^{st} (G) (1^{st} (F) (x)), 1^{st} (G) (1^{st} (F) (y))⟩ comp (E) 1^{st} (G) (1^{st} (F) (z))$
143	3 134 135 112 108 46 114	cofu2	$⊢ ((φ \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 \circ_{func} F) z) (g) = (1^{st} (F) (y) 2^{nd} (G) 1^{st} (F) (z)) ((y 2^{nd} (F) z) (g))$
144	3 134 135 107 112 46 113	cofu2	$⊢ ((φ \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 \circ_{func} F) y) (f) = (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) ((x 2^{nd} (F) y) (f))$
145	142 143 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)))) \to (y 2^{nd} (G \circ_{func} F) z) (g) (⟨1^{st} (G \circ_{func} F) (x), 1^{st} (G \circ_{func} F) (y)⟩ comp (E) 1^{st} (G \circ_{func} F) (z)) (x 2^{nd} (G \circ_{func} F) y) (f) = (1^{st} (F) (y) 2^{nd} (G) 1^{st} (F) (z)) ((y 2^{nd} (F) z) (g)) (⟨1^{st} (G) (1^{st} (F) (x)), 1^{st} (G) (1^{st} (F) (y))⟩ comp (E) 1^{st} (G) (1^{st} (F) (z))) (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) ((x 2^{nd} (F) y) (f))$
146	133 137 145	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 \circ_{func} F) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (G \circ_{func} F) z) (g) (⟨1^{st} (G \circ_{func} F) (x), 1^{st} (G \circ_{func} F) (y)⟩ comp (E) 1^{st} (G \circ_{func} F) (z)) (x 2^{nd} (G \circ_{func} F) y) (f)$
147	146	anassrs	$⊢ (((φ \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 \circ_{func} F) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (G \circ_{func} F) z) (g) (⟨1^{st} (G \circ_{func} F) (x), 1^{st} (G \circ_{func} F) (y)⟩ comp (E) 1^{st} (G \circ_{func} F) (z)) (x 2^{nd} (G \circ_{func} F) y) (f)$
148	147	ralrimivva	$⊢ ((φ \land x \in {Base}_{C}) \land (y \in {Base}_{C} \land z \in {Base}_{C})) \to \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (x 2^{nd} (G \circ_{func} F) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (G \circ_{func} F) z) (g) (⟨1^{st} (G \circ_{func} F) (x), 1^{st} (G \circ_{func} F) (y)⟩ comp (E) 1^{st} (G \circ_{func} F) (z)) (x 2^{nd} (G \circ_{func} F) y) (f)$
149	148	ralrimivva	$⊢ (φ \land x \in {Base}_{C}) \to \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (x 2^{nd} (G \circ_{func} F) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (G \circ_{func} F) z) (g) (⟨1^{st} (G \circ_{func} F) (x), 1^{st} (G \circ_{func} F) (y)⟩ comp (E) 1^{st} (G \circ_{func} F) (z)) (x 2^{nd} (G \circ_{func} F) y) (f)$
150	105 149	jca	$⊢ (φ \land x \in {Base}_{C}) \to ((x 2^{nd} (G \circ_{func} F) x) (Id (C) (x)) = Id (E) (1^{st} (G \circ_{func} F) (x)) \land \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (x 2^{nd} (G \circ_{func} F) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (G \circ_{func} F) z) (g) (⟨1^{st} (G \circ_{func} F) (x), 1^{st} (G \circ_{func} F) (y)⟩ comp (E) 1^{st} (G \circ_{func} F) (z)) (x 2^{nd} (G \circ_{func} F) y) (f))$
151	150	ralrimiva	$⊢ φ \to \forall x \in {Base}_{C} ((x 2^{nd} (G \circ_{func} F) x) (Id (C) (x)) = Id (E) (1^{st} (G \circ_{func} F) (x)) \land \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (x 2^{nd} (G \circ_{func} F) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (G \circ_{func} F) z) (g) (⟨1^{st} (G \circ_{func} F) (x), 1^{st} (G \circ_{func} F) (y)⟩ comp (E) 1^{st} (G \circ_{func} F) (z)) (x 2^{nd} (G \circ_{func} F) y) (f))$
152		funcrcl	$⊢ G \in (D Func E) \to (D \in Cat \land E \in Cat)$
153	2 152	syl	$⊢ φ \to (D \in Cat \land E \in Cat)$
154	153	simprd	$⊢ φ \to E \in Cat$
155	3 17 46 38 84 90 110 121 99 154	isfunc	$⊢ φ \to (1^{st} (G \circ_{func} F) (C Func E) 2^{nd} (G \circ_{func} F) \leftrightarrow (1^{st} (G \circ_{func} F) : {Base}_{C} ⟶ {Base}_{E} \land 2^{nd} (G \circ_{func} F) \in \underset{z \in {Base}_{C} \times {Base}_{C}}{⨉} ({(1^{st} (G \circ_{func} F) (1^{st} (z)) Hom (E) 1^{st} (G \circ_{func} F) (2^{nd} (z)))}^{Hom (C) (z)}) \land \forall x \in {Base}_{C} ((x 2^{nd} (G \circ_{func} F) x) (Id (C) (x)) = Id (E) (1^{st} (G \circ_{func} F) (x)) \land \forall y \in {Base}_{C} \forall z \in {Base}_{C} \forall f \in (x Hom (C) y) \forall g \in (y Hom (C) z) (x 2^{nd} (G \circ_{func} F) z) (g (⟨x, y⟩ comp (C) z) f) = (y 2^{nd} (G \circ_{func} F) z) (g) (⟨1^{st} (G \circ_{func} F) (x), 1^{st} (G \circ_{func} F) (y)⟩ comp (E) 1^{st} (G \circ_{func} F) (z)) (x 2^{nd} (G \circ_{func} F) y) (f))))$
156	29 83 151 155	mpbir3and	$⊢ φ \to 1^{st} (G \circ_{func} F) (C Func E) 2^{nd} (G \circ_{func} F)$
157		df-br	$⊢ 1^{st} (G \circ_{func} F) (C Func E) 2^{nd} (G \circ_{func} F) \leftrightarrow ⟨1^{st} (G \circ_{func} F), 2^{nd} (G \circ_{func} F)⟩ \in (C Func E)$
158	156 157	sylib	$⊢ φ \to ⟨1^{st} (G \circ_{func} F), 2^{nd} (G \circ_{func} F)⟩ \in (C Func E)$
159	15 158	eqeltrd	$⊢ φ \to G \circ_{func} F \in (C Func E)$

Metamath Proof Explorer

Theorem cofucl

Proof