Some shortenings, some credits and ALT restorations. Some edits

[benjub]

Review by commit. Commit messages are self-descriptive.

• To @BTernaryTau : I restored credit to Norm for ordsuci because, even though he didn't write that precise statement, the following two conditions are met: this is very close to a subproof of the theorem ~suceloni he contributed (the subproof can be seen in ~suceloniOLD), and since that subproof is in the deprecated theorem ~suceloniOLD which is bound to be removed, the credit to Norm would be lost. This is a general practice we have thought would be fair a few months ago (I think also @jkingdon was part of it). Search for instance "extract" used as an explanation of some "Revised by" tags. Of course, credit matters are never clear-cut ("how much inspiration have I received, how much is due to myself?" never has a clear-cut answer). To me, this removes nothing to your contributions nor the way they are credited.
• I restored epweonOLD to epweonALT since, although it requires ax-un, it is much shorter than epweon (less than half the number of essential steps). More generally, proofs which are much shorter, even if they use more axioms, should be kept as ALT. @BTernaryTau @avekens @wlammen : maybe there were similar things happening with other recent changes around the ax-un/ax-pow removals ? Do we need to do a review of these ?
• onuniorsuc: I added this closed form because I found myself looking for it and wondering why there was no such statement in set.mm.
• I deprecated the "associated inferences" ontrci and onuniorsuci since they were used each only once. This is a followup to Put some existing theorems in closed form. #4507.
• Fix some comment edits (see ~brtp and ~fvresval by @sctfn). Some rephrasings; "allow us" adds (almost) no information to "allow", except maybe the impression that the writer is egocentric.

[wlammen]

You might want to look at #4551 #4538 #4515 #4491 #4472 #4466 #4463 #4460 for more candidates for ALT

[BTernaryTau]

Ugh, sorry, I keep making revision messages and OLD theorems on autopilot. I'll try to go through my recent changes and see what else I've missed.

[benjub]

Ugh, sorry, I keep making revision messages and OLD theorems on autopilot. I'll try to go through my recent changes and see what else I've missed.

Don't be sorry please ! I really like these ax-pow and ax-un removals you've made. I'm going over the PRs mentioned above by @wlammen and there is very little to (maybe) update. I'm making a shortlist right now and will submit it here to your ("plural your", as in "you all") judgment.

[benjub]

I went over the PRs mentioned by Wolf. In my latest (and tentatively last) commit in this PR, I restored two "OLD" proofs as "ALT" since they are much shorter. These are the only two cases I found (other OLD proofs are only slightly shorter or are longer). I also found one shortening, which is minor, so didn't keep an OLD version. I think that's all (so that the "shortlist" of bordercases I mentioned above is actually very short, since it is empty !).

[jkingdon]

• I restored credit to Norm for ordsuci because . . . I think also @jkingdon was part of it . . .

I'll agree that the Contributed lines are far from an exact science. The language we put at https://us.metamath.org/mpeuni/conventions-comments.html is "An exception should be made if a theorem is essentially an extract or a variant of an already existing theorem, in which case the contributor should be that of the statement from which it is derived"

Or to say in another way which I think means largely the same thing, preserve the oldest contributed line which seems plausible.

We don't actually have a guideline saying that the Revised by lines should show all the different changes a theorem went through (in fact, sometimes it can be hard to tell whether the change being described in a Revised by is still present after a further revision without spending a lot of time with git). But I don't see anything wrong with the Revised by being proposed here.