Definition df-prj

Description: Define the function that, for a set a , arity n , and index i , returns the i -th n -ary projection on a . This is the n -ary operation on a that, for any sequence of n elements of a , returns the element having index i . (Contributed by Adrian Ducourtial, 3-Apr-2025)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprj	⊢ prj
1		va	⊢ 𝑎
2		cvv	⊢ V
3		vn	⊢ 𝑛
4		com	⊢ ω
5		c1o	⊢ 1o
6	4 5	cdif	⊢ ( ω ∖ 1o )
7		vi	⊢ 𝑖
8	3	cv	⊢ 𝑛
9		vx	⊢ 𝑥
10	1	cv	⊢ 𝑎
11		cmap	⊢ ↑m
12	10 8 11	co	⊢ ( 𝑎 ↑m 𝑛 )
13	9	cv	⊢ 𝑥
14	7	cv	⊢ 𝑖
15	14 13	cfv	⊢ ( 𝑥 ‘ 𝑖 )
16	9 12 15	cmpt	⊢ ( 𝑥 ∈ ( 𝑎 ↑m 𝑛 ) ↦ ( 𝑥 ‘ 𝑖 ) )
17	3 7 6 8 16	cmpo	⊢ ( 𝑛 ∈ ( ω ∖ 1o ) , 𝑖 ∈ 𝑛 ↦ ( 𝑥 ∈ ( 𝑎 ↑m 𝑛 ) ↦ ( 𝑥 ‘ 𝑖 ) ) )
18	1 2 17	cmpt	⊢ ( 𝑎 ∈ V ↦ ( 𝑛 ∈ ( ω ∖ 1o ) , 𝑖 ∈ 𝑛 ↦ ( 𝑥 ∈ ( 𝑎 ↑m 𝑛 ) ↦ ( 𝑥 ‘ 𝑖 ) ) ) )
19	0 18	wceq	⊢ prj = ( 𝑎 ∈ V ↦ ( 𝑛 ∈ ( ω ∖ 1o ) , 𝑖 ∈ 𝑛 ↦ ( 𝑥 ∈ ( 𝑎 ↑m 𝑛 ) ↦ ( 𝑥 ‘ 𝑖 ) ) ) )