search

metamath / set.mm

Metamath source file for logic and set theory
Other
243 stars 88 forks source link

add nsyl5 to main #4001

Closed wlammen closed 3 months ago

wlammen commented 3 months ago
  1. Add a new "negated syllogism inference" named nsyl5 to main. nsyl5 is to nsyl4 what nsyl is to nsyl3. I encountered the need for such an addition already several times (for example moexexlem,, wl-nax6im, and more), and today again while designing a proof. This time I had enough. I looked up simple patterns for a possible application, and let the metamath minimizer do the work. I currently count 44 replacements, saving 7 lines in total.
  2. In a few instances the minimizer found an even better result than just using nsyl5, particularly in mathboxes. I picked its suggestion in such a case. Affected here are inelpisys, itg2addnclem3, itgcoscmulx, iundjiunlem, smfmbfcex, setrec2lem1
  3. Mathbox: rename wl-df3mintru2-2 to wl-df2-3mintru2
  4. Mathbox: add rotating and commuting theorems to the 3mintru2 complex.