Definition df-suppos 35700

Description: Define the function that, when given an 𝑛-ary operation 𝑓 and 𝑛 many 𝑚-ary operations (𝑔‘∅), ..., (𝑔‘∪ 𝑛), returns the superposition of 𝑓 with the (𝑔‘𝑖), itself another 𝑚-ary operation on 𝑎. Given 𝑥 (a sequence of 𝑚 arguments in 𝑎), the superposition effectively applies each of the (𝑔‘𝑖) to 𝑥, then applies 𝑓 to the resulting sequence of 𝑛 function values. This can be seen as a generalized version of function composition; see paragraph 3 of [Szendrei] p. 11. (Contributed by Adrian Ducourtial, 3-Apr-2025.)

Assertion

Ref	Expression
df-suppos	⊢ suppos = (𝑎 ∈ V ↦ (𝑛 ∈ (ω ∖ 1o), 𝑚 ∈ (ω ∖ 1o) ↦ (𝑓 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛)), 𝑔 ∈ ((𝑎 ↑m (𝑎 ↑m 𝑚)) ↑m 𝑛) ↦ (𝑥 ∈ (𝑎 ↑m 𝑚) ↦ (𝑓‘(𝑖 ∈ 𝑛 ↦ ((𝑔‘𝑖)‘𝑥)))))))

Distinct variable group:   𝑓,𝑎,𝑔,𝑖,𝑚,𝑛,𝑥

Detailed syntax breakdown of Definition df-suppos

Step	Hyp	Ref	Expression
1		csuppos 35699	. 2 class suppos
2		va	. . 3 setvar 𝑎
3		cvv 3480	. . 3 class V
4		vn	. . . 4 setvar 𝑛
5		vm	. . . 4 setvar 𝑚
6		com 7887	. . . . 5 class ω
7		c1o 8499	. . . . 5 class 1o
8	6, 7	cdif 3948	. . . 4 class (ω ∖ 1o)
9		vf	. . . . 5 setvar 𝑓
10		vg	. . . . 5 setvar 𝑔
11	2	cv 1539	. . . . . 6 class 𝑎
12	4	cv 1539	. . . . . . 7 class 𝑛
13		cmap 8866	. . . . . . 7 class ↑m
14	11, 12, 13	co 7431	. . . . . 6 class (𝑎 ↑m 𝑛)
15	11, 14, 13	co 7431	. . . . 5 class (𝑎 ↑m (𝑎 ↑m 𝑛))
16	5	cv 1539	. . . . . . . 8 class 𝑚
17	11, 16, 13	co 7431	. . . . . . 7 class (𝑎 ↑m 𝑚)
18	11, 17, 13	co 7431	. . . . . 6 class (𝑎 ↑m (𝑎 ↑m 𝑚))
19	18, 12, 13	co 7431	. . . . 5 class ((𝑎 ↑m (𝑎 ↑m 𝑚)) ↑m 𝑛)
20		vx	. . . . . 6 setvar 𝑥
21		vi	. . . . . . . 8 setvar 𝑖
22	20	cv 1539	. . . . . . . . 9 class 𝑥
23	21	cv 1539	. . . . . . . . . 10 class 𝑖
24	10	cv 1539	. . . . . . . . . 10 class 𝑔
25	23, 24	cfv 6561	. . . . . . . . 9 class (𝑔‘𝑖)
26	22, 25	cfv 6561	. . . . . . . 8 class ((𝑔‘𝑖)‘𝑥)
27	21, 12, 26	cmpt 5225	. . . . . . 7 class (𝑖 ∈ 𝑛 ↦ ((𝑔‘𝑖)‘𝑥))
28	9	cv 1539	. . . . . . 7 class 𝑓
29	27, 28	cfv 6561	. . . . . 6 class (𝑓‘(𝑖 ∈ 𝑛 ↦ ((𝑔‘𝑖)‘𝑥)))
30	20, 17, 29	cmpt 5225	. . . . 5 class (𝑥 ∈ (𝑎 ↑m 𝑚) ↦ (𝑓‘(𝑖 ∈ 𝑛 ↦ ((𝑔‘𝑖)‘𝑥))))
31	9, 10, 15, 19, 30	cmpo 7433	. . . 4 class (𝑓 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛)), 𝑔 ∈ ((𝑎 ↑m (𝑎 ↑m 𝑚)) ↑m 𝑛) ↦ (𝑥 ∈ (𝑎 ↑m 𝑚) ↦ (𝑓‘(𝑖 ∈ 𝑛 ↦ ((𝑔‘𝑖)‘𝑥)))))
32	4, 5, 8, 8, 31	cmpo 7433	. . 3 class (𝑛 ∈ (ω ∖ 1o), 𝑚 ∈ (ω ∖ 1o) ↦ (𝑓 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛)), 𝑔 ∈ ((𝑎 ↑m (𝑎 ↑m 𝑚)) ↑m 𝑛) ↦ (𝑥 ∈ (𝑎 ↑m 𝑚) ↦ (𝑓‘(𝑖 ∈ 𝑛 ↦ ((𝑔‘𝑖)‘𝑥))))))
33	2, 3, 32	cmpt 5225	. 2 class (𝑎 ∈ V ↦ (𝑛 ∈ (ω ∖ 1o), 𝑚 ∈ (ω ∖ 1o) ↦ (𝑓 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛)), 𝑔 ∈ ((𝑎 ↑m (𝑎 ↑m 𝑚)) ↑m 𝑛) ↦ (𝑥 ∈ (𝑎 ↑m 𝑚) ↦ (𝑓‘(𝑖 ∈ 𝑛 ↦ ((𝑔‘𝑖)‘𝑥)))))))
34	1, 33	wceq 1540	1 wff suppos = (𝑎 ∈ V ↦ (𝑛 ∈ (ω ∖ 1o), 𝑚 ∈ (ω ∖ 1o) ↦ (𝑓 ∈ (𝑎 ↑m (𝑎 ↑m 𝑛)), 𝑔 ∈ ((𝑎 ↑m (𝑎 ↑m 𝑚)) ↑m 𝑛) ↦ (𝑥 ∈ (𝑎 ↑m 𝑚) ↦ (𝑓‘(𝑖 ∈ 𝑛 ↦ ((𝑔‘𝑖)‘𝑥)))))))

This definition is referenced by: (None)