Reduced ax-13 usage (a lot)

[GinoGiotto]

Part of https://groups.google.com/g/metamath/c/OB2_9sYgDfA.

I decided to speed things up a bit, both for my own mental well being and to increase the chances of success. In this PR I emptied my mathbox and added most remaining lemmas located in ax-13-complete.

Adding so many theorems in a batch might generate some disapproval, but hear me out:

With this PR, dependencies on ax-13 have been eliminated from 6631 theorems (about 12x more than my previous record so far #3355). This means that I freed about 20% of the 32,000 theorems that currently rely on it.

As usual I created a commit to show the changes in axiom usage 2eb15fa. Unfortunately github doesn't allow us to visualize extensive diffs so you'll have to verify axiom usage by yourself. The comparison can be performed with the command metamath-knife set.mm -X ax.txt on the version of set.mm edited by this PR and on the version of set.mm of my base branch (which currently corresponds to the most updated version of set.mm, although this won't last for long).

In the upcoming PRs, I will publish the minimizations that will bring ax-13 usage even lower.

[tirix]

Unfortunately github doesn't allow us to visualize extensive diffs so you'll have to verify axiom usage by yourself

It might be possible to view the diff by checking out that version locally.

This means that I freed about 20% of the 32,000 theorems that currently rely on it.

That sounds great, keep up the good work!

Adding so many theorems in a batch might generate some disapproval

Once again I think everybody agrees with the direction taken. It's just a matter of the way to realise that goal, and in my opinion we can rework the naming and discouraged usages later on.

[benjub]

I used the conventions "Do this." instead of "did this" in the git history.