Inversions of a Permutation of [n]

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let $n\in\mathbb{N}$, with $[n]$ as in Intervals of Natural Numbers §segment, a set by Permutations of a Set and the Set of Permutations of [n] §permutations, $S_{n}$ as in Permutations of a Set and the Set of Permutations of [n] §permutations and Permutations of a Set and the Set of Permutations of [n] §membership, and the strict order $<$ of $\mathbb{N}_{0}$ as in The Order on Omega §strict; $[n]\times[n]$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set.

¶ For $\sigma\in S_{n}$, the set of inversions of $\sigma$ is

$$\mathrm{Inv}(\sigma)=\{p\in[n]\times[n]:\exists i\,\exists j\,(p=(i,j)\wedge i<j\wedge\sigma(j)<\sigma(i))\},$$

formed by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted from a formula in which the values $\sigma(i)$ and $\sigma(j)$ are used properly, since $p\in[n]\times[n]$ and $p=(i,j)$ give $i,j\in[n]$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership and $\operatorname{dom}\sigma=[n]$ by Permutations of a Set and the Set of Permutations of [n] §membership, and which is therefore predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value and Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §closure; it is a subclass of $[n]\times[n]$ by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, hence a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §subclass. An inversion of $\sigma$ is an element of $\mathrm{Inv}(\sigma)$.

¶ For $\sigma\in S_{n}$ and a set $p$: $p\in\mathrm{Inv}(\sigma)$ if and only if $p=(i,j)$ for some $i,j\in[n]$ with $i<j$ and $\sigma(j)<\sigma(i)$, by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction and Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership.