uncfcl

Description: The uncurry operation takes a functor F : C --> ( D --> E ) to a functor uncurryF ( F ) : C X. D --> E . (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))$
Assertion	uncfcl	$⊢ φ \to F \in ((C \times_{c} D) Func E)$

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	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))$
6		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)$
7		eqid	$⊢ (D FuncCat E) \times_{c} D = (D FuncCat E) \times_{c} D$
8		eqid	$⊢ C \times_{c} D = C \times_{c} D$
9		funcrcl	$⊢ G \in (C Func (D FuncCat E)) \to (C \in Cat \land D FuncCat E \in Cat)$
10	4 9	syl	$⊢ φ \to (C \in Cat \land D FuncCat E \in Cat)$
11	10	simpld	$⊢ φ \to C \in Cat$
12		eqid	$⊢ C {1^{st}}_{F} D = C {1^{st}}_{F} D$
13	8 11 2 12	1stfcl	$⊢ φ \to C {1^{st}}_{F} D \in ((C \times_{c} D) Func C)$
14	13 4	cofucl	$⊢ φ \to G \circ_{func} (C {1^{st}}_{F} D) \in ((C \times_{c} D) Func (D FuncCat E))$
15		eqid	$⊢ C {2^{nd}}_{F} D = C {2^{nd}}_{F} D$
16	8 11 2 15	2ndfcl	$⊢ φ \to C {2^{nd}}_{F} D \in ((C \times_{c} D) Func D)$
17	6 7 14 16	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))$
18		eqid	$⊢ D {eval}_{F} E = D {eval}_{F} E$
19		eqid	$⊢ D FuncCat E = D FuncCat E$
20	18 19 2 3	evlfcl	$⊢ φ \to D {eval}_{F} E \in (((D FuncCat E) \times_{c} D) Func E)$
21	17 20	cofucl	$⊢ φ \to (D {eval}_{F} E) \circ_{func} ((G \circ_{func} (C {1^{st}}_{F} D)) {⟨,⟩}_{F} (C {2^{nd}}_{F} D)) \in ((C \times_{c} D) Func E)$
22	5 21	eqeltrd	$⊢ φ \to F \in ((C \times_{c} D) Func E)$

Metamath Proof Explorer

Theorem uncfcl

Proof