Add exel (from mathbox sn-el), exex, exneq (from proof of dtru) #4521
Conversation
…update dtru and comments.
|
@tirix : Metamath swiss knife panics 😱 https://github.com/benjub/set.mm/actions/runs/12581185293/job/35064486255 (edit: link for this repo and not my fork: https://github.com/metamath/set.mm/actions/runs/12581203415/job/35064534429) |
| 9-Oct-2024.) (Proof modification is discouraged.) | ||
| (New usage is discouraged.) $) | ||
| (Contributed by NM, 7-Nov-2006.) Avoid ~ ax-13 . (Revised by BJ, | ||
| 31-May-2019.) (Revised by Gino Giotto, 5-Sep-2023.) Avoid ~ ax-12 . |
There was a problem hiding this comment.
I remember somewhere that you removed ax-13 before me, so you can remove my credit.
There was a problem hiding this comment.
I remember you had also removed ax-13 later and independently (since bj-dtru was in my mathbox, it was less visible). Following your comment, I am removing the tag concerning your revision.
| ~ ax-12 . (Revised by Rohan Ridenour, 9-Oct-2024.) Use ~ ax-pr instead | ||
| of ~ ax-pow . (Revised by BTernaryTau, 3-Dec-2024.) Extract this | ||
| result from the proof from ~ dtru . (Revised by BJ, 2-Jan-2025.) $) | ||
| exex $p |- E. x E. y -. x = y $= |
There was a problem hiding this comment.
I'd prefer exexneq here instead of exex. I would like exex to be bj-exexbiex when it will be moved in main. Notice that I called exexw with this idea in mind.
There was a problem hiding this comment.
I had considered that label exexneq before the PR, but thought it might be too long. Since you also thought of it and @icecream17 agrees, I'll go with it: better to be more explicit, even if slightly longer.
(On the other hand, exexw may not be explicit enough, compared to exexbiexw, even though the latter is quite long. And for instance, alex already exists for something different from bj-alexbiex. But that's another story.)
Done. You may of course update its comment later, since it is in your mathbox. Note the difference of nature between el (or elALT*) on the one hand and exel (or sn-exelALT) on the other hand: free variables are implicitly universally quantified. |
|
@tirix @digama0 : Metamath swiss knife panics 😱 🙀 https://github.com/metamath/set.mm/actions/runs/12597930645/job/35111826362 |
set.mm
Outdated
| $( $j usage 'exel' avoids 'ax-5' 'ax-7' 'ax-8' 'ax-9' 'ax-10 'ax-11' | ||
| 'ax-12' 'ax-13''ax-ext' 'ax-sep' 'ax-nul' 'ax-pow'; $) |
There was a problem hiding this comment.
Metamath knife panics because of the missing space between ax-13 and ax-ext.
A closing quote is also missing after ax-10 (here and in below), but that does not seem to be an issue.
There was a problem hiding this comment.
Clearly Metamath knife should not panic though, but raise an error. I'll open an issue to track this.
There was a problem hiding this comment.
Don't be sorry ! Thanks for fixing this PR and for opening the associated issue.
Add exel (from mathbox sn-el), exex, exneq (from proof of dtru), and update dtru and comments.
FYI @icecream17 @GinoGiotto @BTernaryTau and Rohan Ridenour, who contributed to the current form of these results.