Theorem 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	⊢ 𝐹 = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 )
	uncfval.c	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	uncfval.d	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	uncfval.f	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
Assertion	uncfcl	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		uncfval.g	⊢ 𝐹 = ( ⟨“ 𝐶 𝐷 𝐸 ”⟩ uncurryF 𝐺 )
2		uncfval.c	⊢ ( 𝜑 → 𝐷 ∈ Cat )
3		uncfval.d	⊢ ( 𝜑 → 𝐸 ∈ Cat )
4		uncfval.f	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) )
5	1 2 3 4	uncfval	⊢ ( 𝜑 → 𝐹 = ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) ) )
6		eqid	⊢ ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) = ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) )
7		eqid	⊢ ( ( 𝐷 FuncCat 𝐸 ) ×c 𝐷 ) = ( ( 𝐷 FuncCat 𝐸 ) ×c 𝐷 )
8		eqid	⊢ ( 𝐶 ×c 𝐷 ) = ( 𝐶 ×c 𝐷 )
9		funcrcl	⊢ ( 𝐺 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐸 ) ) → ( 𝐶 ∈ Cat ∧ ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) )
10	4 9	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( 𝐷 FuncCat 𝐸 ) ∈ Cat ) )
11	10	simpld	⊢ ( 𝜑 → 𝐶 ∈ Cat )
12		eqid	⊢ ( 𝐶 1stF 𝐷 ) = ( 𝐶 1stF 𝐷 )
13	8 11 2 12	1stfcl	⊢ ( 𝜑 → ( 𝐶 1stF 𝐷 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐶 ) )
14	13 4	cofucl	⊢ ( 𝜑 → ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ∈ ( ( 𝐶 ×c 𝐷 ) Func ( 𝐷 FuncCat 𝐸 ) ) )
15		eqid	⊢ ( 𝐶 2ndF 𝐷 ) = ( 𝐶 2ndF 𝐷 )
16	8 11 2 15	2ndfcl	⊢ ( 𝜑 → ( 𝐶 2ndF 𝐷 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐷 ) )
17	6 7 14 16	prfcl	⊢ ( 𝜑 → ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) ∈ ( ( 𝐶 ×c 𝐷 ) Func ( ( 𝐷 FuncCat 𝐸 ) ×c 𝐷 ) ) )
18		eqid	⊢ ( 𝐷 evalF 𝐸 ) = ( 𝐷 evalF 𝐸 )
19		eqid	⊢ ( 𝐷 FuncCat 𝐸 ) = ( 𝐷 FuncCat 𝐸 )
20	18 19 2 3	evlfcl	⊢ ( 𝜑 → ( 𝐷 evalF 𝐸 ) ∈ ( ( ( 𝐷 FuncCat 𝐸 ) ×c 𝐷 ) Func 𝐸 ) )
21	17 20	cofucl	⊢ ( 𝜑 → ( ( 𝐷 evalF 𝐸 ) ∘func ( ( 𝐺 ∘func ( 𝐶 1stF 𝐷 ) ) ⟨,⟩F ( 𝐶 2ndF 𝐷 ) ) ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )
22	5 21	eqeltrd	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐸 ) )