Definition df-prcof 49148

Description: Definition of pre-composition functors. The object part of the pre-composition functor given by 𝐹 pre-composes a functor with 𝐹; the morphism part pre-composes a natural transformation with the object part of 𝐹, in terms of function composition. Comments before the definition in § 3 of Chapter X in p. 236 of Mac Lane, Saunders, Categories for the Working Mathematician, 2nd Edition, Springer Science+Business Media, New York, (1998) [QA169.M33 1998]; available at https://math.mit.edu/~hrm/palestine/maclane-categories.pdf (retrieved 3 Nov 2025). The notation −∘_F is inspired by this page: https://1lab.dev/Cat.Functor.Compose.html.

The pre-composition functor can also be defined as a transposed curry of the functor composition bifunctor (precofval3 49145). But such definition requires an explicit third category. prcoftposcurfuco 49156 and prcoftposcurfucoa 49157 prove the equivalence. (Contributed by Zhi Wang, 2-Nov-2025.)

Assertion

Ref	Expression
df-prcof	⊢ −∘F = (𝑝 ∈ V, 𝑓 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑑⦌⦋(2nd ‘𝑝) / 𝑒⦌⦋(𝑑 Func 𝑒) / 𝑏⦌⟨(𝑘 ∈ 𝑏 ↦ (𝑘 ∘func 𝑓)), (𝑘 ∈ 𝑏, 𝑙 ∈ 𝑏 ↦ (𝑎 ∈ (𝑘(𝑑 Nat 𝑒)𝑙) ↦ (𝑎 ∘ (1st ‘𝑓))))⟩)

Distinct variable group:   𝑎,𝑏,𝑑,𝑒,𝑓,𝑘,𝑙,𝑝

Detailed syntax breakdown of Definition df-prcof

Step	Hyp	Ref	Expression
1		cprcof 49147	. 2 class −∘F
2		vp	. . 3 setvar 𝑝
3		vf	. . 3 setvar 𝑓
4		cvv 3457	. . 3 class V
5		vd	. . . 4 setvar 𝑑
6	2	cv 1538	. . . . 5 class 𝑝
7		c1st 7981	. . . . 5 class 1st
8	6, 7	cfv 6528	. . . 4 class (1st ‘𝑝)
9		ve	. . . . 5 setvar 𝑒
10		c2nd 7982	. . . . . 6 class 2nd
11	6, 10	cfv 6528	. . . . 5 class (2nd ‘𝑝)
12		vb	. . . . . 6 setvar 𝑏
13	5	cv 1538	. . . . . . 7 class 𝑑
14	9	cv 1538	. . . . . . 7 class 𝑒
15		cfunc 17854	. . . . . . 7 class Func
16	13, 14, 15	co 7400	. . . . . 6 class (𝑑 Func 𝑒)
17		vk	. . . . . . . 8 setvar 𝑘
18	12	cv 1538	. . . . . . . 8 class 𝑏
19	17	cv 1538	. . . . . . . . 9 class 𝑘
20	3	cv 1538	. . . . . . . . 9 class 𝑓
21		ccofu 17856	. . . . . . . . 9 class ∘func
22	19, 20, 21	co 7400	. . . . . . . 8 class (𝑘 ∘func 𝑓)
23	17, 18, 22	cmpt 5199	. . . . . . 7 class (𝑘 ∈ 𝑏 ↦ (𝑘 ∘func 𝑓))
24		vl	. . . . . . . 8 setvar 𝑙
25		va	. . . . . . . . 9 setvar 𝑎
26	24	cv 1538	. . . . . . . . . 10 class 𝑙
27		cnat 17944	. . . . . . . . . . 11 class Nat
28	13, 14, 27	co 7400	. . . . . . . . . 10 class (𝑑 Nat 𝑒)
29	19, 26, 28	co 7400	. . . . . . . . 9 class (𝑘(𝑑 Nat 𝑒)𝑙)
30	25	cv 1538	. . . . . . . . . 10 class 𝑎
31	20, 7	cfv 6528	. . . . . . . . . 10 class (1st ‘𝑓)
32	30, 31	ccom 5656	. . . . . . . . 9 class (𝑎 ∘ (1st ‘𝑓))
33	25, 29, 32	cmpt 5199	. . . . . . . 8 class (𝑎 ∈ (𝑘(𝑑 Nat 𝑒)𝑙) ↦ (𝑎 ∘ (1st ‘𝑓)))
34	17, 24, 18, 18, 33	cmpo 7402	. . . . . . 7 class (𝑘 ∈ 𝑏, 𝑙 ∈ 𝑏 ↦ (𝑎 ∈ (𝑘(𝑑 Nat 𝑒)𝑙) ↦ (𝑎 ∘ (1st ‘𝑓))))
35	23, 34	cop 4605	. . . . . 6 class ⟨(𝑘 ∈ 𝑏 ↦ (𝑘 ∘func 𝑓)), (𝑘 ∈ 𝑏, 𝑙 ∈ 𝑏 ↦ (𝑎 ∈ (𝑘(𝑑 Nat 𝑒)𝑙) ↦ (𝑎 ∘ (1st ‘𝑓))))⟩
36	12, 16, 35	csb 3872	. . . . 5 class ⦋(𝑑 Func 𝑒) / 𝑏⦌⟨(𝑘 ∈ 𝑏 ↦ (𝑘 ∘func 𝑓)), (𝑘 ∈ 𝑏, 𝑙 ∈ 𝑏 ↦ (𝑎 ∈ (𝑘(𝑑 Nat 𝑒)𝑙) ↦ (𝑎 ∘ (1st ‘𝑓))))⟩
37	9, 11, 36	csb 3872	. . . 4 class ⦋(2nd ‘𝑝) / 𝑒⦌⦋(𝑑 Func 𝑒) / 𝑏⦌⟨(𝑘 ∈ 𝑏 ↦ (𝑘 ∘func 𝑓)), (𝑘 ∈ 𝑏, 𝑙 ∈ 𝑏 ↦ (𝑎 ∈ (𝑘(𝑑 Nat 𝑒)𝑙) ↦ (𝑎 ∘ (1st ‘𝑓))))⟩
38	5, 8, 37	csb 3872	. . 3 class ⦋(1st ‘𝑝) / 𝑑⦌⦋(2nd ‘𝑝) / 𝑒⦌⦋(𝑑 Func 𝑒) / 𝑏⦌⟨(𝑘 ∈ 𝑏 ↦ (𝑘 ∘func 𝑓)), (𝑘 ∈ 𝑏, 𝑙 ∈ 𝑏 ↦ (𝑎 ∈ (𝑘(𝑑 Nat 𝑒)𝑙) ↦ (𝑎 ∘ (1st ‘𝑓))))⟩
39	2, 3, 4, 4, 38	cmpo 7402	. 2 class (𝑝 ∈ V, 𝑓 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑑⦌⦋(2nd ‘𝑝) / 𝑒⦌⦋(𝑑 Func 𝑒) / 𝑏⦌⟨(𝑘 ∈ 𝑏 ↦ (𝑘 ∘func 𝑓)), (𝑘 ∈ 𝑏, 𝑙 ∈ 𝑏 ↦ (𝑎 ∈ (𝑘(𝑑 Nat 𝑒)𝑙) ↦ (𝑎 ∘ (1st ‘𝑓))))⟩)
40	1, 39	wceq 1539	1 wff −∘F = (𝑝 ∈ V, 𝑓 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑑⦌⦋(2nd ‘𝑝) / 𝑒⦌⦋(𝑑 Func 𝑒) / 𝑏⦌⟨(𝑘 ∈ 𝑏 ↦ (𝑘 ∘func 𝑓)), (𝑘 ∈ 𝑏, 𝑙 ∈ 𝑏 ↦ (𝑎 ∈ (𝑘(𝑑 Nat 𝑒)𝑙) ↦ (𝑎 ∘ (1st ‘𝑓))))⟩)

This definition is referenced by:  reldmprcof  49149  prcofvalg  49150