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 49303

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 49345). The object part maps two functors to their composition (fuco11 49312 and fuco11b 49323). The morphism part defines the "composition" of two natural transformations (fuco22 49325) into another natural transformation (fuco22nat 49332) such that a "cube-like" diagram commutes. The naturality property also gives an alternate definition (fuco23a 49338). Note that such "composition" is different from fucco 17890 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 49302	. 2 class ∘_F
2		vp	. . 3 setvar 𝑝
3		ve	. . 3 setvar 𝑒
4		cvv 3438	. . 3 class V
5		vc	. . . 4 setvar 𝑐
6	2	cv 1539	. . . . 5 class 𝑝
7		c1st 7929	. . . . 5 class 1^st
8	6, 7	cfv 6486	. . . 4 class (1^st ‘𝑝)
9		vd	. . . . 5 setvar 𝑑
10		c2nd 7930	. . . . . 6 class 2^nd
11	6, 10	cfv 6486	. . . . 5 class (2^nd ‘𝑝)
12		vw	. . . . . 6 setvar 𝑤
13	9	cv 1539	. . . . . . . 8 class 𝑑
14	3	cv 1539	. . . . . . . 8 class 𝑒
15		cfunc 17779	. . . . . . . 8 class Func
16	13, 14, 15	co 7353	. . . . . . 7 class (𝑑 Func 𝑒)
17	5	cv 1539	. . . . . . . 8 class 𝑐
18	17, 13, 15	co 7353	. . . . . . 7 class (𝑐 Func 𝑑)
19	16, 18	cxp 5621	. . . . . 6 class ((𝑑 Func 𝑒) × (𝑐 Func 𝑑))
20		ccofu 17781	. . . . . . . 8 class ∘_func
21	12	cv 1539	. . . . . . . 8 class 𝑤
22	20, 21	cres 5625	. . . . . . 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 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 1539	. . . . . . . . . . . . . 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 17869	. . . . . . . . . . . . . . . 16 class Nat
44	13, 14, 43	co 7353	. . . . . . . . . . . . . . 15 class (𝑑 Nat 𝑒)
45	30, 39, 44	co 7353	. . . . . . . . . . . . . 14 class ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣))
46	17, 13, 43	co 7353	. . . . . . . . . . . . . . 15 class (𝑐 Nat 𝑑)
47	27, 36, 46	co 7353	. . . . . . . . . . . . . 14 class ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣))
48		vx	. . . . . . . . . . . . . . 15 setvar 𝑥
49		cbs 17138	. . . . . . . . . . . . . . . 16 class Base
50	17, 49	cfv 6486	. . . . . . . . . . . . . . 15 class (Base‘𝑐)
51	48	cv 1539	. . . . . . . . . . . . . . . . . 18 class 𝑥
52	34	cv 1539	. . . . . . . . . . . . . . . . . 18 class 𝑚
53	51, 52	cfv 6486	. . . . . . . . . . . . . . . . 17 class (𝑚‘𝑥)
54	41	cv 1539	. . . . . . . . . . . . . . . . 17 class 𝑏
55	53, 54	cfv 6486	. . . . . . . . . . . . . . . 16 class (𝑏‘(𝑚‘𝑥))
56	42	cv 1539	. . . . . . . . . . . . . . . . . 18 class 𝑎
57	51, 56	cfv 6486	. . . . . . . . . . . . . . . . 17 class (𝑎‘𝑥)
58	25	cv 1539	. . . . . . . . . . . . . . . . . . 19 class 𝑓
59	51, 58	cfv 6486	. . . . . . . . . . . . . . . . . 18 class (𝑓‘𝑥)
60	32	cv 1539	. . . . . . . . . . . . . . . . . 18 class 𝑙
61	59, 53, 60	co 7353	. . . . . . . . . . . . . . . . 17 class ((𝑓‘𝑥)𝑙(𝑚‘𝑥))
62	57, 61	cfv 6486	. . . . . . . . . . . . . . . 16 class (((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))
63	29	cv 1539	. . . . . . . . . . . . . . . . . . 19 class 𝑘
64	59, 63	cfv 6486	. . . . . . . . . . . . . . . . . 18 class (𝑘‘(𝑓‘𝑥))
65	53, 63	cfv 6486	. . . . . . . . . . . . . . . . . 18 class (𝑘‘(𝑚‘𝑥))
66	64, 65	cop 4585	. . . . . . . . . . . . . . . . 17 class ⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩
67	38	cv 1539	. . . . . . . . . . . . . . . . . 18 class 𝑟
68	53, 67	cfv 6486	. . . . . . . . . . . . . . . . 17 class (𝑟‘(𝑚‘𝑥))
69		cco 17191	. . . . . . . . . . . . . . . . . 18 class comp
70	14, 69	cfv 6486	. . . . . . . . . . . . . . . . 17 class (comp‘𝑒)
71	66, 68, 70	co 7353	. . . . . . . . . . . . . . . 16 class (⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))
72	55, 62, 71	co 7353	. . . . . . . . . . . . . . 15 class ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))
73	48, 50, 72	cmpt 5176	. . . . . . . . . . . . . 14 class (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))
74	41, 42, 45, 47, 73	cmpo 7355	. . . . . . . . . . . . 13 class (𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))
75	38, 40, 74	csb 3853	. . . . . . . . . . . 12 class ⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))
76	34, 37, 75	csb 3853	. . . . . . . . . . 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 3853	. . . . . . . . . 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 3853	. . . . . . . . 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 3853	. . . . . . . 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 7355	. . . . . . 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 4585	. . . . . 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 3853	. . . . 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 3853	. . . 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 3853	. . 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 7355	. 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 49304

W3C validator