Define the indiscrete topology in iset.mm

[jkingdon]

The definition in set.mm - in https://us.metamath.org/mpeuni/indistopon.html and related theorems - is {∅, 𝐴} and that is not going to work intuitionistically.

We plan on defining it to be the collection of all sets such that the membership relation does not depend on x, i.e. { s | A. x e. s s = X }

The key theorems are the analogues to https://us.metamath.org/mpeuni/indistopon.html , https://us.metamath.org/mpeuni/indistop.html , https://us.metamath.org/mpeuni/indisuni.html , https://us.metamath.org/mpeuni/indistps.html , https://us.metamath.org/mpeuni/indistps2.html . There are a few more which depend on those, but that's the start.

[digama0]

I think you can also do similar things for the other topologies mentioned in #3088:

• finite complement topology: { s | A. x e. s E. t e. Fin A = ( s u. t ) }
• countable complement topology: { s | A. x e. s E. t ( t ~<_ om /\ A = ( s u. t ) ) }
• particular point topology: { s e. ~P A | A. x e. s P e. s }

[david-a-wheeler]

I'll ask my usual question: Should we modify the definition in set.mm so it would work in both set.mm and iset.mm? I suspect the answer may be "no" in this case, but I feel I should ask.

[benjub]

...the collection of all sets such that the membership relation does not depend on x, i.e. { s | A. x e. s s = X }

This sentence is not very clear and does not match the statement. I think a more transparent expression for the indiscrete topology on A (derived from an explicited version of the above sentence) is

{ x e. ~P A | F/ y e. A y e. x } 

where the restricted nonfreeness quantifier has the natural definition ( F/ x e. A ph <-> ( E. x e. A ph -> A. x e. A ph ) ). This expression is indeed equivalent to the one given by @digama0, and this should be a theorem, I think.

[digama0]

I think it's a bit much to add a restricted not-free quantifier just for that. FTR I got that definition by starting from A. x A. y ( x e. s -> y e. s ) and then progressively simplifying it, since we generally prefer short definitions and unpack them in subsequent theorems.

[benjub]

Yes, it wouldn't make sense to define the restricted nonfreeness quantifier just for that, but I think it's missing anyway (A., E., E!, E*, _iota, { | }, all have their restricted versions), so we might as well use it here once it's introduced.

Without using the nonfreeness quantifier, this would give { x e. ~P A | ( E. y e. A y e. x -> A. y e. A y e. x ) } which could also be written E. y e. ( A \cap x ) -> A \subseteq x, that is (since we know x \subseteq A), E. y e. x -> x = A that is, if x is inhabited, then it is equal to A. Your starting expression A. x A. y ( x e. s -> y e. s ) is also easy to grasp. Any of these could be the definition, and the equivalences shown as theorems. If the less transparent definition is chosen because it's shorter (though it still has a dummy variable), then the comment should be adapted, with link to an easier to grasp definition, since again, if you look at the top post above, it's not obvious at first sight that the comment (when made precise) and the formula are equivalent.

[jkingdon]

I'll ask my usual question: Should we modify the definition in set.mm so it would work in both set.mm and iset.mm? I suspect the answer may be "no" in this case, but I feel I should ask.

My usual answer is that we shouldn't do so if the modified definition would be significantly longer or more awkward, and this feels like such a situation to me. If you have excluded middle it is really odd to have to explain what's wrong with {∅, 𝐴}, given that the replacement is pretty hard to understand at a glance.

[david-a-wheeler]

Fair enough, I suspected that but I felt I had to ask.