I like you. Unlike most people, you actually think about things.
The usual way of doing this is to think of a tuple $x \in X^n$ as a function $n \rightarrow X$, not necessarily injective, where $n$ is identified with the set $\{0,\ldots,n-1\}$. Then:
First.
$a \in x$ can be interpreted as shorthand for $a \in \mathrm{img}(x)$, so yes, this makes sense.
You may wish to define a new symbol $\dot{\in}$ and assert that $a \mathbin{\dot{\in}} x$ is the number of times $a$ occurs in the tuple $x$. Explicitly, if $x \in X^n$, then $$a \mathbin{\dot{\in}} x = |i \in n : x_i = a|.$$
You can write $x^{-1}(a)$ for the set of all indices at which the value $a$ occurs. Explicitly, if $x \in X^n$, then $$x^{-1}(a) = \{i \in n : x_i = a\}.$$
Second. Yes, you can take Cartesian products of functions, so Cartesian products of tuples is a special case. In particular:$$\frac{f : A \rightarrow B \qquad f' : A' \rightarrow B'}{f \times f' : A \times A' \rightarrow B \times B'}$$
$$(f \times f')(a,a') = (f(a),f(a'))$$
According to category theory, this is all packaged up into something called the "Cartesian product functor." Judging by your interests, you should definitely learn some category theory.
As you noted, the Cartesian product of tuples won't usually be a tuple. You can solve this as follows. For each pair of natural numbers $a$ and $b$, there's a function $\lambda_{a,b} : ab \rightarrow a \times b$ that implements of the lexicographical order. Then if $x \in X^a$ and $y \in Y^b$, we can build $x \times y : a \times b \rightarrow Y \times X$, and then compose with $\lambda$ to obtain $$(x \times y) \circ \lambda_{a,b} : ab \rightarrow X \times Y,$$ which is a tuple. This has something to do with commutativity.
Third. Instead of defining functions on tuples, the usual thing is to define functions on the domain or codomain. For instance, if you want to count the number occurrences in a tuple $x \in X^n$, this could be viewed as the function $X \rightarrow \mathbb{N}$ defined by $a \mapsto a \mathbin{\dot{\in}} x$.
Fourth. Everything I've said ignores your initial injectivity assumption. If this is fundamental to what you're doing, perhaps what you're really looking for is the notion of a "finite totally-ordered set." These can be treated as if they were sets in a rather direct way. You're correct to note that if $A$ and $B$ are finite totally-ordered sets, then $A \times B$ isn't totally-ordered with the usual order. It is, however, partially ordered. And you can use to lexicographic order to totalize this, if desired.
Best Answer
As Carl remarks in comments, your formulation in the question is perfectly all right. However, if you have a good reason to want to write it down symbolically (and "because that is more mathematical" is not a good reason; it is false), then you can just do it part for part:
For every pair of elements $i$ and $j$ from $A$ ($\forall i,j\in A$) where $i$ is not equal to $j$ ($i\ne j$) it holds that ($\Rightarrow)$ the second element of the pair $i$ ($\pi_2(i)$) does not equal ($\ne$) the second element of pair $j$ ($\pi_2(j)$): $$ \forall i,j\in A: i\ne j\Rightarrow \pi_2(i)\ne \pi_2(j)$$ where $\pi_2$ is the second projection function. If you don't want to use the $\pi_2$, you can write $$ \forall \langle a,b\rangle, \langle c,d\rangle\in A: \langle a,b\rangle\ne\langle c,d\rangle\Rightarrow b\ne d$$ or a bit shorter as $$ \forall \langle a,b\rangle, \langle c,d\rangle\in A: b=d\Rightarrow a=c$$ If you're in a completely formal setting where you can't quantify over patterns such as $\langle a,b\rangle$, you'll need to do something like $$ \forall a,b,x: \langle a,x\rangle\in A\land \langle b,x\rangle\in A\Rightarrow a=b$$
Since quantifiers are involved here, the logic is (first-order) predicate calculus.
By the way, the usual name for a 2-tuple, except (possibly) when you're speaking to machines instead of to people, is an ordered pair.