uncf2

Description: Value of the uncurry functor on a morphism. (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$
	uncf2.h	$⊢ H = Hom (C)$
	uncf2.j	$⊢ J = Hom (D)$
	uncf2.z	$⊢ φ \to Z \in A$
	uncf2.w	$⊢ φ \to W \in B$
	uncf2.r	$⊢ φ \to R \in (X H Z)$
	uncf2.s	$⊢ φ \to S \in (Y J W)$
Assertion	uncf2	$⊢ φ \to R (⟨X, Y⟩ 2^{nd} (F) ⟨Z, W⟩) S = (X 2^{nd} (G) Z) (R) (W) (⟨1^{st} (1^{st} (G) (X)) (Y), 1^{st} (1^{st} (G) (X)) (W)⟩ comp (E) 1^{st} (1^{st} (G) (Z)) (W)) (Y 2^{nd} (1^{st} (G) (X)) W) (S)$

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		uncf2.h	$⊢ H = Hom (C)$
10		uncf2.j	$⊢ J = Hom (D)$
11		uncf2.z	$⊢ φ \to Z \in A$
12		uncf2.w	$⊢ φ \to W \in B$
13		uncf2.r	$⊢ φ \to R \in (X H Z)$
14		uncf2.s	$⊢ φ \to S \in (Y J W)$
15	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))$
16	15	fveq2d	$⊢ φ \to 2^{nd} (F) = 2^{nd} ((D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)))$
17	16	oveqd	$⊢ φ \to ⟨X, Y⟩ 2^{nd} (F) ⟨Z, W⟩ = ⟨X, Y⟩ 2^{nd} ((D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))) ⟨Z, W⟩$
18	17	oveqd	$⊢ φ \to R (⟨X, Y⟩ 2^{nd} (F) ⟨Z, W⟩) S = R (⟨X, Y⟩ 2^{nd} ((D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))) ⟨Z, W⟩) S$
19		df-ov	$⊢ R (⟨X, Y⟩ 2^{nd} ((D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))) ⟨Z, W⟩) S = (⟨X, Y⟩ 2^{nd} ((D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))) ⟨Z, W⟩) (⟨R, S⟩)$
20		eqid	$⊢ C \times_{c} D = C \times_{c} D$
21	20 5 6	xpcbas	$⊢ A \times B = {Base}_{(C \times_{c} D)}$
22		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)$
23		eqid	$⊢ (D FuncCat E) \times_{c} D = (D FuncCat E) \times_{c} D$
24		funcrcl	$⊢ G \in (C Func (D FuncCat E)) \to (C \in Cat \land D FuncCat E \in Cat)$
25	4 24	syl	$⊢ φ \to (C \in Cat \land D FuncCat E \in Cat)$
26	25	simpld	$⊢ φ \to C \in Cat$
27		eqid	$⊢ C {1^{st}}_{F} D = C {1^{st}}_{F} D$
28	20 26 2 27	1stfcl	$⊢ φ \to C {1^{st}}_{F} D \in ((C \times_{c} D) Func C)$
29	28 4	cofucl	$⊢ φ \to G \circ_{func} (C {1^{st}}_{F} D) \in ((C \times_{c} D) Func (D FuncCat E))$
30		eqid	$⊢ C {2^{nd}}_{F} D = C {2^{nd}}_{F} D$
31	20 26 2 30	2ndfcl	$⊢ φ \to C {2^{nd}}_{F} D \in ((C \times_{c} D) Func D)$
32	22 23 29 31	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))$
33		eqid	$⊢ D {eval}_{F} E = D {eval}_{F} E$
34		eqid	$⊢ D FuncCat E = D FuncCat E$
35	33 34 2 3	evlfcl	$⊢ φ \to D {eval}_{F} E \in (((D FuncCat E) \times_{c} D) Func E)$
36	7 8	opelxpd	$⊢ φ \to ⟨X, Y⟩ \in (A \times B)$
37	11 12	opelxpd	$⊢ φ \to ⟨Z, W⟩ \in (A \times B)$
38		eqid	$⊢ Hom (C \times_{c} D) = Hom (C \times_{c} D)$
39	13 14	opelxpd	$⊢ φ \to ⟨R, S⟩ \in ((X H Z) \times (Y J W))$
40	20 5 6 9 10 7 8 11 12 38	xpchom2	$⊢ φ \to ⟨X, Y⟩ Hom (C \times_{c} D) ⟨Z, W⟩ = (X H Z) \times (Y J W)$
41	39 40	eleqtrrd	$⊢ φ \to ⟨R, S⟩ \in (⟨X, Y⟩ Hom (C \times_{c} D) ⟨Z, W⟩)$
42	21 32 35 36 37 38 41	cofu2	$⊢ φ \to (⟨X, Y⟩ 2^{nd} ((D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))) ⟨Z, W⟩) (⟨R, S⟩) = (1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨X, Y⟩) 2^{nd} (D {eval}_{F} E) 1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨Z, W⟩)) ((⟨X, Y⟩ 2^{nd} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) ⟨Z, W⟩) (⟨R, S⟩))$
43	19 42	eqtrid	$⊢ φ \to R (⟨X, Y⟩ 2^{nd} ((D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D))) ⟨Z, W⟩) S = (1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨X, Y⟩) 2^{nd} (D {eval}_{F} E) 1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨Z, W⟩)) ((⟨X, Y⟩ 2^{nd} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) ⟨Z, W⟩) (⟨R, S⟩))$
44	18 43	eqtrd	$⊢ φ \to R (⟨X, Y⟩ 2^{nd} (F) ⟨Z, W⟩) S = (1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨X, Y⟩) 2^{nd} (D {eval}_{F} E) 1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨Z, W⟩)) ((⟨X, Y⟩ 2^{nd} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) ⟨Z, W⟩) (⟨R, S⟩))$
45	22 21 38 29 31 36	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⟩)⟩$
46	21 28 4 36	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⟩))$
47	20 21 38 26 2 27 36	1stf1	$⊢ φ \to 1^{st} (C {1^{st}}_{F} D) (⟨X, Y⟩) = 1^{st} (⟨X, Y⟩)$
48		op1stg	$⊢ (X \in A \land Y \in B) \to 1^{st} (⟨X, Y⟩) = X$
49	7 8 48	syl2anc	$⊢ φ \to 1^{st} (⟨X, Y⟩) = X$
50	47 49	eqtrd	$⊢ φ \to 1^{st} (C {1^{st}}_{F} D) (⟨X, Y⟩) = X$
51	50	fveq2d	$⊢ φ \to 1^{st} (G) (1^{st} (C {1^{st}}_{F} D) (⟨X, Y⟩)) = 1^{st} (G) (X)$
52	46 51	eqtrd	$⊢ φ \to 1^{st} (G \circ_{func} (C {1^{st}}_{F} D)) (⟨X, Y⟩) = 1^{st} (G) (X)$
53	20 21 38 26 2 30 36	2ndf1	$⊢ φ \to 1^{st} (C {2^{nd}}_{F} D) (⟨X, Y⟩) = 2^{nd} (⟨X, Y⟩)$
54		op2ndg	$⊢ (X \in A \land Y \in B) \to 2^{nd} (⟨X, Y⟩) = Y$
55	7 8 54	syl2anc	$⊢ φ \to 2^{nd} (⟨X, Y⟩) = Y$
56	53 55	eqtrd	$⊢ φ \to 1^{st} (C {2^{nd}}_{F} D) (⟨X, Y⟩) = Y$
57	52 56	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⟩$
58	45 57	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⟩$
59	22 21 38 29 31 37	prf1	$⊢ φ \to 1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨Z, W⟩) = ⟨1^{st} (G \circ_{func} (C {1^{st}}_{F} D)) (⟨Z, W⟩), 1^{st} (C {2^{nd}}_{F} D) (⟨Z, W⟩)⟩$
60	21 28 4 37	cofu1	$⊢ φ \to 1^{st} (G \circ_{func} (C {1^{st}}_{F} D)) (⟨Z, W⟩) = 1^{st} (G) (1^{st} (C {1^{st}}_{F} D) (⟨Z, W⟩))$
61	20 21 38 26 2 27 37	1stf1	$⊢ φ \to 1^{st} (C {1^{st}}_{F} D) (⟨Z, W⟩) = 1^{st} (⟨Z, W⟩)$
62		op1stg	$⊢ (Z \in A \land W \in B) \to 1^{st} (⟨Z, W⟩) = Z$
63	11 12 62	syl2anc	$⊢ φ \to 1^{st} (⟨Z, W⟩) = Z$
64	61 63	eqtrd	$⊢ φ \to 1^{st} (C {1^{st}}_{F} D) (⟨Z, W⟩) = Z$
65	64	fveq2d	$⊢ φ \to 1^{st} (G) (1^{st} (C {1^{st}}_{F} D) (⟨Z, W⟩)) = 1^{st} (G) (Z)$
66	60 65	eqtrd	$⊢ φ \to 1^{st} (G \circ_{func} (C {1^{st}}_{F} D)) (⟨Z, W⟩) = 1^{st} (G) (Z)$
67	20 21 38 26 2 30 37	2ndf1	$⊢ φ \to 1^{st} (C {2^{nd}}_{F} D) (⟨Z, W⟩) = 2^{nd} (⟨Z, W⟩)$
68		op2ndg	$⊢ (Z \in A \land W \in B) \to 2^{nd} (⟨Z, W⟩) = W$
69	11 12 68	syl2anc	$⊢ φ \to 2^{nd} (⟨Z, W⟩) = W$
70	67 69	eqtrd	$⊢ φ \to 1^{st} (C {2^{nd}}_{F} D) (⟨Z, W⟩) = W$
71	66 70	opeq12d	$⊢ φ \to ⟨1^{st} (G \circ_{func} (C {1^{st}}_{F} D)) (⟨Z, W⟩), 1^{st} (C {2^{nd}}_{F} D) (⟨Z, W⟩)⟩ = ⟨1^{st} (G) (Z), W⟩$
72	59 71	eqtrd	$⊢ φ \to 1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨Z, W⟩) = ⟨1^{st} (G) (Z), W⟩$
73	58 72	oveq12d	$⊢ φ \to 1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨X, Y⟩) 2^{nd} (D {eval}_{F} E) 1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨Z, W⟩) = ⟨1^{st} (G) (X), Y⟩ 2^{nd} (D {eval}_{F} E) ⟨1^{st} (G) (Z), W⟩$
74	22 21 38 29 31 36 37 41	prf2	$⊢ φ \to (⟨X, Y⟩ 2^{nd} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) ⟨Z, W⟩) (⟨R, S⟩) = ⟨(⟨X, Y⟩ 2^{nd} (G \circ_{func} (C {1^{st}}_{F} D)) ⟨Z, W⟩) (⟨R, S⟩), (⟨X, Y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨Z, W⟩) (⟨R, S⟩)⟩$
75	21 28 4 36 37 38 41	cofu2	$⊢ φ \to (⟨X, Y⟩ 2^{nd} (G \circ_{func} (C {1^{st}}_{F} D)) ⟨Z, W⟩) (⟨R, S⟩) = (1^{st} (C {1^{st}}_{F} D) (⟨X, Y⟩) 2^{nd} (G) 1^{st} (C {1^{st}}_{F} D) (⟨Z, W⟩)) ((⟨X, Y⟩ 2^{nd} (C {1^{st}}_{F} D) ⟨Z, W⟩) (⟨R, S⟩))$
76	50 64	oveq12d	$⊢ φ \to 1^{st} (C {1^{st}}_{F} D) (⟨X, Y⟩) 2^{nd} (G) 1^{st} (C {1^{st}}_{F} D) (⟨Z, W⟩) = X 2^{nd} (G) Z$
77	20 21 38 26 2 27 36 37	1stf2	$⊢ φ \to ⟨X, Y⟩ 2^{nd} (C {1^{st}}_{F} D) ⟨Z, W⟩ = {1^{st} ↾}_{(⟨X, Y⟩ Hom (C \times_{c} D) ⟨Z, W⟩)}$
78	77	fveq1d	$⊢ φ \to (⟨X, Y⟩ 2^{nd} (C {1^{st}}_{F} D) ⟨Z, W⟩) (⟨R, S⟩) = ({1^{st} ↾}_{(⟨X, Y⟩ Hom (C \times_{c} D) ⟨Z, W⟩)}) (⟨R, S⟩)$
79	41	fvresd	$⊢ φ \to ({1^{st} ↾}_{(⟨X, Y⟩ Hom (C \times_{c} D) ⟨Z, W⟩)}) (⟨R, S⟩) = 1^{st} (⟨R, S⟩)$
80		op1stg	$⊢ (R \in (X H Z) \land S \in (Y J W)) \to 1^{st} (⟨R, S⟩) = R$
81	13 14 80	syl2anc	$⊢ φ \to 1^{st} (⟨R, S⟩) = R$
82	78 79 81	3eqtrd	$⊢ φ \to (⟨X, Y⟩ 2^{nd} (C {1^{st}}_{F} D) ⟨Z, W⟩) (⟨R, S⟩) = R$
83	76 82	fveq12d	$⊢ φ \to (1^{st} (C {1^{st}}_{F} D) (⟨X, Y⟩) 2^{nd} (G) 1^{st} (C {1^{st}}_{F} D) (⟨Z, W⟩)) ((⟨X, Y⟩ 2^{nd} (C {1^{st}}_{F} D) ⟨Z, W⟩) (⟨R, S⟩)) = (X 2^{nd} (G) Z) (R)$
84	75 83	eqtrd	$⊢ φ \to (⟨X, Y⟩ 2^{nd} (G \circ_{func} (C {1^{st}}_{F} D)) ⟨Z, W⟩) (⟨R, S⟩) = (X 2^{nd} (G) Z) (R)$
85	20 21 38 26 2 30 36 37	2ndf2	$⊢ φ \to ⟨X, Y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨Z, W⟩ = {2^{nd} ↾}_{(⟨X, Y⟩ Hom (C \times_{c} D) ⟨Z, W⟩)}$
86	85	fveq1d	$⊢ φ \to (⟨X, Y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨Z, W⟩) (⟨R, S⟩) = ({2^{nd} ↾}_{(⟨X, Y⟩ Hom (C \times_{c} D) ⟨Z, W⟩)}) (⟨R, S⟩)$
87	41	fvresd	$⊢ φ \to ({2^{nd} ↾}_{(⟨X, Y⟩ Hom (C \times_{c} D) ⟨Z, W⟩)}) (⟨R, S⟩) = 2^{nd} (⟨R, S⟩)$
88		op2ndg	$⊢ (R \in (X H Z) \land S \in (Y J W)) \to 2^{nd} (⟨R, S⟩) = S$
89	13 14 88	syl2anc	$⊢ φ \to 2^{nd} (⟨R, S⟩) = S$
90	86 87 89	3eqtrd	$⊢ φ \to (⟨X, Y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨Z, W⟩) (⟨R, S⟩) = S$
91	84 90	opeq12d	$⊢ φ \to ⟨(⟨X, Y⟩ 2^{nd} (G \circ_{func} (C {1^{st}}_{F} D)) ⟨Z, W⟩) (⟨R, S⟩), (⟨X, Y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨Z, W⟩) (⟨R, S⟩)⟩ = ⟨(X 2^{nd} (G) Z) (R), S⟩$
92	74 91	eqtrd	$⊢ φ \to (⟨X, Y⟩ 2^{nd} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) ⟨Z, W⟩) (⟨R, S⟩) = ⟨(X 2^{nd} (G) Z) (R), S⟩$
93	73 92	fveq12d	$⊢ φ \to (1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨X, Y⟩) 2^{nd} (D {eval}_{F} E) 1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨Z, W⟩)) ((⟨X, Y⟩ 2^{nd} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) ⟨Z, W⟩) (⟨R, S⟩)) = (⟨1^{st} (G) (X), Y⟩ 2^{nd} (D {eval}_{F} E) ⟨1^{st} (G) (Z), W⟩) (⟨(X 2^{nd} (G) Z) (R), S⟩)$
94		df-ov	$⊢ (X 2^{nd} (G) Z) (R) (⟨1^{st} (G) (X), Y⟩ 2^{nd} (D {eval}_{F} E) ⟨1^{st} (G) (Z), W⟩) S = (⟨1^{st} (G) (X), Y⟩ 2^{nd} (D {eval}_{F} E) ⟨1^{st} (G) (Z), W⟩) (⟨(X 2^{nd} (G) Z) (R), S⟩)$
95	93 94	eqtr4di	$⊢ φ \to (1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨X, Y⟩) 2^{nd} (D {eval}_{F} E) 1^{st} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) (⟨Z, W⟩)) ((⟨X, Y⟩ 2^{nd} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) ⟨Z, W⟩) (⟨R, S⟩)) = (X 2^{nd} (G) Z) (R) (⟨1^{st} (G) (X), Y⟩ 2^{nd} (D {eval}_{F} E) ⟨1^{st} (G) (Z), W⟩) S$
96		eqid	$⊢ comp (E) = comp (E)$
97		eqid	$⊢ D Nat E = D Nat E$
98	34	fucbas	$⊢ D Func E = {Base}_{(D FuncCat E)}$
99		relfunc	$⊢ Rel (C Func (D FuncCat E))$
100		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)$
101	99 4 100	sylancr	$⊢ φ \to 1^{st} (G) (C Func (D FuncCat E)) 2^{nd} (G)$
102	5 98 101	funcf1	$⊢ φ \to 1^{st} (G) : A ⟶ D Func E$
103	102 7	ffvelcdmd	$⊢ φ \to 1^{st} (G) (X) \in (D Func E)$
104	102 11	ffvelcdmd	$⊢ φ \to 1^{st} (G) (Z) \in (D Func E)$
105		eqid	$⊢ ⟨1^{st} (G) (X), Y⟩ 2^{nd} (D {eval}_{F} E) ⟨1^{st} (G) (Z), W⟩ = ⟨1^{st} (G) (X), Y⟩ 2^{nd} (D {eval}_{F} E) ⟨1^{st} (G) (Z), W⟩$
106	34 97	fuchom	$⊢ D Nat E = Hom (D FuncCat E)$
107	5 9 106 101 7 11	funcf2	$⊢ φ \to (X 2^{nd} (G) Z) : X H Z ⟶ 1^{st} (G) (X) (D Nat E) 1^{st} (G) (Z)$
108	107 13	ffvelcdmd	$⊢ φ \to (X 2^{nd} (G) Z) (R) \in (1^{st} (G) (X) (D Nat E) 1^{st} (G) (Z))$
109	33 2 3 6 10 96 97 103 104 8 12 105 108 14	evlf2val	$⊢ φ \to (X 2^{nd} (G) Z) (R) (⟨1^{st} (G) (X), Y⟩ 2^{nd} (D {eval}_{F} E) ⟨1^{st} (G) (Z), W⟩) S = (X 2^{nd} (G) Z) (R) (W) (⟨1^{st} (1^{st} (G) (X)) (Y), 1^{st} (1^{st} (G) (X)) (W)⟩ comp (E) 1^{st} (1^{st} (G) (Z)) (W)) (Y 2^{nd} (1^{st} (G) (X)) W) (S)$
110	44 95 109	3eqtrd	$⊢ φ \to R (⟨X, Y⟩ 2^{nd} (F) ⟨Z, W⟩) S = (X 2^{nd} (G) Z) (R) (W) (⟨1^{st} (1^{st} (G) (X)) (Y), 1^{st} (1^{st} (G) (X)) (W)⟩ comp (E) 1^{st} (1^{st} (G) (Z)) (W)) (Y 2^{nd} (1^{st} (G) (X)) W) (S)$

Metamath Proof Explorer

Theorem uncf2

Proof