Metamath Proof Explorer

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 ∈ V ⟼ n ∈ ω ∖ 1 𝑜 , i ∈ n ⟼ x ∈ a n ⟼ x ⁡ i

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprj class prj
1 va setvar a
2 cvv class V
3 vn setvar n
4 com class ω
5 c1o class 1 𝑜
6 4 5 cdif class ω ∖ 1 𝑜
7 vi setvar i
8 3 cv setvar n
9 vx setvar x
10 1 cv setvar a
11 cmap class ↑ 𝑚
12 10 8 11 co class a n
13 9 cv setvar x
14 7 cv setvar i
15 14 13 cfv class x ⁡ i
16 9 12 15 cmpt class x ∈ a n ⟼ x ⁡ i
17 3 7 6 8 16 cmpo class n ∈ ω ∖ 1 𝑜 , i ∈ n ⟼ x ∈ a n ⟼ x ⁡ i
18 1 2 17 cmpt class a ∈ V ⟼ n ∈ ω ∖ 1 𝑜 , i ∈ n ⟼ x ∈ a n ⟼ x ⁡ i
19 0 18 wceq wff prj = a ∈ V ⟼ n ∈ ω ∖ 1 𝑜 , i ∈ n ⟼ x ∈ a n ⟼ x ⁡ i