Projection functions

[ducourtial.metam...@passfwd.com]

Hello all,

I've been dabbling with formalizing a result in clone theory, requiring me to define the notion of a clone (which, so far as I know, is not already in set.mm). One aspect of this is the notion of a projection: For a set A, a natural number n > 0, and an integer 0 <= i < n, the i-th n-ary projection on A is the function p : A^n \to A given by

p(x_0, ..., x_i, ..., x_{n-1}) = x_i.

I have tried to capture this notion in Metamath (in the general case), but I would appreciate any feedback on my formulation, primarily with regards to simplicity and conventions in set.mm. Below, I give an outline of my proposed definition.

Firstly, I model the numbers n, i as ordinals for convenience; in particular, the condition that 0 <= i < n simply becomes i e. n, while the condition that n be positive is expressed as n e. ( _om \ 1o ).

Secondly, in desiring p to "pick out" the i-th argument, it appears to me that defining p as a traditional n-ary operation, with domain A^n, is impractical (correct me if I'm wrong). Instead, I've chosen to define p as a function on length-n sequences of elements in A; in Metamath, we would have p : ( A ^m n ) --> A. Thus, for some sequence of arguments x e. ( A ^m n ), the i-th argument would be given by ( x ` i ) for i e. n.

In total, I define a class proj which, when given a set A and suitable ordinals n, i, returns the i-th n-ary projection on A. Here's the full definition:

|- proj = ( a e. _V |-> ( n e. ( _om \ 1o ) , i e. n |-> ( x e. ( a ^m n ) |-> ( x ` i ) ) ) )

I'd like to ask: Is my approach reasonable, or have I gone off the rails?

I hope the above is sufficiently clear, and I thank any suggestions in advance.

All the best,
Adrian