save ax-riotaBAD in glbconN

[icecream17]

add discouraged tags to direct consequences of ax-riotaBAD

1218 -> 1154 (-64) dependents on ax-riotaBAD

no $j usage since ax-riotaBAD will be deleted

extra: 'autominimize' subsym1 (it would be automatic but nsb was changed to closed form; no tag or old) (shorter subsym1)

Part of #4265

[wlammen]

This is a change in NM's mathbox in a section labelled "Legacy theorems using obsolete axioms". What is the long-term intention of this pull request?
The modification of glbconN is ok. The proof is 3 lines shorter, and, by the way, does not depend on ax-un any more.
I checked your proof out and viewed it with gen-html: This theorem was proved from axioms: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext ax-rep ax-sep ax-nul ax-pow ax-pr, and compare this to glbconN

[icecream17]

According to the comment of https://us.metamath.org/mpeuni/ax-riotaBAD.html it and its direct consequences will be deleted

https://us.metamath.org/mpeuni/df-aiota.html does a similar thing to ax-riotaBAD. I think all direct consequences of ax-riotaBAD have corresponding consequences for df-aiota. So not much information is lost.

[wlammen]

The point here is that you modify a foreign mathbox. In my opinion we should not allow that on a regular basis. Normally you either get the consent of the mathbox owner, or develop the theory by copying the material to your mathbox.

Obviously Norm's mathbox is now abandonded, so we should find a way to get along with it. I support your moderate changes, but would like to hear other opinions, too.

Maybe we can find rules to handle mathboxes where the owner hasn't shown up for some time, say 3 years or so. To avoid having garbage around nobody cares about any more.

[GinoGiotto]

I fully support this PR and the plan of deleting ax-riotaBAD. The comment itself makes it very clear that it is obsolete and should be removed.

Imo keeping old inconsistent material is not a good look, and we should encourage people to keep the database tight. I don't know about a general rule for changing abandoned mathboxes, but the lack of such rule should not be an obstacle to make positive changes such as this one.

[wlammen]

I opened an issue #4541 to collect opinions on this matter.

[avekens]

I think we should not merge these changes as long as there is no common agreement how to proceed with issue #4265 - there are no comments on this issue yet, so it should be decided first if the proposed solution should be implemented. See also the more general discussion in #4541.

[icecream17]

In #4541 @avekens mentioned how the discouraged tags for ax-riotaBAD and its direct consequences are unnecessary, since the theorems are in a mathbox and won't be used. If there are no objections to this I'll change the pr accordingly tomorrow.

I added the OLD version of glbconN to be on the safe side, but note that if ax-riotaBAD is eliminated, then its removal would also remove these OLD versions before a year is up.

[avekens]

OK now.