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 48886

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 48926). The object part maps two functors to their composition (fuco11 48895). The morphism part defines the "composition" of two natural transformations (fuco22 48906) into another natural transformation (fuco22nat 48913) such that a "cube-like" diagram commutes. The naturality property also gives an alternate definition (fuco23a 48919). Note that such "composition" is different from fucco 18028 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 48885	. 2 class ∘_F
2		vp	. . 3 setvar 𝑝
3		ve	. . 3 setvar 𝑒
4		cvv 3481	. . 3 class V
5		vc	. . . 4 setvar 𝑐
6	2	cv 1538	. . . . 5 class 𝑝
7		c1st 8020	. . . . 5 class 1^st
8	6, 7	cfv 6569	. . . 4 class (1^st ‘𝑝)
9		vd	. . . . 5 setvar 𝑑
10		c2nd 8021	. . . . . 6 class 2^nd
11	6, 10	cfv 6569	. . . . 5 class (2^nd ‘𝑝)
12		vw	. . . . . 6 setvar 𝑤
13	9	cv 1538	. . . . . . . 8 class 𝑑
14	3	cv 1538	. . . . . . . 8 class 𝑒
15		cfunc 17914	. . . . . . . 8 class Func
16	13, 14, 15	co 7438	. . . . . . 7 class (𝑑 Func 𝑒)
17	5	cv 1538	. . . . . . . 8 class 𝑐
18	17, 13, 15	co 7438	. . . . . . 7 class (𝑐 Func 𝑑)
19	16, 18	cxp 5691	. . . . . 6 class ((𝑑 Func 𝑒) × (𝑐 Func 𝑑))
20		ccofu 17916	. . . . . . . 8 class ∘_func
21	12	cv 1538	. . . . . . . 8 class 𝑤
22	20, 21	cres 5695	. . . . . . 7 class ( ∘_func ↾ 𝑤)
23		vu	. . . . . . . 8 setvar 𝑢
24		vv	. . . . . . . 8 setvar 𝑣
25		vf	. . . . . . . . 9 setvar 𝑓
26	23	cv 1538	. . . . . . . . . . 11 class 𝑢
27	26, 10	cfv 6569	. . . . . . . . . 10 class (2^nd ‘𝑢)
28	27, 7	cfv 6569	. . . . . . . . 9 class (1^st ‘(2^nd ‘𝑢))
29		vk	. . . . . . . . . 10 setvar 𝑘
30	26, 7	cfv 6569	. . . . . . . . . . 11 class (1^st ‘𝑢)
31	30, 7	cfv 6569	. . . . . . . . . 10 class (1^st ‘(1^st ‘𝑢))
32		vl	. . . . . . . . . . 11 setvar 𝑙
33	30, 10	cfv 6569	. . . . . . . . . . 11 class (2^nd ‘(1^st ‘𝑢))
34		vm	. . . . . . . . . . . 12 setvar 𝑚
35	24	cv 1538	. . . . . . . . . . . . . 14 class 𝑣
36	35, 10	cfv 6569	. . . . . . . . . . . . 13 class (2^nd ‘𝑣)
37	36, 7	cfv 6569	. . . . . . . . . . . 12 class (1^st ‘(2^nd ‘𝑣))
38		vr	. . . . . . . . . . . . 13 setvar 𝑟
39	35, 7	cfv 6569	. . . . . . . . . . . . . 14 class (1^st ‘𝑣)
40	39, 7	cfv 6569	. . . . . . . . . . . . 13 class (1^st ‘(1^st ‘𝑣))
41		vb	. . . . . . . . . . . . . 14 setvar 𝑏
42		va	. . . . . . . . . . . . . 14 setvar 𝑎
43		cnat 18005	. . . . . . . . . . . . . . . 16 class Nat
44	13, 14, 43	co 7438	. . . . . . . . . . . . . . 15 class (𝑑 Nat 𝑒)
45	30, 39, 44	co 7438	. . . . . . . . . . . . . 14 class ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣))
46	17, 13, 43	co 7438	. . . . . . . . . . . . . . 15 class (𝑐 Nat 𝑑)
47	27, 36, 46	co 7438	. . . . . . . . . . . . . 14 class ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣))
48		vx	. . . . . . . . . . . . . . 15 setvar 𝑥
49		cbs 17254	. . . . . . . . . . . . . . . 16 class Base
50	17, 49	cfv 6569	. . . . . . . . . . . . . . 15 class (Base‘𝑐)
51	48	cv 1538	. . . . . . . . . . . . . . . . . 18 class 𝑥
52	34	cv 1538	. . . . . . . . . . . . . . . . . 18 class 𝑚
53	51, 52	cfv 6569	. . . . . . . . . . . . . . . . 17 class (𝑚‘𝑥)
54	41	cv 1538	. . . . . . . . . . . . . . . . 17 class 𝑏
55	53, 54	cfv 6569	. . . . . . . . . . . . . . . 16 class (𝑏‘(𝑚‘𝑥))
56	42	cv 1538	. . . . . . . . . . . . . . . . . 18 class 𝑎
57	51, 56	cfv 6569	. . . . . . . . . . . . . . . . 17 class (𝑎‘𝑥)
58	25	cv 1538	. . . . . . . . . . . . . . . . . . 19 class 𝑓
59	51, 58	cfv 6569	. . . . . . . . . . . . . . . . . 18 class (𝑓‘𝑥)
60	32	cv 1538	. . . . . . . . . . . . . . . . . 18 class 𝑙
61	59, 53, 60	co 7438	. . . . . . . . . . . . . . . . 17 class ((𝑓‘𝑥)𝑙(𝑚‘𝑥))
62	57, 61	cfv 6569	. . . . . . . . . . . . . . . 16 class (((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))
63	29	cv 1538	. . . . . . . . . . . . . . . . . . 19 class 𝑘
64	59, 63	cfv 6569	. . . . . . . . . . . . . . . . . 18 class (𝑘‘(𝑓‘𝑥))
65	53, 63	cfv 6569	. . . . . . . . . . . . . . . . . 18 class (𝑘‘(𝑚‘𝑥))
66	64, 65	cop 4640	. . . . . . . . . . . . . . . . 17 class ⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩
67	38	cv 1538	. . . . . . . . . . . . . . . . . 18 class 𝑟
68	53, 67	cfv 6569	. . . . . . . . . . . . . . . . 17 class (𝑟‘(𝑚‘𝑥))
69		cco 17319	. . . . . . . . . . . . . . . . . 18 class comp
70	14, 69	cfv 6569	. . . . . . . . . . . . . . . . 17 class (comp‘𝑒)
71	66, 68, 70	co 7438	. . . . . . . . . . . . . . . 16 class (⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))
72	55, 62, 71	co 7438	. . . . . . . . . . . . . . 15 class ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))
73	48, 50, 72	cmpt 5234	. . . . . . . . . . . . . 14 class (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥))))
74	41, 42, 45, 47, 73	cmpo 7440	. . . . . . . . . . . . 13 class (𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))
75	38, 40, 74	csb 3911	. . . . . . . . . . . 12 class ⦋(1^st ‘(1^st ‘𝑣)) / 𝑟⦌(𝑏 ∈ ((1^st ‘𝑢)(𝑑 Nat 𝑒)(1^st ‘𝑣)), 𝑎 ∈ ((2^nd ‘𝑢)(𝑐 Nat 𝑑)(2^nd ‘𝑣)) ↦ (𝑥 ∈ (Base‘𝑐) ↦ ((𝑏‘(𝑚‘𝑥))(⟨(𝑘‘(𝑓‘𝑥)), (𝑘‘(𝑚‘𝑥))⟩(comp‘𝑒)(𝑟‘(𝑚‘𝑥)))(((𝑓‘𝑥)𝑙(𝑚‘𝑥))‘(𝑎‘𝑥)))))
76	34, 37, 75	csb 3911	. . . . . . . . . . 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 3911	. . . . . . . . . 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 3911	. . . . . . . . 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 3911	. . . . . . . 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 7440	. . . . . . 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 4640	. . . . . 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 3911	. . . . 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 3911	. . . 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 3911	. . 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 7440	. 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 1539	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 48887

W3C validator