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 = ( a e. _V |-> ( n e. ( _om \ 1o ) , i e. n |-> ( x e. ( a ^m n ) |-> ( x ` i ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprj	|- prj
1		va	|- a
2		cvv	|- _V
3		vn	|- n
4		com	|- _om
5		c1o	|- 1o
6	4 5	cdif	|- ( _om \ 1o )
7		vi	|- i
8	3	cv	|- n
9		vx	|- x
10	1	cv	|- a
11		cmap	|- ^m
12	10 8 11	co	|- ( a ^m n )
13	9	cv	|- x
14	7	cv	|- i
15	14 13	cfv	|- ( x ` i )
16	9 12 15	cmpt	|- ( x e. ( a ^m n ) |-> ( x ` i ) )
17	3 7 6 8 16	cmpo	|- ( n e. ( _om \ 1o ) , i e. n |-> ( x e. ( a ^m n ) |-> ( x ` i ) ) )
18	1 2 17	cmpt	|- ( a e. _V |-> ( n e. ( _om \ 1o ) , i e. n |-> ( x e. ( a ^m n ) |-> ( x ` i ) ) ) )
19	0 18	wceq	|- prj = ( a e. _V |-> ( n e. ( _om \ 1o ) , i e. n |-> ( x e. ( a ^m n ) |-> ( x ` i ) ) ) )