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 49306

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 49348). The object part maps two functors to their composition (fuco11 49315 and fuco11b 49326). The morphism part defines the "composition" of two natural transformations (fuco22 49328) into another natural transformation (fuco22nat 49335) such that a "cube-like" diagram commutes. The naturality property also gives an alternate definition (fuco23a 49341). Note that such "composition" is different from fucco 17927 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 49305	. 2 class ∘_F
2		vp	. . 3 setvar 𝑝
3		ve	. . 3 setvar 𝑒
4		cvv 3447	. . 3 class V
5		vc	. . . 4 setvar 𝑐
6	2	cv 1539	. . . . 5 class 𝑝
7		c1st 7966	. . . . 5 class 1^st
8	6, 7	cfv 6511	. . . 4 class (1^st ‘𝑝)
9		vd	. . . . 5 setvar 𝑑
10		c2nd 7967	. . . . . 6 class 2^nd
11	6, 10	cfv 6511	. . . . 5 class (2^nd ‘𝑝)
12		vw	. . . . . 6 setvar 𝑤
13	9	cv 1539	. . . . . . . 8 class 𝑑
14	3	cv 1539	. . . . . . . 8 class 𝑒
15		cfunc 17816	. . . . . . . 8 class Func
16	13, 14, 15	co 7387	. . . . . . 7 class (𝑑 Func 𝑒)
17	5	cv 1539	. . . . . . . 8 class 𝑐
18	17, 13, 15	co 7387	. . . . . . 7 class (𝑐 Func 𝑑)
19	16, 18	cxp 5636	. . . . . 6 class ((𝑑 Func 𝑒) × (𝑐 Func 𝑑))
20		ccofu 17818	. . . . . . . 8 class ∘_func
21	12	cv 1539	. . . . . . . 8 class 𝑤
22	20, 21	cres 5640	. . . . . . 7 class ( ∘_func ↾ 𝑤)
23		vu	. . . . . . . 8 setvar 𝑢
24		vv	. . . . . . . 8 setvar 𝑣
25		vf	. . . . . . . . 9 setvar 𝑓
26	23	cv 1539	. . . . . . . . . . 11 class 𝑢
27	26, 10	cfv 6511	. . . . . . . . . 10 class (2^nd ‘𝑢)
28	27, 7	cfv 6511	. . . . . . . . 9 class (1^st ‘(2^nd ‘𝑢))
29		vk	. . . . . . . . . 10 setvar 𝑘
30	26, 7	cfv 6511	. . . . . . . . . . 11 class (1^st ‘𝑢)
31	30, 7	cfv 6511	. . . . . . . . . 10 class (1^st ‘(1^st ‘𝑢))
32		vl	. . . . . . . . . . 11 setvar 𝑙
33	30, 10	cfv 6511	. . . . . . . . . . 11 class (2^nd ‘(1^st ‘𝑢))
34		vm	. . . . . . . . . . . 12 setvar 𝑚
35	24	cv 1539	. . . . . . . . . . . . . 14 class 𝑣
36	35, 10	cfv 6511	. . . . . . . . . . . . 13 class (2^nd ‘𝑣)
37	36, 7	cfv 6511	. . . . . . . . . . . 12 class (1^st ‘(2^nd ‘𝑣))
38		vr	. . . . . . . . . . . . 13 setvar 𝑟
39	35, 7	cfv 6511	. . . . . . . . . . . . . 14 class (1^st ‘𝑣)
40	39, 7	cfv 6511	. . . . . . . . . . . . 13 class (1^st ‘(1^st ‘𝑣))
41		vb	. . . . . . . . . . . . . 14 setvar 𝑏
42		va	. . . . . . . . . . . . . 14 setvar 𝑎
43		cnat 17906	. . . . . . . . . . . . . . . 16 class Nat
44	13, 14, 43	co 7387	. . . . . . . . . . . . . . 15 class (𝑑 Nat 𝑒)
45	30, 39, 44	co 7387	. . . . . . . . . . . . . 14 class ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣))
46	17, 13, 43	co 7387	. . . . . . . . . . . . . . 15 class (𝑐 Nat 𝑑)
47	27, 36, 46	co 7387	. . . . . . . . . . . . . 14 class ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣))
48		vx	. . . . . . . . . . . . . . 15 setvar 𝑥
49		cbs 17179	. . . . . . . . . . . . . . . 16 class Base
50	17, 49	cfv 6511	. . . . . . . . . . . . . . 15 class (Base‘𝑐)
51	48	cv 1539	. . . . . . . . . . . . . . . . . 18 class 𝑥
52	34	cv 1539	. . . . . . . . . . . . . . . . . 18 class 𝑚
53	51, 52	cfv 6511	. . . . . . . . . . . . . . . . 17 class (𝑚‘𝑥)
54	41	cv 1539	. . . . . . . . . . . . . . . . 17 class 𝑏
55	53, 54	cfv 6511	. . . . . . . . . . . . . . . 16 class (𝑏‘(𝑚‘𝑥))
56	42	cv 1539	. . . . . . . . . . . . . . . . . 18 class 𝑎
57	51, 56	cfv 6511	. . . . . . . . . . . . . . . . 17 class (𝑎‘𝑥)
58	25	cv 1539	. . . . . . . . . . . . . . . . . . 19 class 𝑓
59	51, 58	cfv 6511	. . . . . . . . . . . . . . . . . 18 class (𝑓‘𝑥)
60	32	cv 1539	. . . . . . . . . . . . . . . . . 18 class 𝑙
61	59, 53, 60	co 7387	. . . . . . . . . . . . . . . . 17 class ((𝑓‘𝑥)𝑙(𝑚‘𝑥))
62	57, 61	cfv 6511	. . . . . . . . . . . . . . . 16 class (((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))
63	29	cv 1539	. . . . . . . . . . . . . . . . . . 19 class 𝑘
64	59, 63	cfv 6511	. . . . . . . . . . . . . . . . . 18 class (𝑘‘(𝑓‘𝑥))
65	53, 63	cfv 6511	. . . . . . . . . . . . . . . . . 18 class (𝑘‘(𝑚‘𝑥))
66	64, 65	cop 4595	. . . . . . . . . . . . . . . . 17 class ⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩
67	38	cv 1539	. . . . . . . . . . . . . . . . . 18 class 𝑟
68	53, 67	cfv 6511	. . . . . . . . . . . . . . . . 17 class (𝑟‘(𝑚‘𝑥))
69		cco 17232	. . . . . . . . . . . . . . . . . 18 class comp
70	14, 69	cfv 6511	. . . . . . . . . . . . . . . . 17 class (comp‘𝑒)
71	66, 68, 70	co 7387	. . . . . . . . . . . . . . . 16 class (⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))
72	55, 62, 71	co 7387	. . . . . . . . . . . . . . 15 class ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))
73	48, 50, 72	cmpt 5188	. . . . . . . . . . . . . 14 class (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))
74	41, 42, 45, 47, 73	cmpo 7389	. . . . . . . . . . . . 13 class (𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))
75	38, 40, 74	csb 3862	. . . . . . . . . . . 12 class ⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))
76	34, 37, 75	csb 3862	. . . . . . . . . . 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 3862	. . . . . . . . . 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 3862	. . . . . . . . 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 3862	. . . . . . . 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 7389	. . . . . . 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 4595	. . . . . 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 3862	. . . . 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 3862	. . . 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 3862	. . 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 7389	. 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 1540	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 49307

W3C validator