df-fuco

Description: Definition of functor composition bifunctors. Given three categories C , D , and E , ( <. C , D >. o.F E ) is a functor from the product category of two categories of functors to a category of functors ( fucofunc ). The object part maps two functors to their composition ( fuco11 ). The morphism part defines the "composition" of two natural transformations ( fuco22 ) into another natural transformation ( fuco22nat ) such that a "cube-like" diagram commutes. The naturality property also gives an alternate definition ( fuco23a ). Note that such "composition" is different from fucco because they "compose" along different "axes". (Contributed by Zhi Wang, 29-Sep-2025)

		Ref	Expression
	Assertion	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 ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfuco	⊢ ∘_F
1		vp	⊢ 𝑝
2		cvv	⊢ V
3		ve	⊢ 𝑒
4		c1st	⊢ 1^st
5	1	cv	⊢ 𝑝
6	5 4	cfv	⊢ ( 1^st ‘ 𝑝 )
7		vc	⊢ 𝑐
8		c2nd	⊢ 2^nd
9	5 8	cfv	⊢ ( 2^nd ‘ 𝑝 )
10		vd	⊢ 𝑑
11	10	cv	⊢ 𝑑
12		cfunc	⊢ Func
13	3	cv	⊢ 𝑒
14	11 13 12	co	⊢ ( 𝑑 Func 𝑒 )
15	7	cv	⊢ 𝑐
16	15 11 12	co	⊢ ( 𝑐 Func 𝑑 )
17	14 16	cxp	⊢ ( ( 𝑑 Func 𝑒 ) × ( 𝑐 Func 𝑑 ) )
18		vw	⊢ 𝑤
19		ccofu	⊢ ∘_func
20	18	cv	⊢ 𝑤
21	19 20	cres	⊢ ( ∘_func ↾ 𝑤 )
22		vu	⊢ 𝑢
23		vv	⊢ 𝑣
24	22	cv	⊢ 𝑢
25	24 8	cfv	⊢ ( 2^nd ‘ 𝑢 )
26	25 4	cfv	⊢ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) )
27		vf	⊢ 𝑓
28	24 4	cfv	⊢ ( 1^st ‘ 𝑢 )
29	28 4	cfv	⊢ ( 1^st ‘ ( 1^st ‘ 𝑢 ) )
30		vk	⊢ 𝑘
31	28 8	cfv	⊢ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) )
32		vl	⊢ 𝑙
33	23	cv	⊢ 𝑣
34	33 8	cfv	⊢ ( 2^nd ‘ 𝑣 )
35	34 4	cfv	⊢ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) )
36		vm	⊢ 𝑚
37	33 4	cfv	⊢ ( 1^st ‘ 𝑣 )
38	37 4	cfv	⊢ ( 1^st ‘ ( 1^st ‘ 𝑣 ) )
39		vr	⊢ 𝑟
40		vb	⊢ 𝑏
41		cnat	⊢ Nat
42	11 13 41	co	⊢ ( 𝑑 Nat 𝑒 )
43	28 37 42	co	⊢ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) )
44		va	⊢ 𝑎
45	15 11 41	co	⊢ ( 𝑐 Nat 𝑑 )
46	25 34 45	co	⊢ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) )
47		vx	⊢ 𝑥
48		cbs	⊢ Base
49	15 48	cfv	⊢ ( Base ‘ 𝑐 )
50	40	cv	⊢ 𝑏
51	36	cv	⊢ 𝑚
52	47	cv	⊢ 𝑥
53	52 51	cfv	⊢ ( 𝑚 ‘ 𝑥 )
54	53 50	cfv	⊢ ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) )
55	30	cv	⊢ 𝑘
56	27	cv	⊢ 𝑓
57	52 56	cfv	⊢ ( 𝑓 ‘ 𝑥 )
58	57 55	cfv	⊢ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) )
59	53 55	cfv	⊢ ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) )
60	58 59	cop	⊢ ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩
61		cco	⊢ comp
62	13 61	cfv	⊢ ( comp ‘ 𝑒 )
63	39	cv	⊢ 𝑟
64	53 63	cfv	⊢ ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) )
65	60 64 62	co	⊢ ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) )
66	32	cv	⊢ 𝑙
67	57 53 66	co	⊢ ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) )
68	44	cv	⊢ 𝑎
69	52 68	cfv	⊢ ( 𝑎 ‘ 𝑥 )
70	69 67	cfv	⊢ ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) )
71	54 70 65	co	⊢ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) )
72	47 49 71	cmpt	⊢ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) )
73	40 44 43 46 72	cmpo	⊢ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) )
74	39 38 73	csb	⊢ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) )
75	36 35 74	csb	⊢ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) )
76	32 31 75	csb	⊢ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) )
77	30 29 76	csb	⊢ ⦋ ( 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 ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) )
78	27 26 77	csb	⊢ ⦋ ( 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 ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) )
79	22 23 20 20 78	cmpo	⊢ ( 𝑢 ∈ 𝑤 , 𝑣 ∈ 𝑤 ↦ ⦋ ( 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	21 79	cop	⊢ ⟨ ( ∘_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 ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩
81	18 17 80	csb	⊢ ⦋ ( ( 𝑑 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 ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩
82	10 9 81	csb	⊢ ⦋ ( 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 ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩
83	7 6 82	csb	⊢ ⦋ ( 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 ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩
84	1 3 2 2 83	cmpo	⊢ ( 𝑝 ∈ 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 ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )
85	0 84	wceq	⊢ ∘_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 ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )

Metamath Proof Explorer

Definition df-fuco

Detailed syntax breakdown