Revise iotan0

changes-set.txt

@@ -94,6 +94,7 @@ make a github issue.)
 
 DONE:
 Date      Old         New         Notes
+17-Oct-26 iotan0      [same]      Remove sethood requirement from antecedent
 14-Oct-26 flt4lem*    [same]      Revise to `( A gcd B ) = 1` to shorten overall
 30-Sep-26 cnvssb      [same]      Moved from RP's mathbox to main set.mm
 29-Sep-26 fununiq     [same]      Moved from SF's mathbox to main set.mm

discouraged

@@ -17386,6 +17386,7 @@ New usage of "intidl" is discouraged (2 uses).
 New usage of "intnatN" is discouraged (0 uses).
 New usage of "iorlid" is discouraged (2 uses).
 New usage of "iotaeq" is discouraged (0 uses).
+New usage of "iotan0OLD" is discouraged (0 uses).
 New usage of "ip0i" is discouraged (1 uses).
 New usage of "ip1i" is discouraged (2 uses).
 New usage of "ip1ilem" is discouraged (1 uses).
@@ -20722,6 +20723,7 @@ Proof modification of "int2" is discouraged (14 steps).
 Proof modification of "int3" is discouraged (17 steps).
 Proof modification of "intidl" is discouraged (503 steps).
 Proof modification of "iorlid" is discouraged (57 steps).
+Proof modification of "iotan0OLD" is discouraged (86 steps).
 Proof modification of "iscmgmALT" is discouraged (57 steps).
 Proof modification of "iscom2" is discouraged (130 steps).
 Proof modification of "iscringd" is discouraged (867 steps).

set.mm

@@ -62634,9 +62634,19 @@ Definite description binder (inverted iota)
     iotan0.1 $e |- ( x = A -> ( ph <-> ps ) ) $.
     $( Representation of "the unique element such that ` ph ` " with a class
        expression ` A ` which is not the empty set (that means that "the unique
-       element such that ` ph ` " exists).  (Contributed by AV,
-       30-Jan-2024.) $)
-    iotan0 $p |- ( ( A e. V /\ A =/= (/) /\ A = ( iota x ph ) ) -> ps ) $=
+       element such that ` ph ` " exists).  (Contributed by AV, 30-Jan-2024.)
+       Remove sethood antecedent.  (Revised by Eric Schmidt, 17-Oct-2026.) $)
+    iotan0 $p |- ( ( A =/= (/) /\ A = ( iota x ph ) ) -> ps ) $=
+      ( c0 wne cio wceq wa weu pm13.18 expcom iotanul necon1ai syl6 imp wi wcel
+      cvv iotaex eleq1 mpbiri eqcom iota2 biimprd biimtrid impancom mpancom mpd
+      adantl ) DFGZDACHZIZJACKZBULUNUOULUNUMFGZUOUNULUPDUMFLMUOUMFACNOPQUNUOBRZ
+      ULDTSZUNUQUNURUMTSACUADUMTUBUCURUOUNBUNUMDIZURUOJZBDUMUDUTBUSABCDTEUEUFUG
+      UHUIUKUJ $.
+
+    $( Obsolete version of ~ iotan0 as of 17-Oct-2026.  (Contributed by AV,
+       30-Jan-2024.)  (Proof modification is discouraged.)
+       (New usage is discouraged.) $)
+    iotan0OLD $p |- ( ( A e. V /\ A =/= (/) /\ A = ( iota x ph ) ) -> ps ) $=
       ( wcel c0 wne cio wceq w3a weu pm13.18 expcom iotanul necon1ai syl6 a1i
       wi 3imp wa eqcom iota2 biimprd biimtrid impancom 3adant2 mpd ) DEGZDHIZDA
       CJZKZLACMZBUJUKUMUNUKUMUNTTUJUKUMULHIZUNUMUKUODULHNOUNULHACPQRSUAUJUMUNBT
@@ -234011,14 +234021,13 @@ everywhere defined internal operation (see ~ mndcl ), whose operation is
        with this theorem.  (Contributed by AV, 29-Jan-2024.) $)
     sgrpidmnd $p |- ( ( G e. Smgrp /\ E. e e. B ( e =/= (/) /\ e = .0. ) )
                        -> G e. Mnd ) $=
-      ( vx vy csgrp wcel cv c0 wne wceq wa wrex cplusg co wral wi cfv cmnd eqid
-      cio grpidval eqeq2i w3a weq eleq1w oveq1 eqeq1d ovanraleqv anbi12d iotan0
-      rsp simpl2im 3expb expcom sylan2b impcom ralrimiv reximia anim2i ismnddef
-      ex sylibr ) CIJZBKZLMZVHDNZOZBAPZOVGVHGKZCQUAZRZVMNZVMVHVNRVMNOZGASZBAPZO
-      CUBJVLVSVGVKVRBAVHAJZVKVRVTVKOVQGAVKVTVMAJVQTZVJVIVHHKZAJZWBVMVNRZVMNZVMW
-      BVNRVMNOGASZOZHUDZNZVTWATDWHVHGAVNHCDEVNUCZFUEUFVTVIWIOWAVTVIWIWAVTVIWIUG
-      VTVRWAWGVTVROHVHAHBUHZWCVTWFVRHBAUIWEVPGVMWBVMVNAVHWKWDVOVMWBVHVMVNUJUKUL
-      UMUNVQGAUOUPUQURUSUTVAVEVBVCAVNBCGEWJVDVF $.
+      ( vx vy csgrp wcel cv c0 wne wceq wa wrex cplusg cfv co wral cmnd wi eqid
+      cio grpidval eqeq2i weq eleq1w oveq1 eqeq1d ovanraleqv anbi12d iotan0 rsp
+      simpl2im sylan2b ralrimiv reximi anim2i ismnddef sylibr ) CIJZBKZLMZVCDNZ
+      OZBAPZOVBVCGKZCQRZSZVHNZVHVCVISVHNOZGATZBAPZOCUAJVGVNVBVFVMBAVFVLGAVEVDVC
+      HKZAJZVOVHVISZVHNZVHVOVISVHNOGATZOZHUDZNZVHAJVLUBZDWAVCGAVIHCDEVIUCZFUEUF
+      VDWBOVCAJZVMWCVTWEVMOHVCHBUGZVPWEVSVMHBAUHVRVKGVHVOVHVIAVCWFVQVJVHVOVCVHV
+      IUIUJUKULUMVLGAUNUOUPUQURUSAVIBCGEWDUTVA $.
   $}
 
   ${