uncfcurf

Description: Cancellation of uncurry with curry. (Contributed by Mario Carneiro, 13-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		uncfcurf.g	$⊢ G = ⟨C, D⟩ {curry}_{F} F$
2		uncfcurf.c	$⊢ φ \to C \in Cat$
3		uncfcurf.d	$⊢ φ \to D \in Cat$
4		uncfcurf.f	$⊢ φ \to F \in ((C \times_{c} D) Func E)$
5		eqid	$⊢ ⟨“ C D E ”⟩ {uncurry}_{F} G = ⟨“ C D E ”⟩ {uncurry}_{F} G$
6	3	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \to D \in Cat$
7		funcrcl	$⊢ F \in ((C \times_{c} D) Func E) \to (C \times_{c} D \in Cat \land E \in Cat)$
8	4 7	syl	$⊢ φ \to (C \times_{c} D \in Cat \land E \in Cat)$
9	8	simprd	$⊢ φ \to E \in Cat$
10	9	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \to E \in Cat$
11		eqid	$⊢ D FuncCat E = D FuncCat E$
12	1 11 2 3 4	curfcl	$⊢ φ \to G \in (C Func (D FuncCat E))$
13	12	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \to G \in (C Func (D FuncCat E))$
14		eqid	$⊢ {Base}_{C} = {Base}_{C}$
15		eqid	$⊢ {Base}_{D} = {Base}_{D}$
16		simprl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \to x \in {Base}_{C}$
17		simprr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \to y \in {Base}_{D}$
18	5 6 10 13 14 15 16 17	uncf1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \to x 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) y = 1^{st} (1^{st} (G) (x)) (y)$
19	2	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \to C \in Cat$
20	4	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \to F \in ((C \times_{c} D) Func E)$
21		eqid	$⊢ 1^{st} (G) (x) = 1^{st} (G) (x)$
22	1 14 19 6 20 15 16 21 17	curf11	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \to 1^{st} (1^{st} (G) (x)) (y) = x 1^{st} (F) y$
23	18 22	eqtrd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \to x 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) y = x 1^{st} (F) y$
24	23	ralrimivva	$⊢ φ \to \forall x \in {Base}_{C} \forall y \in {Base}_{D} x 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) y = x 1^{st} (F) y$
25		eqid	$⊢ C \times_{c} D = C \times_{c} D$
26	25 14 15	xpcbas	$⊢ {Base}_{C} \times {Base}_{D} = {Base}_{(C \times_{c} D)}$
27		eqid	$⊢ {Base}_{E} = {Base}_{E}$
28		relfunc	$⊢ Rel ((C \times_{c} D) Func E)$
29	5 3 9 12	uncfcl	$⊢ φ \to ⟨“ C D E ”⟩ {uncurry}_{F} G \in ((C \times_{c} D) Func E)$
30		1st2ndbr	$⊢ (Rel ((C \times_{c} D) Func E) \land ⟨“ C D E ”⟩ {uncurry}_{F} G \in ((C \times_{c} D) Func E)) \to 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) ((C \times_{c} D) Func E) 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G)$
31	28 29 30	sylancr	$⊢ φ \to 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) ((C \times_{c} D) Func E) 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G)$
32	26 27 31	funcf1	$⊢ φ \to 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) : {Base}_{C} \times {Base}_{D} ⟶ {Base}_{E}$
33	32	ffnd	$⊢ φ \to 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) Fn ({Base}_{C} \times {Base}_{D})$
34		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)$
35	28 4 34	sylancr	$⊢ φ \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
36	26 27 35	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{C} \times {Base}_{D} ⟶ {Base}_{E}$
37	36	ffnd	$⊢ φ \to 1^{st} (F) Fn ({Base}_{C} \times {Base}_{D})$
38		eqfnov2	$⊢ (1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) Fn ({Base}_{C} \times {Base}_{D}) \land 1^{st} (F) Fn ({Base}_{C} \times {Base}_{D})) \to (1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) = 1^{st} (F) \leftrightarrow \forall x \in {Base}_{C} \forall y \in {Base}_{D} x 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) y = x 1^{st} (F) y)$
39	33 37 38	syl2anc	$⊢ φ \to (1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) = 1^{st} (F) \leftrightarrow \forall x \in {Base}_{C} \forall y \in {Base}_{D} x 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) y = x 1^{st} (F) y)$
40	24 39	mpbird	$⊢ φ \to 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) = 1^{st} (F)$
41	3	ad3antrrr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to D \in Cat$
42	9	ad3antrrr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to E \in Cat$
43	12	ad3antrrr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to G \in (C Func (D FuncCat E))$
44	16	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to x \in {Base}_{C}$
45	44	adantr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to x \in {Base}_{C}$
46	17	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to y \in {Base}_{D}$
47	46	adantr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to y \in {Base}_{D}$
48		eqid	$⊢ Hom (C) = Hom (C)$
49		eqid	$⊢ Hom (D) = Hom (D)$
50		simprl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to z \in {Base}_{C}$
51	50	adantr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to z \in {Base}_{C}$
52		simprr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to w \in {Base}_{D}$
53	52	adantr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to w \in {Base}_{D}$
54		simprl	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to f \in (x Hom (C) z)$
55		simprr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to g \in (y Hom (D) w)$
56	5 41 42 43 14 15 45 47 48 49 51 53 54 55	uncf2	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to f (⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩) g = (x 2^{nd} (G) z) (f) (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) (g)$
57	2	ad3antrrr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to C \in Cat$
58	4	ad3antrrr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to F \in ((C \times_{c} D) Func E)$
59	1 14 57 41 58 15 45 21 47	curf11	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to 1^{st} (1^{st} (G) (x)) (y) = x 1^{st} (F) y$
60		df-ov	$⊢ x 1^{st} (F) y = 1^{st} (F) (⟨x, y⟩)$
61	59 60	eqtrdi	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to 1^{st} (1^{st} (G) (x)) (y) = 1^{st} (F) (⟨x, y⟩)$
62	1 14 57 41 58 15 45 21 53	curf11	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to 1^{st} (1^{st} (G) (x)) (w) = x 1^{st} (F) w$
63		df-ov	$⊢ x 1^{st} (F) w = 1^{st} (F) (⟨x, w⟩)$
64	62 63	eqtrdi	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to 1^{st} (1^{st} (G) (x)) (w) = 1^{st} (F) (⟨x, w⟩)$
65	61 64	opeq12d	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to ⟨1^{st} (1^{st} (G) (x)) (y), 1^{st} (1^{st} (G) (x)) (w)⟩ = ⟨1^{st} (F) (⟨x, y⟩), 1^{st} (F) (⟨x, w⟩)⟩$
66		eqid	$⊢ 1^{st} (G) (z) = 1^{st} (G) (z)$
67	1 14 57 41 58 15 51 66 53	curf11	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to 1^{st} (1^{st} (G) (z)) (w) = z 1^{st} (F) w$
68		df-ov	$⊢ z 1^{st} (F) w = 1^{st} (F) (⟨z, w⟩)$
69	67 68	eqtrdi	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to 1^{st} (1^{st} (G) (z)) (w) = 1^{st} (F) (⟨z, w⟩)$
70	65 69	oveq12d	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to ⟨1^{st} (1^{st} (G) (x)) (y), 1^{st} (1^{st} (G) (x)) (w)⟩ comp (E) 1^{st} (1^{st} (G) (z)) (w) = ⟨1^{st} (F) (⟨x, y⟩), 1^{st} (F) (⟨x, w⟩)⟩ comp (E) 1^{st} (F) (⟨z, w⟩)$
71		eqid	$⊢ Id (D) = Id (D)$
72		eqid	$⊢ (x 2^{nd} (G) z) (f) = (x 2^{nd} (G) z) (f)$
73	1 14 57 41 58 15 48 71 45 51 54 72 53	curf2val	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to (x 2^{nd} (G) z) (f) (w) = f (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) Id (D) (w)$
74		df-ov	$⊢ f (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) Id (D) (w) = (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) (⟨f, Id (D) (w)⟩)$
75	73 74	eqtrdi	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to (x 2^{nd} (G) z) (f) (w) = (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) (⟨f, Id (D) (w)⟩)$
76		eqid	$⊢ Id (C) = Id (C)$
77	1 14 57 41 58 15 45 21 47 49 76 53 55	curf12	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to (y 2^{nd} (1^{st} (G) (x)) w) (g) = Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, w⟩) g$
78		df-ov	$⊢ Id (C) (x) (⟨x, y⟩ 2^{nd} (F) ⟨x, w⟩) g = (⟨x, y⟩ 2^{nd} (F) ⟨x, w⟩) (⟨Id (C) (x), g⟩)$
79	77 78	eqtrdi	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to (y 2^{nd} (1^{st} (G) (x)) w) (g) = (⟨x, y⟩ 2^{nd} (F) ⟨x, w⟩) (⟨Id (C) (x), g⟩)$
80	70 75 79	oveq123d	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to (x 2^{nd} (G) z) (f) (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) (g) = (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) (⟨f, Id (D) (w)⟩) (⟨1^{st} (F) (⟨x, y⟩), 1^{st} (F) (⟨x, w⟩)⟩ comp (E) 1^{st} (F) (⟨z, w⟩)) (⟨x, y⟩ 2^{nd} (F) ⟨x, w⟩) (⟨Id (C) (x), g⟩)$
81		eqid	$⊢ Hom (C \times_{c} D) = Hom (C \times_{c} D)$
82		eqid	$⊢ comp (C \times_{c} D) = comp (C \times_{c} D)$
83		eqid	$⊢ comp (E) = comp (E)$
84	35	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
85	84	adantr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to 1^{st} (F) ((C \times_{c} D) Func E) 2^{nd} (F)$
86		opelxpi	$⊢ (x \in {Base}_{C} \land y \in {Base}_{D}) \to ⟨x, y⟩ \in ({Base}_{C} \times {Base}_{D})$
87	86	ad2antlr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to ⟨x, y⟩ \in ({Base}_{C} \times {Base}_{D})$
88	87	adantr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to ⟨x, y⟩ \in ({Base}_{C} \times {Base}_{D})$
89	45 53	opelxpd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to ⟨x, w⟩ \in ({Base}_{C} \times {Base}_{D})$
90		opelxpi	$⊢ (z \in {Base}_{C} \land w \in {Base}_{D}) \to ⟨z, w⟩ \in ({Base}_{C} \times {Base}_{D})$
91	90	adantl	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to ⟨z, w⟩ \in ({Base}_{C} \times {Base}_{D})$
92	91	adantr	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to ⟨z, w⟩ \in ({Base}_{C} \times {Base}_{D})$
93	14 48 76 57 45	catidcl	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to Id (C) (x) \in (x Hom (C) x)$
94	93 55	opelxpd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to ⟨Id (C) (x), g⟩ \in ((x Hom (C) x) \times (y Hom (D) w))$
95	25 14 15 48 49 45 47 45 53 81	xpchom2	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to ⟨x, y⟩ Hom (C \times_{c} D) ⟨x, w⟩ = (x Hom (C) x) \times (y Hom (D) w)$
96	94 95	eleqtrrd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to ⟨Id (C) (x), g⟩ \in (⟨x, y⟩ Hom (C \times_{c} D) ⟨x, w⟩)$
97	15 49 71 41 53	catidcl	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to Id (D) (w) \in (w Hom (D) w)$
98	54 97	opelxpd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to ⟨f, Id (D) (w)⟩ \in ((x Hom (C) z) \times (w Hom (D) w))$
99	25 14 15 48 49 45 53 51 53 81	xpchom2	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to ⟨x, w⟩ Hom (C \times_{c} D) ⟨z, w⟩ = (x Hom (C) z) \times (w Hom (D) w)$
100	98 99	eleqtrrd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to ⟨f, Id (D) (w)⟩ \in (⟨x, w⟩ Hom (C \times_{c} D) ⟨z, w⟩)$
101	26 81 82 83 85 88 89 92 96 100	funcco	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) (⟨f, Id (D) (w)⟩ (⟨⟨x, y⟩, ⟨x, w⟩⟩ comp (C \times_{c} D) ⟨z, w⟩) ⟨Id (C) (x), g⟩) = (⟨x, w⟩ 2^{nd} (F) ⟨z, w⟩) (⟨f, Id (D) (w)⟩) (⟨1^{st} (F) (⟨x, y⟩), 1^{st} (F) (⟨x, w⟩)⟩ comp (E) 1^{st} (F) (⟨z, w⟩)) (⟨x, y⟩ 2^{nd} (F) ⟨x, w⟩) (⟨Id (C) (x), g⟩)$
102		eqid	$⊢ comp (C) = comp (C)$
103		eqid	$⊢ comp (D) = comp (D)$
104	25 14 15 48 49 45 47 45 53 102 103 82 51 53 93 55 54 97	xpcco2	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to ⟨f, Id (D) (w)⟩ (⟨⟨x, y⟩, ⟨x, w⟩⟩ comp (C \times_{c} D) ⟨z, w⟩) ⟨Id (C) (x), g⟩ = ⟨f (⟨x, x⟩ comp (C) z) Id (C) (x), Id (D) (w) (⟨y, w⟩ comp (D) w) g⟩$
105	104	fveq2d	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) (⟨f, Id (D) (w)⟩ (⟨⟨x, y⟩, ⟨x, w⟩⟩ comp (C \times_{c} D) ⟨z, w⟩) ⟨Id (C) (x), g⟩) = (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) (⟨f (⟨x, x⟩ comp (C) z) Id (C) (x), Id (D) (w) (⟨y, w⟩ comp (D) w) g⟩)$
106		df-ov	$⊢ (f (⟨x, x⟩ comp (C) z) Id (C) (x)) (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) (Id (D) (w) (⟨y, w⟩ comp (D) w) g) = (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) (⟨f (⟨x, x⟩ comp (C) z) Id (C) (x), Id (D) (w) (⟨y, w⟩ comp (D) w) g⟩)$
107	105 106	eqtr4di	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) (⟨f, Id (D) (w)⟩ (⟨⟨x, y⟩, ⟨x, w⟩⟩ comp (C \times_{c} D) ⟨z, w⟩) ⟨Id (C) (x), g⟩) = (f (⟨x, x⟩ comp (C) z) Id (C) (x)) (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) (Id (D) (w) (⟨y, w⟩ comp (D) w) g)$
108	14 48 76 57 45 102 51 54	catrid	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to f (⟨x, x⟩ comp (C) z) Id (C) (x) = f$
109	15 49 71 41 47 103 53 55	catlid	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to Id (D) (w) (⟨y, w⟩ comp (D) w) g = g$
110	108 109	oveq12d	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to (f (⟨x, x⟩ comp (C) z) Id (C) (x)) (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) (Id (D) (w) (⟨y, w⟩ comp (D) w) g) = f (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) g$
111	107 110	eqtrd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) (⟨f, Id (D) (w)⟩ (⟨⟨x, y⟩, ⟨x, w⟩⟩ comp (C \times_{c} D) ⟨z, w⟩) ⟨Id (C) (x), g⟩) = f (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) g$
112	80 101 111	3eqtr2d	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to (x 2^{nd} (G) z) (f) (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) (g) = f (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) g$
113	56 112	eqtrd	$⊢ (((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \land (f \in (x Hom (C) z) \land g \in (y Hom (D) w))) \to f (⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩) g = f (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) g$
114	113	ralrimivva	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to \forall f \in (x Hom (C) z) \forall g \in (y Hom (D) w) f (⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩) g = f (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) g$
115		eqid	$⊢ Hom (E) = Hom (E)$
116	31	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) ((C \times_{c} D) Func E) 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G)$
117	26 81 115 116 87 91	funcf2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to (⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩) : ⟨x, y⟩ Hom (C \times_{c} D) ⟨z, w⟩ ⟶ 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) (⟨x, y⟩) Hom (E) 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) (⟨z, w⟩)$
118	25 14 15 48 49 44 46 50 52 81	xpchom2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to ⟨x, y⟩ Hom (C \times_{c} D) ⟨z, w⟩ = (x Hom (C) z) \times (y Hom (D) w)$
119	118	feq2d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to ((⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩) : ⟨x, y⟩ Hom (C \times_{c} D) ⟨z, w⟩ ⟶ 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) (⟨x, y⟩) Hom (E) 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) (⟨z, w⟩) \leftrightarrow (⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩) : (x Hom (C) z) \times (y Hom (D) w) ⟶ 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) (⟨x, y⟩) Hom (E) 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) (⟨z, w⟩))$
120	117 119	mpbid	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to (⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩) : (x Hom (C) z) \times (y Hom (D) w) ⟶ 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) (⟨x, y⟩) Hom (E) 1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G) (⟨z, w⟩)$
121	120	ffnd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to (⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩) Fn ((x Hom (C) z) \times (y Hom (D) w))$
122	26 81 115 84 87 91	funcf2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) : ⟨x, y⟩ Hom (C \times_{c} D) ⟨z, w⟩ ⟶ 1^{st} (F) (⟨x, y⟩) Hom (E) 1^{st} (F) (⟨z, w⟩)$
123	118	feq2d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to ((⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) : ⟨x, y⟩ Hom (C \times_{c} D) ⟨z, w⟩ ⟶ 1^{st} (F) (⟨x, y⟩) Hom (E) 1^{st} (F) (⟨z, w⟩) \leftrightarrow (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) : (x Hom (C) z) \times (y Hom (D) w) ⟶ 1^{st} (F) (⟨x, y⟩) Hom (E) 1^{st} (F) (⟨z, w⟩))$
124	122 123	mpbid	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) : (x Hom (C) z) \times (y Hom (D) w) ⟶ 1^{st} (F) (⟨x, y⟩) Hom (E) 1^{st} (F) (⟨z, w⟩)$
125	124	ffnd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) Fn ((x Hom (C) z) \times (y Hom (D) w))$
126		eqfnov2	$⊢ ((⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩) Fn ((x Hom (C) z) \times (y Hom (D) w)) \land (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) Fn ((x Hom (C) z) \times (y Hom (D) w))) \to (⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩ = ⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩ \leftrightarrow \forall f \in (x Hom (C) z) \forall g \in (y Hom (D) w) f (⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩) g = f (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) g)$
127	121 125 126	syl2anc	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to (⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩ = ⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩ \leftrightarrow \forall f \in (x Hom (C) z) \forall g \in (y Hom (D) w) f (⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩) g = f (⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩) g)$
128	114 127	mpbird	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \land (z \in {Base}_{C} \land w \in {Base}_{D})) \to ⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩ = ⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩$
129	128	ralrimivva	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{D})) \to \forall z \in {Base}_{C} \forall w \in {Base}_{D} ⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩ = ⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩$
130	129	ralrimivva	$⊢ φ \to \forall x \in {Base}_{C} \forall y \in {Base}_{D} \forall z \in {Base}_{C} \forall w \in {Base}_{D} ⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩ = ⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩$
131		oveq2	$⊢ v = ⟨z, w⟩ \to u 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) v = u 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩$
132		oveq2	$⊢ v = ⟨z, w⟩ \to u 2^{nd} (F) v = u 2^{nd} (F) ⟨z, w⟩$
133	131 132	eqeq12d	$⊢ v = ⟨z, w⟩ \to (u 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) v = u 2^{nd} (F) v \leftrightarrow u 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩ = u 2^{nd} (F) ⟨z, w⟩)$
134	133	ralxp	$⊢ \forall v \in ({Base}_{C} \times {Base}_{D}) u 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) v = u 2^{nd} (F) v \leftrightarrow \forall z \in {Base}_{C} \forall w \in {Base}_{D} u 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩ = u 2^{nd} (F) ⟨z, w⟩$
135		oveq1	$⊢ u = ⟨x, y⟩ \to u 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩ = ⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩$
136		oveq1	$⊢ u = ⟨x, y⟩ \to u 2^{nd} (F) ⟨z, w⟩ = ⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩$
137	135 136	eqeq12d	$⊢ u = ⟨x, y⟩ \to (u 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩ = u 2^{nd} (F) ⟨z, w⟩ \leftrightarrow ⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩ = ⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩)$
138	137	2ralbidv	$⊢ u = ⟨x, y⟩ \to (\forall z \in {Base}_{C} \forall w \in {Base}_{D} u 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩ = u 2^{nd} (F) ⟨z, w⟩ \leftrightarrow \forall z \in {Base}_{C} \forall w \in {Base}_{D} ⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩ = ⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩)$
139	134 138	bitrid	$⊢ u = ⟨x, y⟩ \to (\forall v \in ({Base}_{C} \times {Base}_{D}) u 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) v = u 2^{nd} (F) v \leftrightarrow \forall z \in {Base}_{C} \forall w \in {Base}_{D} ⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩ = ⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩)$
140	139	ralxp	$⊢ \forall u \in ({Base}_{C} \times {Base}_{D}) \forall v \in ({Base}_{C} \times {Base}_{D}) u 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) v = u 2^{nd} (F) v \leftrightarrow \forall x \in {Base}_{C} \forall y \in {Base}_{D} \forall z \in {Base}_{C} \forall w \in {Base}_{D} ⟨x, y⟩ 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) ⟨z, w⟩ = ⟨x, y⟩ 2^{nd} (F) ⟨z, w⟩$
141	130 140	sylibr	$⊢ φ \to \forall u \in ({Base}_{C} \times {Base}_{D}) \forall v \in ({Base}_{C} \times {Base}_{D}) u 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) v = u 2^{nd} (F) v$
142	26 31	funcfn2	$⊢ φ \to 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) Fn (({Base}_{C} \times {Base}_{D}) \times ({Base}_{C} \times {Base}_{D}))$
143	26 35	funcfn2	$⊢ φ \to 2^{nd} (F) Fn (({Base}_{C} \times {Base}_{D}) \times ({Base}_{C} \times {Base}_{D}))$
144		eqfnov2	$⊢ (2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) Fn (({Base}_{C} \times {Base}_{D}) \times ({Base}_{C} \times {Base}_{D})) \land 2^{nd} (F) Fn (({Base}_{C} \times {Base}_{D}) \times ({Base}_{C} \times {Base}_{D}))) \to (2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) = 2^{nd} (F) \leftrightarrow \forall u \in ({Base}_{C} \times {Base}_{D}) \forall v \in ({Base}_{C} \times {Base}_{D}) u 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) v = u 2^{nd} (F) v)$
145	142 143 144	syl2anc	$⊢ φ \to (2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) = 2^{nd} (F) \leftrightarrow \forall u \in ({Base}_{C} \times {Base}_{D}) \forall v \in ({Base}_{C} \times {Base}_{D}) u 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) v = u 2^{nd} (F) v)$
146	141 145	mpbird	$⊢ φ \to 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G) = 2^{nd} (F)$
147	40 146	opeq12d	$⊢ φ \to ⟨1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G), 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G)⟩ = ⟨1^{st} (F), 2^{nd} (F)⟩$
148		1st2nd	$⊢ (Rel ((C \times_{c} D) Func E) \land ⟨“ C D E ”⟩ {uncurry}_{F} G \in ((C \times_{c} D) Func E)) \to ⟨“ C D E ”⟩ {uncurry}_{F} G = ⟨1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G), 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G)⟩$
149	28 29 148	sylancr	$⊢ φ \to ⟨“ C D E ”⟩ {uncurry}_{F} G = ⟨1^{st} (⟨“ C D E ”⟩ {uncurry}_{F} G), 2^{nd} (⟨“ C D E ”⟩ {uncurry}_{F} G)⟩$
150		1st2nd	$⊢ (Rel ((C \times_{c} D) Func E) \land F \in ((C \times_{c} D) Func E)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
151	28 4 150	sylancr	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
152	147 149 151	3eqtr4d	$⊢ φ \to ⟨“ C D E ”⟩ {uncurry}_{F} G = F$

Metamath Proof Explorer

Theorem uncfcurf

Proof