Definition df-suppos

Description: Define the function that, when given an n -ary operation f and n many m -ary operations ( g(/) ) , ..., ( gU. n ) , returns the superposition of f with the ( gi ) , itself another m -ary operation on a . Given x (a sequence of m arguments in a ), the superposition effectively applies each of the ( gi ) to x , then applies f to the resulting sequence of n 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)

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

Detailed syntax breakdown

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