curf2ndf

Description: As shown in diagval , the currying of the first projection is the diagonal functor. On the other hand, the currying of the second projection is x e. C |-> ( y e. D |-> y ) , which is a constant functor of the identity functor at D . (Contributed by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	curf2ndf.q	$⊢ Q = D FuncCat D$
	curf2ndf.c	$⊢ φ \to C \in Cat$
	curf2ndf.d	$⊢ φ \to D \in Cat$
Assertion	curf2ndf	$⊢ φ \to ⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D) = 1^{st} (Q Δ_{func} C) ({id}_{func} (D))$

Proof

Step	Hyp	Ref	Expression
1		curf2ndf.q	$⊢ Q = D FuncCat D$
2		curf2ndf.c	$⊢ φ \to C \in Cat$
3		curf2ndf.d	$⊢ φ \to D \in Cat$
4		df-ov	$⊢ x 1^{st} (C {2^{nd}}_{F} D) y = 1^{st} (C {2^{nd}}_{F} D) (⟨x, y⟩)$
5		eqid	$⊢ C \times_{c} D = C \times_{c} D$
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7		eqid	$⊢ {Base}_{D} = {Base}_{D}$
8	5 6 7	xpcbas	$⊢ {Base}_{C} \times {Base}_{D} = {Base}_{(C \times_{c} D)}$
9		eqid	$⊢ Hom (C \times_{c} D) = Hom (C \times_{c} D)$
10	2	ad2antrr	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to C \in Cat$
11	3	ad2antrr	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to D \in Cat$
12		eqid	$⊢ C {2^{nd}}_{F} D = C {2^{nd}}_{F} D$
13		opelxpi	$⊢ (x \in {Base}_{C} \land y \in {Base}_{D}) \to ⟨x, y⟩ \in ({Base}_{C} \times {Base}_{D})$
14	13	adantll	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to ⟨x, y⟩ \in ({Base}_{C} \times {Base}_{D})$
15	5 8 9 10 11 12 14	2ndf1	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to 1^{st} (C {2^{nd}}_{F} D) (⟨x, y⟩) = 2^{nd} (⟨x, y⟩)$
16		vex	$⊢ x \in V$
17		vex	$⊢ y \in V$
18	16 17	op2nd	$⊢ 2^{nd} (⟨x, y⟩) = y$
19	15 18	eqtrdi	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to 1^{st} (C {2^{nd}}_{F} D) (⟨x, y⟩) = y$
20	4 19	syl5eq	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \to x 1^{st} (C {2^{nd}}_{F} D) y = y$
21	20	mpteq2dva	$⊢ (φ \land x \in {Base}_{C}) \to (y \in {Base}_{D} ⟼ x 1^{st} (C {2^{nd}}_{F} D) y) = (y \in {Base}_{D} ⟼ y)$
22		mptresid	$⊢ {I ↾}_{{Base}_{D}} = (y \in {Base}_{D} ⟼ y)$
23	21 22	eqtr4di	$⊢ (φ \land x \in {Base}_{C}) \to (y \in {Base}_{D} ⟼ x 1^{st} (C {2^{nd}}_{F} D) y) = {I ↾}_{{Base}_{D}}$
24		df-ov	$⊢ Id (C) (x) (⟨x, y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨x, z⟩) f = (⟨x, y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨x, z⟩) (⟨Id (C) (x), f⟩)$
25	10	ad2antrr	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to C \in Cat$
26	11	ad2antrr	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to D \in Cat$
27	14	ad2antrr	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to ⟨x, y⟩ \in ({Base}_{C} \times {Base}_{D})$
28		simp-4r	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to x \in {Base}_{C}$
29		simplr	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to z \in {Base}_{D}$
30	28 29	opelxpd	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to ⟨x, z⟩ \in ({Base}_{C} \times {Base}_{D})$
31	5 8 9 25 26 12 27 30	2ndf2	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to ⟨x, y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨x, z⟩ = {2^{nd} ↾}_{(⟨x, y⟩ Hom (C \times_{c} D) ⟨x, z⟩)}$
32	31	fveq1d	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to (⟨x, y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨x, z⟩) (⟨Id (C) (x), f⟩) = ({2^{nd} ↾}_{(⟨x, y⟩ Hom (C \times_{c} D) ⟨x, z⟩)}) (⟨Id (C) (x), f⟩)$
33	24 32	syl5eq	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to Id (C) (x) (⟨x, y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨x, z⟩) f = ({2^{nd} ↾}_{(⟨x, y⟩ Hom (C \times_{c} D) ⟨x, z⟩)}) (⟨Id (C) (x), f⟩)$
34		eqid	$⊢ Hom (C) = Hom (C)$
35		eqid	$⊢ Id (C) = Id (C)$
36	2	adantr	$⊢ (φ \land x \in {Base}_{C}) \to C \in Cat$
37		simpr	$⊢ (φ \land x \in {Base}_{C}) \to x \in {Base}_{C}$
38	6 34 35 36 37	catidcl	$⊢ (φ \land x \in {Base}_{C}) \to Id (C) (x) \in (x Hom (C) x)$
39	38	ad5ant12	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to Id (C) (x) \in (x Hom (C) x)$
40		simpr	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to f \in (y Hom (D) z)$
41	39 40	opelxpd	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to ⟨Id (C) (x), f⟩ \in ((x Hom (C) x) \times (y Hom (D) z))$
42		eqid	$⊢ Hom (D) = Hom (D)$
43		simpllr	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to y \in {Base}_{D}$
44	5 6 7 34 42 28 43 28 29 9	xpchom2	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to ⟨x, y⟩ Hom (C \times_{c} D) ⟨x, z⟩ = (x Hom (C) x) \times (y Hom (D) z)$
45	41 44	eleqtrrd	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to ⟨Id (C) (x), f⟩ \in (⟨x, y⟩ Hom (C \times_{c} D) ⟨x, z⟩)$
46	45	fvresd	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to ({2^{nd} ↾}_{(⟨x, y⟩ Hom (C \times_{c} D) ⟨x, z⟩)}) (⟨Id (C) (x), f⟩) = 2^{nd} (⟨Id (C) (x), f⟩)$
47		fvex	$⊢ Id (C) (x) \in V$
48		vex	$⊢ f \in V$
49	47 48	op2nd	$⊢ 2^{nd} (⟨Id (C) (x), f⟩) = f$
50	46 49	eqtrdi	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to ({2^{nd} ↾}_{(⟨x, y⟩ Hom (C \times_{c} D) ⟨x, z⟩)}) (⟨Id (C) (x), f⟩) = f$
51	33 50	eqtrd	$⊢ ((((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \land f \in (y Hom (D) z)) \to Id (C) (x) (⟨x, y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨x, z⟩) f = f$
52	51	mpteq2dva	$⊢ (((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \to (f \in (y Hom (D) z) ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨x, z⟩) f) = (f \in (y Hom (D) z) ⟼ f)$
53		mptresid	$⊢ {I ↾}_{(y Hom (D) z)} = (f \in (y Hom (D) z) ⟼ f)$
54	52 53	eqtr4di	$⊢ (((φ \land x \in {Base}_{C}) \land y \in {Base}_{D}) \land z \in {Base}_{D}) \to (f \in (y Hom (D) z) ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨x, z⟩) f) = {I ↾}_{(y Hom (D) z)}$
55	54	3impa	$⊢ ((φ \land x \in {Base}_{C}) \land y \in {Base}_{D} \land z \in {Base}_{D}) \to (f \in (y Hom (D) z) ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨x, z⟩) f) = {I ↾}_{(y Hom (D) z)}$
56	55	mpoeq3dva	$⊢ (φ \land x \in {Base}_{C}) \to (y \in {Base}_{D}, z \in {Base}_{D} ⟼ (f \in (y Hom (D) z) ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨x, z⟩) f)) = (y \in {Base}_{D}, z \in {Base}_{D} ⟼ {I ↾}_{(y Hom (D) z)})$
57		fveq2	$⊢ u = ⟨y, z⟩ \to Hom (D) (u) = Hom (D) (⟨y, z⟩)$
58		df-ov	$⊢ y Hom (D) z = Hom (D) (⟨y, z⟩)$
59	57 58	eqtr4di	$⊢ u = ⟨y, z⟩ \to Hom (D) (u) = y Hom (D) z$
60	59	reseq2d	$⊢ u = ⟨y, z⟩ \to {I ↾}_{Hom (D) (u)} = {I ↾}_{(y Hom (D) z)}$
61	60	mpompt	$⊢ (u \in ({Base}_{D} \times {Base}_{D}) ⟼ {I ↾}_{Hom (D) (u)}) = (y \in {Base}_{D}, z \in {Base}_{D} ⟼ {I ↾}_{(y Hom (D) z)})$
62	56 61	eqtr4di	$⊢ (φ \land x \in {Base}_{C}) \to (y \in {Base}_{D}, z \in {Base}_{D} ⟼ (f \in (y Hom (D) z) ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨x, z⟩) f)) = (u \in ({Base}_{D} \times {Base}_{D}) ⟼ {I ↾}_{Hom (D) (u)})$
63	23 62	opeq12d	$⊢ (φ \land x \in {Base}_{C}) \to ⟨(y \in {Base}_{D} ⟼ x 1^{st} (C {2^{nd}}_{F} D) y), (y \in {Base}_{D}, z \in {Base}_{D} ⟼ (f \in (y Hom (D) z) ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨x, z⟩) f))⟩ = ⟨{I ↾}_{{Base}_{D}}, (u \in ({Base}_{D} \times {Base}_{D}) ⟼ {I ↾}_{Hom (D) (u)})⟩$
64		eqid	$⊢ ⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D) = ⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)$
65	3	adantr	$⊢ (φ \land x \in {Base}_{C}) \to D \in Cat$
66	5 2 3 12	2ndfcl	$⊢ φ \to C {2^{nd}}_{F} D \in ((C \times_{c} D) Func D)$
67	66	adantr	$⊢ (φ \land x \in {Base}_{C}) \to C {2^{nd}}_{F} D \in ((C \times_{c} D) Func D)$
68		eqid	$⊢ 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) (x) = 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) (x)$
69	64 6 36 65 67 7 37 68 42 35	curf1	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) (x) = ⟨(y \in {Base}_{D} ⟼ x 1^{st} (C {2^{nd}}_{F} D) y), (y \in {Base}_{D}, z \in {Base}_{D} ⟼ (f \in (y Hom (D) z) ⟼ Id (C) (x) (⟨x, y⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨x, z⟩) f))⟩$
70		eqid	$⊢ {id}_{func} (D) = {id}_{func} (D)$
71	70 7 65 42	idfuval	$⊢ (φ \land x \in {Base}_{C}) \to {id}_{func} (D) = ⟨{I ↾}_{{Base}_{D}}, (u \in ({Base}_{D} \times {Base}_{D}) ⟼ {I ↾}_{Hom (D) (u)})⟩$
72	63 69 71	3eqtr4d	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) (x) = {id}_{func} (D)$
73		eqid	$⊢ Q Δ_{func} C = Q Δ_{func} C$
74	1 3 3	fuccat	$⊢ φ \to Q \in Cat$
75	74	adantr	$⊢ (φ \land x \in {Base}_{C}) \to Q \in Cat$
76	1	fucbas	$⊢ D Func D = {Base}_{Q}$
77	70	idfucl	$⊢ D \in Cat \to {id}_{func} (D) \in (D Func D)$
78	3 77	syl	$⊢ φ \to {id}_{func} (D) \in (D Func D)$
79	78	adantr	$⊢ (φ \land x \in {Base}_{C}) \to {id}_{func} (D) \in (D Func D)$
80		eqid	$⊢ 1^{st} (Q Δ_{func} C) ({id}_{func} (D)) = 1^{st} (Q Δ_{func} C) ({id}_{func} (D))$
81	73 75 36 76 79 80 6 37	diag11	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) (x) = {id}_{func} (D)$
82	72 81	eqtr4d	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) (x) = 1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) (x)$
83	82	mpteq2dva	$⊢ φ \to (x \in {Base}_{C} ⟼ 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) (x)) = (x \in {Base}_{C} ⟼ 1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) (x))$
84		relfunc	$⊢ Rel (C Func Q)$
85	64 1 2 3 66	curfcl	$⊢ φ \to ⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D) \in (C Func Q)$
86		1st2ndbr	$⊢ (Rel (C Func Q) \land ⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D) \in (C Func Q)) \to 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) (C Func Q) 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D))$
87	84 85 86	sylancr	$⊢ φ \to 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) (C Func Q) 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D))$
88	6 76 87	funcf1	$⊢ φ \to 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) : {Base}_{C} ⟶ D Func D$
89	88	feqmptd	$⊢ φ \to 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) = (x \in {Base}_{C} ⟼ 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) (x))$
90	73 74 2 76 78 80	diag1cl	$⊢ φ \to 1^{st} (Q Δ_{func} C) ({id}_{func} (D)) \in (C Func Q)$
91		1st2ndbr	$⊢ (Rel (C Func Q) \land 1^{st} (Q Δ_{func} C) ({id}_{func} (D)) \in (C Func Q)) \to 1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) (C Func Q) 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D)))$
92	84 90 91	sylancr	$⊢ φ \to 1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) (C Func Q) 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D)))$
93	6 76 92	funcf1	$⊢ φ \to 1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) : {Base}_{C} ⟶ D Func D$
94	93	feqmptd	$⊢ φ \to 1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) = (x \in {Base}_{C} ⟼ 1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) (x))$
95	83 89 94	3eqtr4d	$⊢ φ \to 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) = 1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D)))$
96	3	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to D \in Cat$
97	70 7 96	idfu1st	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to 1^{st} ({id}_{func} (D)) = {I ↾}_{{Base}_{D}}$
98	97	coeq2d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to Id (D) \circ 1^{st} ({id}_{func} (D)) = Id (D) \circ ({I ↾}_{{Base}_{D}})$
99		eqid	$⊢ Id (Q) = Id (Q)$
100		eqid	$⊢ Id (D) = Id (D)$
101	78	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to {id}_{func} (D) \in (D Func D)$
102	1 99 100 101	fucid	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to Id (Q) ({id}_{func} (D)) = Id (D) \circ 1^{st} ({id}_{func} (D))$
103	7 100	cidfn	$⊢ D \in Cat \to Id (D) Fn {Base}_{D}$
104	96 103	syl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to Id (D) Fn {Base}_{D}$
105		dffn2	$⊢ Id (D) Fn {Base}_{D} \leftrightarrow Id (D) : {Base}_{D} ⟶ V$
106	104 105	sylib	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to Id (D) : {Base}_{D} ⟶ V$
107	106	feqmptd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to Id (D) = (z \in {Base}_{D} ⟼ Id (D) (z))$
108		fcoi1	$⊢ Id (D) : {Base}_{D} ⟶ V \to Id (D) \circ ({I ↾}_{{Base}_{D}}) = Id (D)$
109	106 108	syl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to Id (D) \circ ({I ↾}_{{Base}_{D}}) = Id (D)$
110	2	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to C \in Cat$
111	110	adantr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to C \in Cat$
112	96	adantr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to D \in Cat$
113		simplrl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to x \in {Base}_{C}$
114		opelxpi	$⊢ (x \in {Base}_{C} \land z \in {Base}_{D}) \to ⟨x, z⟩ \in ({Base}_{C} \times {Base}_{D})$
115	113 114	sylan	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to ⟨x, z⟩ \in ({Base}_{C} \times {Base}_{D})$
116		simplrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to y \in {Base}_{C}$
117		opelxpi	$⊢ (y \in {Base}_{C} \land z \in {Base}_{D}) \to ⟨y, z⟩ \in ({Base}_{C} \times {Base}_{D})$
118	116 117	sylan	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to ⟨y, z⟩ \in ({Base}_{C} \times {Base}_{D})$
119	5 8 9 111 112 12 115 118	2ndf2	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to ⟨x, z⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨y, z⟩ = {2^{nd} ↾}_{(⟨x, z⟩ Hom (C \times_{c} D) ⟨y, z⟩)}$
120	119	oveqd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to f (⟨x, z⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨y, z⟩) Id (D) (z) = f ({2^{nd} ↾}_{(⟨x, z⟩ Hom (C \times_{c} D) ⟨y, z⟩)}) Id (D) (z)$
121		df-ov	$⊢ f ({2^{nd} ↾}_{(⟨x, z⟩ Hom (C \times_{c} D) ⟨y, z⟩)}) Id (D) (z) = ({2^{nd} ↾}_{(⟨x, z⟩ Hom (C \times_{c} D) ⟨y, z⟩)}) (⟨f, Id (D) (z)⟩)$
122		simplr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to f \in (x Hom (C) y)$
123		simpr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to z \in {Base}_{D}$
124	7 42 100 112 123	catidcl	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to Id (D) (z) \in (z Hom (D) z)$
125	122 124	opelxpd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to ⟨f, Id (D) (z)⟩ \in ((x Hom (C) y) \times (z Hom (D) z))$
126	113	adantr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to x \in {Base}_{C}$
127	116	adantr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to y \in {Base}_{C}$
128	5 6 7 34 42 126 123 127 123 9	xpchom2	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to ⟨x, z⟩ Hom (C \times_{c} D) ⟨y, z⟩ = (x Hom (C) y) \times (z Hom (D) z)$
129	125 128	eleqtrrd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to ⟨f, Id (D) (z)⟩ \in (⟨x, z⟩ Hom (C \times_{c} D) ⟨y, z⟩)$
130	129	fvresd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to ({2^{nd} ↾}_{(⟨x, z⟩ Hom (C \times_{c} D) ⟨y, z⟩)}) (⟨f, Id (D) (z)⟩) = 2^{nd} (⟨f, Id (D) (z)⟩)$
131	121 130	syl5eq	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to f ({2^{nd} ↾}_{(⟨x, z⟩ Hom (C \times_{c} D) ⟨y, z⟩)}) Id (D) (z) = 2^{nd} (⟨f, Id (D) (z)⟩)$
132		fvex	$⊢ Id (D) (z) \in V$
133	48 132	op2nd	$⊢ 2^{nd} (⟨f, Id (D) (z)⟩) = Id (D) (z)$
134	131 133	eqtrdi	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to f ({2^{nd} ↾}_{(⟨x, z⟩ Hom (C \times_{c} D) ⟨y, z⟩)}) Id (D) (z) = Id (D) (z)$
135	120 134	eqtrd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \land z \in {Base}_{D}) \to f (⟨x, z⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨y, z⟩) Id (D) (z) = Id (D) (z)$
136	135	mpteq2dva	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (z \in {Base}_{D} ⟼ f (⟨x, z⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨y, z⟩) Id (D) (z)) = (z \in {Base}_{D} ⟼ Id (D) (z))$
137	107 109 136	3eqtr4rd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (z \in {Base}_{D} ⟼ f (⟨x, z⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨y, z⟩) Id (D) (z)) = Id (D) \circ ({I ↾}_{{Base}_{D}})$
138	98 102 137	3eqtr4rd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (z \in {Base}_{D} ⟼ f (⟨x, z⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨y, z⟩) Id (D) (z)) = Id (Q) ({id}_{func} (D))$
139	66	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to C {2^{nd}}_{F} D \in ((C \times_{c} D) Func D)$
140		simpr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to f \in (x Hom (C) y)$
141		eqid	$⊢ (x 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) y) (f) = (x 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) y) (f)$
142	64 6 110 96 139 7 34 100 113 116 140 141	curf2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) y) (f) = (z \in {Base}_{D} ⟼ f (⟨x, z⟩ 2^{nd} (C {2^{nd}}_{F} D) ⟨y, z⟩) Id (D) (z))$
143	74	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to Q \in Cat$
144	73 143 110 76 101 80 6 113 34 99 116 140	diag12	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) y) (f) = Id (Q) ({id}_{func} (D))$
145	138 142 144	3eqtr4d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) y) (f) = (x 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) y) (f)$
146	145	mpteq2dva	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (f \in (x Hom (C) y) ⟼ (x 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) y) (f)) = (f \in (x Hom (C) y) ⟼ (x 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) y) (f))$
147		eqid	$⊢ D Nat D = D Nat D$
148	1 147	fuchom	$⊢ D Nat D = Hom (Q)$
149	87	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) (C Func Q) 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D))$
150		simprl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \in {Base}_{C}$
151		simprr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to y \in {Base}_{C}$
152	6 34 148 149 150 151	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) y) : x Hom (C) y ⟶ 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) (x) (D Nat D) 1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) (y)$
153	152	feqmptd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) y = (f \in (x Hom (C) y) ⟼ (x 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) y) (f))$
154	92	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) (C Func Q) 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D)))$
155	6 34 148 154 150 151	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) y) : x Hom (C) y ⟶ 1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) (x) (D Nat D) 1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) (y)$
156	155	feqmptd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) y = (f \in (x Hom (C) y) ⟼ (x 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) y) (f))$
157	146 153 156	3eqtr4d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) y = x 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) y$
158	157	3impb	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to x 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) y = x 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) y$
159	158	mpoeq3dva	$⊢ φ \to (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) y) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) y)$
160	6 87	funcfn2	$⊢ φ \to 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) Fn ({Base}_{C} \times {Base}_{C})$
161		fnov	$⊢ 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) Fn ({Base}_{C} \times {Base}_{C}) \leftrightarrow 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) y)$
162	160 161	sylib	$⊢ φ \to 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) y)$
163	6 92	funcfn2	$⊢ φ \to 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) Fn ({Base}_{C} \times {Base}_{C})$
164		fnov	$⊢ 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) Fn ({Base}_{C} \times {Base}_{C}) \leftrightarrow 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) y)$
165	163 164	sylib	$⊢ φ \to 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))) y)$
166	159 162 165	3eqtr4d	$⊢ φ \to 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)) = 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D)))$
167	95 166	opeq12d	$⊢ φ \to ⟨1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)), 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D))⟩ = ⟨1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))), 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D)))⟩$
168		1st2nd	$⊢ (Rel (C Func Q) \land ⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D) \in (C Func Q)) \to ⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D) = ⟨1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)), 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D))⟩$
169	84 85 168	sylancr	$⊢ φ \to ⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D) = ⟨1^{st} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D)), 2^{nd} (⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D))⟩$
170		1st2nd	$⊢ (Rel (C Func Q) \land 1^{st} (Q Δ_{func} C) ({id}_{func} (D)) \in (C Func Q)) \to 1^{st} (Q Δ_{func} C) ({id}_{func} (D)) = ⟨1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))), 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D)))⟩$
171	84 90 170	sylancr	$⊢ φ \to 1^{st} (Q Δ_{func} C) ({id}_{func} (D)) = ⟨1^{st} (1^{st} (Q Δ_{func} C) ({id}_{func} (D))), 2^{nd} (1^{st} (Q Δ_{func} C) ({id}_{func} (D)))⟩$
172	167 169 171	3eqtr4d	$⊢ φ \to ⟨C, D⟩ {curry}_{F} (C {2^{nd}}_{F} D) = 1^{st} (Q Δ_{func} C) ({id}_{func} (D))$

Metamath Proof Explorer

Theorem curf2ndf

Proof