Definition df-prj 35137

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

Assertion

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

Distinct variable group:   𝑖,𝑎,𝑛,𝑥

Detailed syntax breakdown of Definition df-prj

Step	Hyp	Ref	Expression
1		cprj 35136	. 2 class prj
2		va	. . 3 setvar 𝑎
3		cvv 3473	. . 3 class V
4		vn	. . . 4 setvar 𝑛
5		vi	. . . 4 setvar 𝑖
6		com 7859	. . . . 5 class ω
7		c1o 8465	. . . . 5 class 1o
8	6, 7	cdif 3945	. . . 4 class (ω ∖ 1o)
9	4	cv 1539	. . . 4 class 𝑛
10		vx	. . . . 5 setvar 𝑥
11	2	cv 1539	. . . . . 6 class 𝑎
12		cmap 8826	. . . . . 6 class ↑m
13	11, 9, 12	co 7412	. . . . 5 class (𝑎 ↑m 𝑛)
14	5	cv 1539	. . . . . 6 class 𝑖
15	10	cv 1539	. . . . . 6 class 𝑥
16	14, 15	cfv 6543	. . . . 5 class (𝑥‘𝑖)
17	10, 13, 16	cmpt 5231	. . . 4 class (𝑥 ∈ (𝑎 ↑m 𝑛) ↦ (𝑥‘𝑖))
18	4, 5, 8, 9, 17	cmpo 7414	. . 3 class (𝑛 ∈ (ω ∖ 1o), 𝑖 ∈ 𝑛 ↦ (𝑥 ∈ (𝑎 ↑m 𝑛) ↦ (𝑥‘𝑖)))
19	2, 3, 18	cmpt 5231	. 2 class (𝑎 ∈ V ↦ (𝑛 ∈ (ω ∖ 1o), 𝑖 ∈ 𝑛 ↦ (𝑥 ∈ (𝑎 ↑m 𝑛) ↦ (𝑥‘𝑖))))
20	1, 19	wceq 1540	1 wff prj = (𝑎 ∈ V ↦ (𝑛 ∈ (ω ∖ 1o), 𝑖 ∈ 𝑛 ↦ (𝑥 ∈ (𝑎 ↑m 𝑛) ↦ (𝑥‘𝑖))))

This definition is referenced by: (None)