Make an extensible structure a map from small integers to sets

[jkingdon]

In set.mm, "map" is not always true because an extensible structure can contain the empty set (not just ordered pairs). It is, however, true for many cases, for example see https://us.metamath.org/mpeuni/cnfldfun.html . For more background, see the https://us.metamath.org/mpeuni/df-struct.html and the section header above it.

My proposal is to make an extensible structure always a map and remove the empty set case. This will require using more sethood hypotheses, but since this is needed in iset.mm anyway (where the current set.mm tricks often won't work), this is well trodden territory. Once you get to anything with M e. Mgm, G e. Grp, etc, then the theorems don't need any changes; it is only an issue up to that point.

How we'd do it:

• Copy https://us.metamath.org/ileuni/strle1g.html , https://us.metamath.org/ileuni/strle2g.html , and https://us.metamath.org/ileuni/strle3g.html from iset.mm to set.mm
• Revise comment of df-struct to describe this intended direction
• Mark https://us.metamath.org/mpeuni/strle1.html , https://us.metamath.org/mpeuni/strle2.html , and https://us.metamath.org/mpeuni/strle3.html as discouraged, with strle1g, strle2g, and strle3g as the suggested replacements
• Mark https://us.metamath.org/mpeuni/ipsstr.html as deprecated and move https://us.metamath.org/ileuni/ipsstrd.html to set.mm as the suggested replacement. Probably also make an ipsstri as some set.mm usages likely could use that.
• Start avoiding the deprecated theorems and see what else needs the kind of sethood hypotheses needed in iset.mm (it will be fewer than iset.mm, because we still get to use fvex and the like).

Further past discussion:

• Extensible structures whose components are proper classes? #4145 (comment) concerning the empty set versus ordered pair question in particular
• I was asked at add extensible structures to iset.mm #3008 (comment) to make suggestions for improvements to extensible structures (particularly in the area of making them easier to understand and work with). I find it hard to keep the whole area in my head so I'm not going to attempt a comprehensive review of extensible structures in general, but this one proposal I think can make them easier to understand and probably avoid some special cases in some proofs.

[benjub]

I agree that the fact that (the first components of) extensible structures are not functions is not convenient. You write that defining them as functions "will require using more sethood hypotheses". This is not necessarily the case. The artificial exception made for the empty set in the definition of an extensible structure comes from the fact that a couple (by which I mean "ordered pair", to avoid confusion) constructed from at least one proper class is the empty set (https://us.metamath.org/mpeuni/opprc.html). That peculiar definition has other problems, and a definition of couples working for proper classes and giving a set if and only if its two components are sets would be much more convenient. By this, I mean the two important properties https://us.metamath.org/mpeuni/bj-2uplex.html and https://us.metamath.org/mpeuni/bj-2uplth.html.

Adopting that definition of couples (or any variant satisfying the above two important properties) would solve at once that problem about extensible structures, among others.

[jkingdon]

Adopting that definition of couples (or any variant satisfying the above two important properties) would solve at once that problem about extensible structures, among others.

I must admit that questions around the definition of ordered pair were not on my bingo card of what responses I expected to get when I created this issue. That does look like an interesting set of ideas, and there are some literature citations making it interesting reading whether or not we change the main definition of ordered pair in set.mm.

I can think of various considerations around this definition (including how extensible structures work if we adopt it) but even questions of how hard to pull at that thread make me think of getting more input from more people, including using features like polls and upvotes (most obviously achieved via #4288 although I suppose if people don't like that mechanism we could seek another).