Finite-index congruences form a filter

For every type $S$ of sorts equipped with a finiteness instance (with no nonemptiness assumption), every $S$-sorted signature $\Sigma$—that is, an arbitrary family of types $\Sigma(w,s)$ of operation symbols indexed by every finite list $w$ of input sorts and output sort $s$, with no finiteness restriction on the operation-symbol types—and every $\Sigma$-algebra $A$, consisting of carrier types $A_s$ (which may be empty or infinite) and an interpretation $A_w\to A_s$ for every symbol of rank $(w,s)$, the following three assertions hold simultaneously: (i) the universal congruence $\top_A$, which relates every pair of elements within each sort, has finite index; (ii) for every two congruences $\Phi,\Psi$ on $A$, if each has finite index, then their intersection $\Phi\cap\Psi$, whose relation at sort $s$ is $x\,(\Phi\cap\Psi)_s\,y\iff(x\,\Phi_s\,y\ \land\ x\,\Psi_s\,y)$, has finite index; and (iii) for every two congruences $\Phi,\Psi$ on $A$, if $\Phi$ has finite index and $\Phi\leq\Psi$, meaning that for every sort $s$ and all $x,y\in A_s$, $x\,\Phi_s\,y$ implies $x\,\Psi_s\,y$, then $\Psi$ has finite index. Here a congruence is, at every sort, an equivalence relation preserved componentwise by every basic operation of $A$, and “$\Phi$ has finite index” means literally that the total disjoint union $\coprod_{s:S}(A_s/{\Phi_s})$ of all sortwise quotient types is finite. Thus the quantified implications are vacuously satisfied whenever their antecedent finite-index conditions fail; $S$ may be empty, in which case every such disjoint union is empty, and a carrier $A_s$ may itself be empty, in which case its quotient contributes no element, whereas under $\top_A$ an inhabited carrier contributes exactly one quotient class.