Remove ax-riotaBAD [mathbox]

[icecream17]

https://us.metamath.org/mpeuni/ax-riotaBAD.html

As noted in #4248 there are several parts of set.mm with bad theorems, so this issue is about one "family" of them: those using ax-riotaBAD (~2.8% of set.mm)

This axiom is only used in https://us.metamath.org/mpeuni/riotaclbgBAD.html, where the inconsistency with set.mm is in the reverse direction. I'd expect that most of the time, deeper in the dependency chain (for instance https://us.metamath.org/mpeuni/glbconN.html), it should be possible to just prove uniqueness directly.

---

Edit: todo list of theorems directly using obsolete riota* theorems:

riotaclbBAD:

• glbconN
• cdlemk36

riotasvd:

• cdleme32a

riotasv2d:

• cdleme42b

riotasv:

• cdleme26e
• cdleme26eALTN
• cdleme26fALTN
• cdleme26f
• cdleme26f2ALTN
• cdleme26f2

riotasv3d

• cdlemefs32sn1aw
• cdleme43fsv1snlem
• cdleme41sn3a
• cdleme40m
• cdleme40n
• cdlemkid
• dihvalcqpre

[avekens]

https://us.metamath.org/mpeuni/ax-riotaBAD.html

As noted in #4248 there are several parts of set.mm with bad theorems, so this issue is about one "family" of them: those using ax-riotaBAD (~2.8% of set.mm)

This axiom is only used in https://us.metamath.org/mpeuni/riotaclbgBAD.html, where the inconsistency with set.mm is in the reverse direction. I'd expect that most of the time, deeper in the dependency chain (for instance https://us.metamath.org/mpeuni/glbconN.html), it should be possible to just prove uniqueness directly.

The discussion in #4248 is about BAD theorems in main, so not about BAD theorems in mathboxes like ~ax-riotaBAD, which is in a mathbox (and all theorems depending on it). Since axioms and theorems of mathboxes must not be used by others, there is no problem with them. Of corse, no BAD theorems should be moved from mathboxes to main unchanged.

As far as I can see, ~mreclatBAD is the only BAD theorem in main, so only this should be revised (or moved into a mathbox).

[avekens]

Regarding ax-riotaBAD: If it is planned that section "Hilbert lattices" should be moved to main, then, of course, the usage of ax-riotaBAD (and ax-riotaBAD itself) should be removed. This is, however, a bigger issue, the following sections in Norm's Mathbox are involved:

• 21.24.9 Ortholattices and orthomodular lattices cops
• 21.24.10 Atomic lattices with covering property ccvr
• 21.24.11 Hilbert lattices chlt
• 21.24.12 Projective geometries based on Hilbert lattices clln
• 21.24.13 Construction of a vector space from a Hilbert lattice cdlema1N
• 21.24.14 Construction of involution and inner product from a Hilbert lattice clpoN

[benjub]

I think both main-section theorems and mathbox theorems should be treated. Main-section theorems should be treated with higher priority, and @avekens is right to draw attention to https://us.metamath.org/mpeuni/mreclatBAD.html (also https://us.metamath.org/mpeuni/mreclatdemoBAD.html should be addressed).