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 49902

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 49944). The object part maps two functors to their composition (fuco11 49911 and fuco11b 49922). The morphism part defines the "composition" of two natural transformations (fuco22 49924) into another natural transformation (fuco22nat 49931) such that a "cube-like" diagram commutes. The naturality property also gives an alternate definition (fuco23a 49937). Note that such "composition" is different from fucco 17981 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 49901	. 2 class ∘_F
2		vp	. . 3 setvar 𝑝
3		ve	. . 3 setvar 𝑒
4		cvv 3453	. . 3 class V
5		vc	. . . 4 setvar 𝑐
6	2	cv 1558	. . . . 5 class 𝑝
7		c1st 7964	. . . . 5 class 1^st
8	6, 7	cfv 6517	. . . 4 class (1^st ‘𝑝)
9		vd	. . . . 5 setvar 𝑑
10		c2nd 7965	. . . . . 6 class 2^nd
11	6, 10	cfv 6517	. . . . 5 class (2^nd ‘𝑝)
12		vw	. . . . . 6 setvar 𝑤
13	9	cv 1558	. . . . . . . 8 class 𝑑
14	3	cv 1558	. . . . . . . 8 class 𝑒
15		cfunc 17870	. . . . . . . 8 class Func
16	13, 14, 15	co 7392	. . . . . . 7 class (𝑑 Func 𝑒)
17	5	cv 1558	. . . . . . . 8 class 𝑐
18	17, 13, 15	co 7392	. . . . . . 7 class (𝑐 Func 𝑑)
19	16, 18	cxp 5643	. . . . . 6 class ((𝑑 Func 𝑒) × (𝑐 Func 𝑑))
20		ccofu 17872	. . . . . . . 8 class ∘_func
21	12	cv 1558	. . . . . . . 8 class 𝑤
22	20, 21	cres 5647	. . . . . . 7 class ( ∘_func ↾ 𝑤)
23		vu	. . . . . . . 8 setvar 𝑢
24		vv	. . . . . . . 8 setvar 𝑣
25		vf	. . . . . . . . 9 setvar 𝑓
26	23	cv 1558	. . . . . . . . . . 11 class 𝑢
27	26, 10	cfv 6517	. . . . . . . . . 10 class (2^nd ‘𝑢)
28	27, 7	cfv 6517	. . . . . . . . 9 class (1^st ‘(2^nd ‘𝑢))
29		vk	. . . . . . . . . 10 setvar 𝑘
30	26, 7	cfv 6517	. . . . . . . . . . 11 class (1^st ‘𝑢)
31	30, 7	cfv 6517	. . . . . . . . . 10 class (1^st ‘(1^st ‘𝑢))
32		vl	. . . . . . . . . . 11 setvar 𝑙
33	30, 10	cfv 6517	. . . . . . . . . . 11 class (2^nd ‘(1^st ‘𝑢))
34		vm	. . . . . . . . . . . 12 setvar 𝑚
35	24	cv 1558	. . . . . . . . . . . . . 14 class 𝑣
36	35, 10	cfv 6517	. . . . . . . . . . . . 13 class (2^nd ‘𝑣)
37	36, 7	cfv 6517	. . . . . . . . . . . 12 class (1^st ‘(2^nd ‘𝑣))
38		vr	. . . . . . . . . . . . 13 setvar 𝑟
39	35, 7	cfv 6517	. . . . . . . . . . . . . 14 class (1^st ‘𝑣)
40	39, 7	cfv 6517	. . . . . . . . . . . . 13 class (1^st ‘(1^st ‘𝑣))
41		vb	. . . . . . . . . . . . . 14 setvar 𝑏
42		va	. . . . . . . . . . . . . 14 setvar 𝑎
43		cnat 17960	. . . . . . . . . . . . . . . 16 class Nat
44	13, 14, 43	co 7392	. . . . . . . . . . . . . . 15 class (𝑑 Nat 𝑒)
45	30, 39, 44	co 7392	. . . . . . . . . . . . . 14 class ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣))
46	17, 13, 43	co 7392	. . . . . . . . . . . . . . 15 class (𝑐 Nat 𝑑)
47	27, 36, 46	co 7392	. . . . . . . . . . . . . 14 class ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣))
48		vx	. . . . . . . . . . . . . . 15 setvar 𝑥
49		cbs 17228	. . . . . . . . . . . . . . . 16 class Base
50	17, 49	cfv 6517	. . . . . . . . . . . . . . 15 class (Base‘𝑐)
51	48	cv 1558	. . . . . . . . . . . . . . . . . 18 class 𝑥
52	34	cv 1558	. . . . . . . . . . . . . . . . . 18 class 𝑚
53	51, 52	cfv 6517	. . . . . . . . . . . . . . . . 17 class (𝑚‘𝑥)
54	41	cv 1558	. . . . . . . . . . . . . . . . 17 class 𝑏
55	53, 54	cfv 6517	. . . . . . . . . . . . . . . 16 class (𝑏‘(𝑚‘𝑥))
56	42	cv 1558	. . . . . . . . . . . . . . . . . 18 class 𝑎
57	51, 56	cfv 6517	. . . . . . . . . . . . . . . . 17 class (𝑎‘𝑥)
58	25	cv 1558	. . . . . . . . . . . . . . . . . . 19 class 𝑓
59	51, 58	cfv 6517	. . . . . . . . . . . . . . . . . 18 class (𝑓‘𝑥)
60	32	cv 1558	. . . . . . . . . . . . . . . . . 18 class 𝑙
61	59, 53, 60	co 7392	. . . . . . . . . . . . . . . . 17 class ((𝑓‘𝑥)𝑙(𝑚‘𝑥))
62	57, 61	cfv 6517	. . . . . . . . . . . . . . . 16 class (((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))
63	29	cv 1558	. . . . . . . . . . . . . . . . . . 19 class 𝑘
64	59, 63	cfv 6517	. . . . . . . . . . . . . . . . . 18 class (𝑘‘(𝑓‘𝑥))
65	53, 63	cfv 6517	. . . . . . . . . . . . . . . . . 18 class (𝑘‘(𝑚‘𝑥))
66	64, 65	cop 4587	. . . . . . . . . . . . . . . . 17 class ⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩
67	38	cv 1558	. . . . . . . . . . . . . . . . . 18 class 𝑟
68	53, 67	cfv 6517	. . . . . . . . . . . . . . . . 17 class (𝑟‘(𝑚‘𝑥))
69		cco 17281	. . . . . . . . . . . . . . . . . 18 class comp
70	14, 69	cfv 6517	. . . . . . . . . . . . . . . . 17 class (comp‘𝑒)
71	66, 68, 70	co 7392	. . . . . . . . . . . . . . . 16 class (⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))
72	55, 62, 71	co 7392	. . . . . . . . . . . . . . 15 class ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))
73	48, 50, 72	cmpt 5180	. . . . . . . . . . . . . 14 class (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))
74	41, 42, 45, 47, 73	cmpo 7394	. . . . . . . . . . . . 13 class (𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))
75	38, 40, 74	csb 3852	. . . . . . . . . . . 12 class ⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))
76	34, 37, 75	csb 3852	. . . . . . . . . . 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 3852	. . . . . . . . . 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 3852	. . . . . . . . 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 3852	. . . . . . . 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 7394	. . . . . . 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 4587	. . . . . 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 3852	. . . . 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 3852	. . . 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 3852	. . 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 7394	. 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 1559	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 49903

W3C validator