Justify df-nfc with restatement by LegionMammal978 · Pull Request #5207 · metamath/set.mm

LegionMammal978 · 2026-02-18T21:23:21Z

This adds a justified restatement for df-nfc per my proposed approach to #4955. To centralize the documentation in one place (and to avoid conflating their purposes), I've created a copy of a1ii called "just", with some information about justified restatements. The rule is used as the final step of a justified restatement, to restate the definition while attaching the justification theorem to the overall proof tree. External tools are still necessary to ensure that a definition is sound, but this method ensures that the justification theorem is accounted for in the axiom usage.

After this change, all previous users of df-nfc use dfnfc instead, and dfnfc is the only direct user of df-nfc. Here's the diff in axiom usage:

Diff

@@ -1,5 +1,6 @@
 idi:
 a1ii:
+just:
 mp2: ax-mp
 mp2b: ax-mp
 a1i: ax-mp ax-1
@@ -2816,47 +2817,48 @@
 clabel: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 sbab: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-12 ax-ext
 nfcjust: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8
-nfci: ax-mp ax-1 ax-2 ax-3 ax-gen
-nfcii: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-10
+dfnfc: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8
+nfci: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8
+nfcii: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-10
 nfcr: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8
-nfcrALT: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-12
+nfcrALT: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-12
 nfcri: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8
-nfcd: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-12
+nfcd: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-12
 nfcrd: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8
 nfcrii: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-12
-nfceqdf: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-12 ax-ext
+nfceqdf: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-12 ax-ext
 nfceqi: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-ext
 nfcxfr: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-ext
 nfcxfrd: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-ext
-nfcv: ax-mp ax-1 ax-2 ax-3 ax-gen ax-5
-nfcvd: ax-mp ax-1 ax-2 ax-3 ax-gen ax-5
-nfab1: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-10
-nfnfc1: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-10 ax-11 ax-12
+nfcv: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8
+nfcvd: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8
+nfab1: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-10
+nfnfc1: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-10 ax-11 ax-12
 clelsb1fw: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-10 ax-11 ax-12
 clelsb1f: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-10 ax-11 ax-12 ax-13
-nfab: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-10 ax-11 ax-12
-nfabg: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-10 ax-11 ax-12 ax-13
-nfaba1: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-10 ax-11
-nfaba1OLD: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-10 ax-11 ax-12
-nfaba1g: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-10 ax-11 ax-12 ax-13
-nfeqd: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-ext
+nfab: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-10 ax-11 ax-12
+nfabg: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-10 ax-11 ax-12 ax-13
+nfaba1: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-10 ax-11
+nfaba1OLD: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-10 ax-11 ax-12
+nfaba1g: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-10 ax-11 ax-12 ax-13
+nfeqd: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 nfeld: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
-nfnfc: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-10 ax-11 ax-12
-nfeq: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-ext
+nfnfc: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-10 ax-11 ax-12
+nfeq: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 nfel: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
-nfeq1: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-ext
+nfeq1: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 nfel1: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
-nfeq2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-ext
+nfeq2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 nfel2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
-drnfc1: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-12 ax-13 ax-ext
-drnfc2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-13 ax-ext
-nfabdw: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-10 ax-11 ax-12
-nfabd: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-10 ax-11 ax-12 ax-13
-nfabd2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-13 ax-ext
+drnfc1: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-12 ax-13 ax-ext
+drnfc2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-13 ax-ext
+nfabdw: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-10 ax-11 ax-12
+nfabd: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-10 ax-11 ax-12 ax-13
+nfabd2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-13 ax-ext
 dvelimdc: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-13 ax-ext
 dvelimc: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-13 ax-ext
-nfcvf: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-13
-nfcvf2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-13
+nfcvf: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-13
+nfcvf2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-13
 cleqf: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-11 ax-12 ax-ext
 eqabf: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 abid2f: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
@@ -2961,8 +2963,8 @@
 nelne2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-ext
 nelelne: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-ext
 neneor: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-ext
-nfne: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-ext
-nfned: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-ext
+nfne: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
+nfned: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 nabbib: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-ext
 neli: ax-mp ax-1 ax-2 ax-3
 nelir: ax-mp ax-1 ax-2 ax-3
@@ -3369,7 +3371,7 @@
 abv: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-11 ax-ext
 abvALT: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-11 ax-ext
 isset: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-ext
-cbvexeqsetf: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-ext
+cbvexeqsetf: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 issetft: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 issetf: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 isseti: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8
@@ -4561,7 +4563,7 @@
 rabsnif: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 rabrsn: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 euabsn2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-ext
-euabsn: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-ext
+euabsn: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 reusn: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-ext
 absneu: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 rabsneu: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
@@ -34674,7 +34676,7 @@
 bj-spcimdvv: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8
 elelb: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-ext
 bj-pwvrelb: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-ext
-bj-nfcsym: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-13 ax-ext
+bj-nfcsym: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-13 ax-ext
 bj-sbeqALT: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 bj-sbeq: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 bj-sbceqgALT: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
@@ -36525,9 +36527,9 @@
 renegclALT: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext ax-sep ax-nul ax-pow ax-pr ax-un ax-resscn ax-1cn ax-icn ax-addcl ax-addrcl ax-mulcl ax-mulrcl ax-mulcom ax-addass ax-mulass ax-distr ax-i2m1 ax-1ne0 ax-1rid ax-rnegex ax-rrecex ax-cnre ax-pre-lttri ax-pre-lttrn ax-pre-ltadd
 elimhyps2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-ext
 dedths2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-ext
-nfcxfrdf: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-12 ax-ext
-nfded: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-ext
-nfded2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-9 ax-10 ax-11 ax-12 ax-ext
+nfcxfrdf: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-12 ax-ext
+nfded: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
+nfded2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 nfunidALT2: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 nfunidALT: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext
 nfopdALT: ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-8 ax-9 ax-10 ax-11 ax-12 ax-ext

GinoGiotto

Looks good. Approved.

LegionMammal978 · 2026-02-19T01:12:06Z

A funny note on the axioms: If we were to decompose the class A in nfcjust into setvar and class abstraction cases, then we can actually avoid ax-8 in the justification; it's not inherently necessary. But avoiding it in the setvar case (using distinctors) would require the most roundabout proof in the world, using ax-nul and ax-pr on top of every other FOL= axiom!

  ${
    $d x y z $.  $d w y z $.  $d ph y z $.
    $( Subcase of ~ nfcjust for ` A = { w | ph } ` , using ~ df-clab instead of
       ~ ax-8 and ~ df-clel .  (Contributed by MH, 18-Feb-2026.) $)
    nfcjustALTab $p |- ( A. y F/ x y e. { w | ph } <->
                         A. z F/ x z e. { w | ph } ) $=
      ( cv cab wcel wnf weq eleq1ab nfbidv cbvalvw ) CFAEGZHZBIDFNHZBICDCDJOPBA
      CDEKLM $.
  $}

  ${
    $d v x y z $.  $d w y z $.
    $( Subcase of ~ nfcjust for ` A = w ` , using ~ ax-9 , ~ ax-10 , ~ ax-11 ,
       ~ ax-12 , ~ ax-13 , ~ ax-nul , and ~ ax-pr instead of ~ ax-8 and
       ~ df-clel .  (Contributed by MH, 18-Feb-2026.) $)
    nfcjustALTset $p |- ( A. y F/ x y e. w <-> A. z F/ x z e. w ) $=
      ( vv cv wcel wnf wb weq wal wel wex wn wo ax-nul sp eximii exnal mpbi nf2
      wceq wi ax-pr 19.37iv orcs ax6evr exlimiiv notnoti pm3.2ni 2false 3bitr4i
      a1i elequ2 sps drnf2 3bitr3d hbn1 dveel2 nf5dh 2thd pm2.61i cbvalvw ) BFZ
      DFZGZAHZCFZVEGZAHZBCVGVJIZVDVHUBADJZAKZVKVMBALZAHZCALZAHZVGVJVOVQIVMVNAKZ
      VNAMZNZOZVPAKZVPAMZNZOZVOVQWAWEVRVTVNNZAMVRNWFBKWFAABPWFBQRVNASTVSBEJZVSE
      WGWGVSWGWGOZVNAWHVNUCZBKWIAEEABUDWIBQRUEUFEBUGUHUIUJWBWDVPNZAMWBNWJCKWJAA
      CPWJCQRVPASTWCCEJZWCEWKWKWCWKWKOZVPAWLVPUCZCKWMAEEACUDWMCQRUEUFECUGUHUIUJ
      UKVNAUAVPAUAULUMVNVFADAVLVNVFIAADBUNUOUPVPVIADAVLVPVIIAADCUNUOUPUQVMNZVGV
      JWNVFAVLAURZADBUSUTWNVIAWOADCUSUTVAVBUMVC $.
  $}

GinoGiotto · 2026-02-19T07:04:06Z

If you allow the use of set theory axioms then one could also avoid ax-6 by using ax6vsep, tho it adds ax-sep and ax-ext in both decompositions and I imagine the proof would be even more convoluted.

This reminds me of nrt2irr, which proves the irrationality of N-th roots of 2 by using Fermat's last theorem.

GinoGiotto · 2026-02-20T09:20:50Z

By the way, you discovered a proof of el that uses ax-12 instead of ax-8. I think this is interesting enough to be added in the database (perhaps as elALT3):

${
   $d x y t $.
   elALT3 $p |- E. y x e. y $=
    ( vt weq wel wex wo wi wal ax-pr sp eximii 19.37iv orcs ax6evr exlimiiv )
    ACDZABEZBFZCQQSQQGZRBTRHZAIUABCCBAJUAAKLMNCAOP $.
$}

MM> sh pr elALT3
29         eximii.1=ax-pr    $a |- E. y A. x ( ( x = t \/ x = t ) -> x e. y )
32         eximii.2=sp       $p |- ( A. x ( ( x = t \/ x = t ) -> x e. y ) -> ( ( x = t \/ x = t ) -> x e. y ) )
33       19.37iv.1=eximii  $p |- E. y ( ( x = t \/ x = t ) -> x e. y )
34     orcs.1=19.37iv    $p |- ( ( x = t \/ x = t ) -> E. y x e. y )
35   exlimiv.1=orcs    $p |- ( x = t -> E. y x e. y )
38   exlimiiv.2=ax6evr $p |- E. t x = t
39 elALT3=exlimiiv   $p |- E. y x e. y

Statement "elALT3" assumes the following axioms ($a statements):
  ax-mp ax-1 ax-2 ax-3 ax-gen ax-4 ax-5 ax-6 ax-7 ax-12 ax-pr

set.mm

LegionMammal978 force-pushed the just-df-nfc branch from 42b5429 to 8d848ea Compare February 18, 2026 21:26

Justify df-nfc, correct usage statements

f1be239

LegionMammal978 force-pushed the just-df-nfc branch from 8d848ea to f1be239 Compare February 18, 2026 21:38

GinoGiotto approved these changes Feb 18, 2026

View reviewed changes

wlammen reviewed Feb 20, 2026

View reviewed changes

set.mm Show resolved Hide resolved

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Justify df-nfc with restatement#5207

Justify df-nfc with restatement#5207
LegionMammal978 wants to merge 1 commit intometamath:developfrom
LegionMammal978:just-df-nfc

LegionMammal978 commented Feb 18, 2026

Uh oh!

GinoGiotto left a comment

Uh oh!

LegionMammal978 commented Feb 19, 2026 •

edited

Loading

Uh oh!

GinoGiotto commented Feb 19, 2026

Uh oh!

GinoGiotto commented Feb 20, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

LegionMammal978 commented Feb 18, 2026

Uh oh!

GinoGiotto left a comment

Choose a reason for hiding this comment

Uh oh!

LegionMammal978 commented Feb 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

GinoGiotto commented Feb 19, 2026

Uh oh!

GinoGiotto commented Feb 20, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

LegionMammal978 commented Feb 19, 2026 •

edited

Loading