df-fuco - Mathbox for Zhi Wang

	Mathbox for Zhi Wang		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-fuco		Structured version Visualization version GIF version

Definition df-fuco 49442

Description: Definition of functor composition bifunctors. Given three categories 𝐶, 𝐷, and 𝐸, (⟨𝐶, 𝐷⟩ ∘_F 𝐸) is a functor from the product category of two categories of functors to a category of functors (fucofunc 49484). The object part maps two functors to their composition (fuco11 49451 and fuco11b 49462). The morphism part defines the "composition" of two natural transformations (fuco22 49464) into another natural transformation (fuco22nat 49471) such that a "cube-like" diagram commutes. The naturality property also gives an alternate definition (fuco23a 49477). Note that such "composition" is different from fucco 17874 because they "compose" along different "axes". (Contributed by Zhi Wang, 29-Sep-2025.)

**Assertion**
Ref	Expression
df-fuco	⊢ ∘_F = (𝑝 ∈ V, 𝑒 ∈ V ↦ ⦋(1^st ‘𝑝) / 𝑐⦌⦋(2^nd ‘𝑝) / 𝑑⦌⦋((𝑑 Func 𝑒) × (𝑐 Func 𝑑)) / 𝑤⦌⟨( ∘_func ↾ 𝑤), (𝑢 ∈ 𝑤, 𝑣 ∈ 𝑤 ↦ ⦋(1^st ‘(2^nd ‘𝑢)) / 𝑓⦌⦋(1^st ‘(1^st ‘𝑢)) / 𝑘⦌⦋(2^nd ‘(1^st ‘𝑢)) / 𝑙⦌⦋(1^st ‘(2^nd ‘𝑣)) / 𝑚⦌⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩)

Distinct variable group: 𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑘,𝑙,𝑚,𝑝,𝑟,𝑢,𝑣,𝑤,𝑥

**Detailed syntax breakdown of Definition df-fuco**
Step	Hyp	Ref	Expression
1		cfuco 49441	. 2 class ∘_F
2		vp	. . 3 setvar 𝑝
3		ve	. . 3 setvar 𝑒
4		cvv 3437	. . 3 class V
5		vc	. . . 4 setvar 𝑐
6	2	cv 1540	. . . . 5 class 𝑝
7		c1st 7925	. . . . 5 class 1^st
8	6, 7	cfv 6486	. . . 4 class (1^st ‘𝑝)
9		vd	. . . . 5 setvar 𝑑
10		c2nd 7926	. . . . . 6 class 2^nd
11	6, 10	cfv 6486	. . . . 5 class (2^nd ‘𝑝)
12		vw	. . . . . 6 setvar 𝑤
13	9	cv 1540	. . . . . . . 8 class 𝑑
14	3	cv 1540	. . . . . . . 8 class 𝑒
15		cfunc 17763	. . . . . . . 8 class Func
16	13, 14, 15	co 7352	. . . . . . 7 class (𝑑 Func 𝑒)
17	5	cv 1540	. . . . . . . 8 class 𝑐
18	17, 13, 15	co 7352	. . . . . . 7 class (𝑐 Func 𝑑)
19	16, 18	cxp 5617	. . . . . 6 class ((𝑑 Func 𝑒) × (𝑐 Func 𝑑))
20		ccofu 17765	. . . . . . . 8 class ∘_func
21	12	cv 1540	. . . . . . . 8 class 𝑤
22	20, 21	cres 5621	. . . . . . 7 class ( ∘_func ↾ 𝑤)
23		vu	. . . . . . . 8 setvar 𝑢
24		vv	. . . . . . . 8 setvar 𝑣
25		vf	. . . . . . . . 9 setvar 𝑓
26	23	cv 1540	. . . . . . . . . . 11 class 𝑢
27	26, 10	cfv 6486	. . . . . . . . . 10 class (2^nd ‘𝑢)
28	27, 7	cfv 6486	. . . . . . . . 9 class (1^st ‘(2^nd ‘𝑢))
29		vk	. . . . . . . . . 10 setvar 𝑘
30	26, 7	cfv 6486	. . . . . . . . . . 11 class (1^st ‘𝑢)
31	30, 7	cfv 6486	. . . . . . . . . 10 class (1^st ‘(1^st ‘𝑢))
32		vl	. . . . . . . . . . 11 setvar 𝑙
33	30, 10	cfv 6486	. . . . . . . . . . 11 class (2^nd ‘(1^st ‘𝑢))
34		vm	. . . . . . . . . . . 12 setvar 𝑚
35	24	cv 1540	. . . . . . . . . . . . . 14 class 𝑣
36	35, 10	cfv 6486	. . . . . . . . . . . . 13 class (2^nd ‘𝑣)
37	36, 7	cfv 6486	. . . . . . . . . . . 12 class (1^st ‘(2^nd ‘𝑣))
38		vr	. . . . . . . . . . . . 13 setvar 𝑟
39	35, 7	cfv 6486	. . . . . . . . . . . . . 14 class (1^st ‘𝑣)
40	39, 7	cfv 6486	. . . . . . . . . . . . 13 class (1^st ‘(1^st ‘𝑣))
41		vb	. . . . . . . . . . . . . 14 setvar 𝑏
42		va	. . . . . . . . . . . . . 14 setvar 𝑎
43		cnat 17853	. . . . . . . . . . . . . . . 16 class Nat
44	13, 14, 43	co 7352	. . . . . . . . . . . . . . 15 class (𝑑 Nat 𝑒)
45	30, 39, 44	co 7352	. . . . . . . . . . . . . 14 class ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣))
46	17, 13, 43	co 7352	. . . . . . . . . . . . . . 15 class (𝑐 Nat 𝑑)
47	27, 36, 46	co 7352	. . . . . . . . . . . . . 14 class ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣))
48		vx	. . . . . . . . . . . . . . 15 setvar 𝑥
49		cbs 17122	. . . . . . . . . . . . . . . 16 class Base
50	17, 49	cfv 6486	. . . . . . . . . . . . . . 15 class (Base‘𝑐)
51	48	cv 1540	. . . . . . . . . . . . . . . . . 18 class 𝑥
52	34	cv 1540	. . . . . . . . . . . . . . . . . 18 class 𝑚
53	51, 52	cfv 6486	. . . . . . . . . . . . . . . . 17 class (𝑚‘𝑥)
54	41	cv 1540	. . . . . . . . . . . . . . . . 17 class 𝑏
55	53, 54	cfv 6486	. . . . . . . . . . . . . . . 16 class (𝑏‘(𝑚‘𝑥))
56	42	cv 1540	. . . . . . . . . . . . . . . . . 18 class 𝑎
57	51, 56	cfv 6486	. . . . . . . . . . . . . . . . 17 class (𝑎‘𝑥)
58	25	cv 1540	. . . . . . . . . . . . . . . . . . 19 class 𝑓
59	51, 58	cfv 6486	. . . . . . . . . . . . . . . . . 18 class (𝑓‘𝑥)
60	32	cv 1540	. . . . . . . . . . . . . . . . . 18 class 𝑙
61	59, 53, 60	co 7352	. . . . . . . . . . . . . . . . 17 class ((𝑓‘𝑥)𝑙(𝑚‘𝑥))
62	57, 61	cfv 6486	. . . . . . . . . . . . . . . 16 class (((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))
63	29	cv 1540	. . . . . . . . . . . . . . . . . . 19 class 𝑘
64	59, 63	cfv 6486	. . . . . . . . . . . . . . . . . 18 class (𝑘‘(𝑓‘𝑥))
65	53, 63	cfv 6486	. . . . . . . . . . . . . . . . . 18 class (𝑘‘(𝑚‘𝑥))
66	64, 65	cop 4581	. . . . . . . . . . . . . . . . 17 class ⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩
67	38	cv 1540	. . . . . . . . . . . . . . . . . 18 class 𝑟
68	53, 67	cfv 6486	. . . . . . . . . . . . . . . . 17 class (𝑟‘(𝑚‘𝑥))
69		cco 17175	. . . . . . . . . . . . . . . . . 18 class comp
70	14, 69	cfv 6486	. . . . . . . . . . . . . . . . 17 class (comp‘𝑒)
71	66, 68, 70	co 7352	. . . . . . . . . . . . . . . 16 class (⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))
72	55, 62, 71	co 7352	. . . . . . . . . . . . . . 15 class ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))
73	48, 50, 72	cmpt 5174	. . . . . . . . . . . . . 14 class (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))
74	41, 42, 45, 47, 73	cmpo 7354	. . . . . . . . . . . . 13 class (𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))
75	38, 40, 74	csb 3846	. . . . . . . . . . . 12 class ⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))
76	34, 37, 75	csb 3846	. . . . . . . . . . 11 class ⦋(1^st ‘(2^nd ‘𝑣)) / 𝑚⦌⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))
77	32, 33, 76	csb 3846	. . . . . . . . . 10 class ⦋(2^nd ‘(1^st ‘𝑢)) / 𝑙⦌⦋(1^st ‘(2^nd ‘𝑣)) / 𝑚⦌⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))
78	29, 31, 77	csb 3846	. . . . . . . . 9 class ⦋(1^st ‘(1^st ‘𝑢)) / 𝑘⦌⦋(2^nd ‘(1^st ‘𝑢)) / 𝑙⦌⦋(1^st ‘(2^nd ‘𝑣)) / 𝑚⦌⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))
79	25, 28, 78	csb 3846	. . . . . . . 8 class ⦋(1^st ‘(2^nd ‘𝑢)) / 𝑓⦌⦋(1^st ‘(1^st ‘𝑢)) / 𝑘⦌⦋(2^nd ‘(1^st ‘𝑢)) / 𝑙⦌⦋(1^st ‘(2^nd ‘𝑣)) / 𝑚⦌⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))
80	23, 24, 21, 21, 79	cmpo 7354	. . . . . . 7 class (𝑢 ∈ 𝑤, 𝑣 ∈ 𝑤 ↦ ⦋(1^st ‘(2^nd ‘𝑢)) / 𝑓⦌⦋(1^st ‘(1^st ‘𝑢)) / 𝑘⦌⦋(2^nd ‘(1^st ‘𝑢)) / 𝑙⦌⦋(1^st ‘(2^nd ‘𝑣)) / 𝑚⦌⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))
81	22, 80	cop 4581	. . . . . 6 class ⟨( ∘_func ↾ 𝑤), (𝑢 ∈ 𝑤, 𝑣 ∈ 𝑤 ↦ ⦋(1^st ‘(2^nd ‘𝑢)) / 𝑓⦌⦋(1^st ‘(1^st ‘𝑢)) / 𝑘⦌⦋(2^nd ‘(1^st ‘𝑢)) / 𝑙⦌⦋(1^st ‘(2^nd ‘𝑣)) / 𝑚⦌⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩
82	12, 19, 81	csb 3846	. . . . 5 class ⦋((𝑑 Func 𝑒) × (𝑐 Func 𝑑)) / 𝑤⦌⟨( ∘_func ↾ 𝑤), (𝑢 ∈ 𝑤, 𝑣 ∈ 𝑤 ↦ ⦋(1^st ‘(2^nd ‘𝑢)) / 𝑓⦌⦋(1^st ‘(1^st ‘𝑢)) / 𝑘⦌⦋(2^nd ‘(1^st ‘𝑢)) / 𝑙⦌⦋(1^st ‘(2^nd ‘𝑣)) / 𝑚⦌⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩
83	9, 11, 82	csb 3846	. . . 4 class ⦋(2^nd ‘𝑝) / 𝑑⦌⦋((𝑑 Func 𝑒) × (𝑐 Func 𝑑)) / 𝑤⦌⟨( ∘_func ↾ 𝑤), (𝑢 ∈ 𝑤, 𝑣 ∈ 𝑤 ↦ ⦋(1^st ‘(2^nd ‘𝑢)) / 𝑓⦌⦋(1^st ‘(1^st ‘𝑢)) / 𝑘⦌⦋(2^nd ‘(1^st ‘𝑢)) / 𝑙⦌⦋(1^st ‘(2^nd ‘𝑣)) / 𝑚⦌⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩
84	5, 8, 83	csb 3846	. . 3 class ⦋(1^st ‘𝑝) / 𝑐⦌⦋(2^nd ‘𝑝) / 𝑑⦌⦋((𝑑 Func 𝑒) × (𝑐 Func 𝑑)) / 𝑤⦌⟨( ∘_func ↾ 𝑤), (𝑢 ∈ 𝑤, 𝑣 ∈ 𝑤 ↦ ⦋(1^st ‘(2^nd ‘𝑢)) / 𝑓⦌⦋(1^st ‘(1^st ‘𝑢)) / 𝑘⦌⦋(2^nd ‘(1^st ‘𝑢)) / 𝑙⦌⦋(1^st ‘(2^nd ‘𝑣)) / 𝑚⦌⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩
85	2, 3, 4, 4, 84	cmpo 7354	. 2 class (𝑝 ∈ V, 𝑒 ∈ V ↦ ⦋(1^st ‘𝑝) / 𝑐⦌⦋(2^nd ‘𝑝) / 𝑑⦌⦋((𝑑 Func 𝑒) × (𝑐 Func 𝑑)) / 𝑤⦌⟨( ∘_func ↾ 𝑤), (𝑢 ∈ 𝑤, 𝑣 ∈ 𝑤 ↦ ⦋(1^st ‘(2^nd ‘𝑢)) / 𝑓⦌⦋(1^st ‘(1^st ‘𝑢)) / 𝑘⦌⦋(2^nd ‘(1^st ‘𝑢)) / 𝑙⦌⦋(1^st ‘(2^nd ‘𝑣)) / 𝑚⦌⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩)
86	1, 85	wceq 1541	1 wff ∘_F = (𝑝 ∈ V, 𝑒 ∈ V ↦ ⦋(1^st ‘𝑝) / 𝑐⦌⦋(2^nd ‘𝑝) / 𝑑⦌⦋((𝑑 Func 𝑒) × (𝑐 Func 𝑑)) / 𝑤⦌⟨( ∘_func ↾ 𝑤), (𝑢 ∈ 𝑤, 𝑣 ∈ 𝑤 ↦ ⦋(1^st ‘(2^nd ‘𝑢)) / 𝑓⦌⦋(1^st ‘(1^st ‘𝑢)) / 𝑘⦌⦋(2^nd ‘(1^st ‘𝑢)) / 𝑙⦌⦋(1^st ‘(2^nd ‘𝑣)) / 𝑚⦌⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))))⟩)

Colors of variables: wff setvar class

This definition is referenced by: fucofvalg 49443

W3C validator