On Mon, Dec 2, 2024 at 8:35 PM Igor Ieskov <[email protected]> wrote:
> I also was able to prove abaeqb. Similarly to Thierry’s proof, my proof > also introduced a disjoint condition for a and b, whereas the task has > disjoints showing that a and b should be non-disjoint. I spent some time > trying to find another proof which will not require this additional > disjoint for a and b, but I could not find it. On the one hand, as I > understand, requiring a and b to be disjoint, means that we cannot > substitute the same set for a and b simultaneously. Please correct me if I > am wrong. For example, with this new disjoint we will not be able to > “apply” this theorem to the statement |- ( ph -> A. x e. B A. x e. B ( x > .o. x ) e. B ). Also the original d-conditions look like it was made > deliberately that a and b should not be disjoint. On the other hand, it was > mentioned that “beware of possible problems in the statements (especially > in the d-conditions)”. Saveliy, could you please comment on that (is it > legal to add a disjoint for a and b and what was your intention)? > This is a typo, the theorem requires a and b to be disjoint. (If they were not disjoint, then you could apply the theorem with the two variables being the same to prove a stronger version of the theorem where you only assume the function is closed on the diagonal, which is not sufficient to prove the conclusion.) -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJSv3F1D_6WGsotSBdSebCEMEsxvg4BD9VjGLBjGXjYKrpA%40mail.gmail.com.
