This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐸 ) )