On the strength of a weak variant of the Axiom of Counting

In this paper $\mathrm{NFU}^{-\mathrm{AC}}$ is used to denote Ronald Jensen's modification of Quine's `New Foundations' Set Theory ($\mathrm{NF}$) fortified with a type-level pairing function but without the Axiom of Choice. The axiom $\mathrm{AxCount}_\geq$ is the variant of the Axiom of Counting which asserts that no finite set is smaller than its own set of singletons. This paper shows that $\mathrm{NFU}^{-\mathrm{AC}}+\mathrm{AxCount}_\geq$ proves the consistency of the Simple Theory of Types with Infinity ($\mathrm{TSTI}$). This result implies that $\mathrm{NF}+\mathrm{AxCount}_\geq$ proves that consistency of $\mathrm{TSTI}$, and that $\mathrm{NFU}^{-\mathrm{AC}}+\mathrm{AxCount}_\geq$ proves the consistency of $\mathrm{NFU}^{-\mathrm{AC}}$.