diff --git a/set.mm b/set.mm
index 91bc13b7c3..21b4d0f963 100644
--- a/set.mm
+++ b/set.mm
@@ -583403,356 +583403,228 @@ A Fne if ( S = (/) , { X } , U. S ) ) $=
 $)
 
   ${
-    $d A u v w x $.  $d B u v w $.  $d R u v w $.
-    weiunlem1.1 $e |- F = ( w e. U_ x e. A B |-> ( iota_ u e.
-        { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) ) $.
-    $( Lemma for ~ weiunpo , ~ weiunso , ~ weiunfr , and ~ weiunse .
-       (Contributed by Matthew House, 23-Aug-2025.) $)
-    weiunlem1 $p |- ( ( R We A /\ R Se A ) -> ( F : U_ x e. A B --> A /\
-        A. w e. U_ x e. A B w e. [_ ( F ` w ) / x ]_ B /\ A. w e. U_ x e. A B
-        A. v e. A ( w e. [_ v / x ]_ B -> -. v R ( F ` w ) ) ) ) $=
-      ( wa cv csb wcel wral wbr wn wi wceq nfcv sylib wwe wse ciun wf crab crio
-      cfv ssrab2 wreu c0 wne wrex eliun sylbb2 wss wereu2 mpanr1 sylan2 riotacl
-      rabn0 syl sselid fmptd simpr fvmpt2 syl2anc eqeltrd elrabsf simprd sbcel2
-      wsbc ralrimiva eqcomd wb cmpt nfriota1 nfmpt nfcxfr nffv nfn nfralw nfra1
-      nfbr nfriota nfeq2 breq2 notbid ralbid riota2f mpbird anbi2i bitri imbi1i
-      impexp ralbii2 3jca ) EGUAEGUBJZAEFUCZEHUDBKZAWSHUGZFLMZBWRNWSACKZFLMZXBW
-      TGOZPZQZCENZBWRNWQBWRXBDKZGOZPZCWSFMZAEUEZNZDXLUFZEHWQWSWRMZJZXLEXNXKAEUH
-      ZXPXMDXLUIZXNXLMZXOWQXLUJUKZXRXOXKAEULXTAWSEFUMXKAEUTUNWQXLEUOXTXRXQDCEXL
-      GUPUQURZXMDXLUSVAZVBIVCWQXABWRXPXKAWTVKZXAXPWTEMZYCXPWTXLMZYDYCJXPWTXNXLX
-      PXOXSWTXNRWQXOVDYBBWRXNXLHIVEVFZYBVGZXKAWTEAESZVHTVIAWTWSFVJTVLWQXGBWRXPX
-      ECXLNZXGXPYIXNWTRZXPWTXNYFVMXPYEXRYIYJVNYGYAXMYIDXLWTDWSHDHBWRXNVOZIDBWRX
-      NDWRSXMDXLVPVQVRDWSSVSZXEDCXLDXLSXDDDXBWTGDXBSDGSYLWCVTWAXHWTRZXJXECXLCXH
-      WTCWSHCHYKICBWRXNCWRSXMCDXLXJCXLWBCXLSWDVQVRCWSSVSWEYMXIXDXHWTXBGWFWGWHWI
-      VFWJXEXFCXLEXBXLMZXEQXBEMZXCJZXEQYOXFQYNYPXEYNYOXKAXBVKZJYPXKAXBEYHVHYQXC
-      YOAXBWSFVJWKWLWMYOXCXEWNWLWOTVLWP $.
-  $}
-
-  ${
-    $d A u v w x $.  $d A s t v w x $.  $d B u $.  $d B s t v w $.  $d F s t $.
-    $d R u $.  $d R s t v w $.
-    weiunlem2.1 $e |- F = ( w e. U_ x e. A B |-> ( iota_ u e.
-        { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) ) $.
-    $( Lemma for ~ weiunpo , ~ weiunso , and ~ weiunse .  (Contributed by
-       Matthew House, 23-Aug-2025.) $)
-    weiunlem2 $p |- ( ( R We A /\ R Se A ) -> ( F : U_ x e. A B --> A /\
-        A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B /\ A. t e. U_ x e. A B
-        A. s e. A ( t e. [_ s / x ]_ B -> -. s R ( F ` t ) ) ) ) $=
-      ( cv csb wcel wral wbr wn wi nfv nfcv wwe wse ciun cfv w3a weiunlem1 biid
-      wa wf crab crio cmpt nfmpt1 nfcxfr nffv nfcsbw nfcri weq id fveq2 csbeq1d
-      eleq12d cbvralw nfbr nfn nfim nfralw nfra1 nfmpt wceq csbeq1 eleq2d breq1
-      nfriota notbid imbi12d eleq1w breq2d ralbidv bitrid 3anbi123i sylib ) FHU
-      AFHUBUHAFGUCZFIUIZBLZAWEIUDZGMZNZBWCOZWEACLZGMZNZWJWFHPZQZRZCFOZBWCOZUEWD
-      ELZAWRIUDZGMZNZEWCOZWRAJLZGMZNZXCWSHPZQZRZJFOZEWCOZUEABCDFGHIKUFWDWDWIXBW
-      QXJWDUGWHXABEWCWHESBEWTBAWSGBWRIBIBWCWJDLHPQZCWEGNAFUJZOZDXLUKZULZKBWCXNU
-      MUNBWRTUOZBGTUPUQBEURZWEWRWGWTXQUSXQAWFWSGWEWRIUTZVAVBVCWPXIBEWCWPESXHBJF
-      BFTXEXGBXEBSXFBBXCWSHBXCTBHTXPVDVEVFVGWPWEXDNZXCWFHPZQZRZJFOXQXIWOYBCJFWO
-      JSXSYACXSCSXTCCXCWFHCXCTCHTCWEICIXOKCBWCXNCWCTXMCDXLXKCXLVHCXLTVNVIUNCWET
-      UOVDVEVFWJXCVJZWLXSWNYAYCWKXDWEAWJXCGVKVLYCWMXTWJXCWFHVMVOVPVCXQYBXHJFXQX
-      SXEYAXGBEXDVQXQXTXFXQWFWSXCHXRVRVOVPVSVTVCWAWB $.
-  $}
-
-  ${
-    $d A u v w x $.  $d A p s t x $.  $d A p q r x y z $.  $d B u $.
-    $d B s t v w $.  $d B p q r y z $.  $d F y z $.  $d F s t $.  $d R u $.
-    $d R s v w $.  $d R q r t $.  $d R p q r y z $.  $d S s $.
-    $d S p q r y z $.  $d T p q r $.
-    weiunpo.1 $e |- F = ( w e. U_ x e. A B |-> ( iota_ u e.
-        { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) ) $.
-    weiunpo.2 $e |- T = { <. y , z >. | ( ( y e. U_ x e. A B /\
+    $d ph t $.  $d A m n o p q r s t u v w x $.  $d A x y z $.
+    $d B m n o p q r s t u v w $.  $d B y z $.  $d C y z $.  $d D y z $.
+    $d E n o s t $.  $d F m n o p q r s t y z $.  $d R m n o p q r s t u v w $.
+    $d R y z $.  $d S m n o p q r s t y z $.  $d T n o p q r $.  $d V p q t $.
+    weiun.1 $e |- F = ( w e. U_ x e. A B |-> ( iota_ u e. { x e. A | w e. B }
+        A. v e. { x e. A | w e. B } -. v R u ) ) $.
+    weiun.2 $e |- T = { <. y , z >. | ( ( y e. U_ x e. A B /\
         z e. U_ x e. A B ) /\ ( ( F ` y ) R ( F ` z ) \/
         ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) ) } $.
+    $( Lemma for ~ weiunpo , ~ weiunso , ~ weiunfr , and ~ weiunse .
+       (Contributed by Matthew House, 8-Sep-2025.) $)
+    weiunlem1 $p |- ( C T D <-> ( ( C e. U_ x e. A B /\
+        D e. U_ x e. A B ) /\ ( ( F ` C ) R ( F ` D ) \/
+        ( ( F ` C ) = ( F ` D ) /\ C [_ ( F ` C ) / x ]_ S D ) ) ) ) $=
+      ( cfv wbr wceq wa cv csb ciun simpl fveq2d simpr breq12d eqeq12d breq123d
+      wo csbeq1d anbi12d orbi12d brab2a ) BUAZNQZCUAZNQZKRZUPURSZUOUQAUPLUBZRZT
+      ZUJINQZJNQZKRZVDVESZIJAVDLUBZRZTZUJBCIJAGHUCZVKMUOISZUQJSZTZUSVFVCVJVNUPV
+      DURVEKVNUOINVLVMUDZUEZVNUQJNVLVMUFZUEZUGVNUTVGVBVIVNUPVDURVEVPVRUHVNUOIUQ
+      JVAVHVOVNAUPVDLVPUKVQUIULUMPUN $.
+
+    ${
+      weiunlem2.3 $e |- ( ph -> R We A ) $.
+      weiunlem2.4 $e |- ( ph -> R Se A ) $.
+      $( Lemma for ~ weiunpo , ~ weiunso , ~ weiunfr , and ~ weiunse .
+         (Contributed by Matthew House, 23-Aug-2025.) $)
+      weiunlem2 $p |- ( ph -> ( F : U_ x e. A B --> A /\
+          A. t e. U_ x e. A B t e. [_ ( F ` t ) / x ]_ B /\
+          A. s e. A A. t e. [_ s / x ]_ B -. s R ( F ` t ) ) ) $=
+        ( vr wwe wse ciun wf cv cfv csb wcel wral wbr w3a wfn crab crio riotaex
+        wn wa fnmpti a1i wceq weq breq2 notbid ralbidv cbvriotavw rabbidv breq1
+        eleq1w cbvralvw raleqdv bitrid riotaeqbidv eqtrid fvmpt3i adantl c0 wne
+        wreu wrex eliun rabn0 bitr4i wss ssrab2 wereu2 sylan2b riotacl2 eqeltrd
+        mpanr1 elrabi 3syl ralrimiva ffnfv sylanbrc wsbc dfsbcq elrabsf simprbi
+        syl nfcv vtoclga sbcel2 sylib simpr anbi2i bitri sylibr ne0d syldan rsp
+        elrab sylc ralrimivva 3jca syl2anc ) AIKUAZIKUBZBIJUCZINUDZHUEZBXTNUFZJ
+        UGUHZHXRUIZOUEZYAKUJZUPZHBYDJUGZUIOIUIZUKRSXPXQUQZXSYCYHYINXRULZYAIUHZH
+        XRUIXSYJYIEXRFUEZGUEZKUJZUPZFEUEJUHZBIUMZUIZGYQUNZNYRGYQUOZPURUSYIYKHXR
+        YIXTXRUHZUQZYAYDTUEZKUJZUPZOXTJUHZBIUMZUIZTUUGUMZUHZYAUUGUHZYKUUBYAUUHT
+        UUGUNZUUIUUAYAUULUTYIEXTYSUULXRNEHVAZYSYLUUCKUJZUPZFYQUIZTYQUNUULYRUUPG
+        TYQGTVAZYOUUOFYQUUQYNUUNYMUUCYLKVBVCVDVEUUMUUPUUHTYQUUGUUMYPUUFBIEHJVHV
+        FZUUPUUEOYQUIUUMUUHUUOUUEFOYQFOVAUUNUUDYLYDUUCKVGVCVIUUMUUEOYQUUGUURVJV
+        KVLVMPYTVNVOUUBUUHTUUGVRZUULUUIUHUUAYIUUGVPVQZUUSUUAUUFBIVSUUTBXTIJVTUU
+        FBIWAWBZYIUUGIWCUUTUUSUUFBIWDTOIUUGKWEWIWFUUHTUUGWGWSWHZUUHTYAUUGWJZUUF
+        BYAIWJWKWLHXRINWMWNYIYBHXRUUBUUFBYAWOZYBUUBUUJUUKUVDUVBUVCUUFBYDWOZUVDO
+        YAUUGUUFBYDYAWPYDUUGUHZYDIUHZUVEUUFBYDIBIWTWQZWRXAWKBYAXTJXBXCWLYIYFOHI
+        YGYIUVGXTYGUHZUQZUQZYFOUUGUIZUVFYFYIUVJUUAUVLUVKUUTUUAUVKUUGYDUVKUVJUVF
+        YIUVJXDUVFUVGUVEUQUVJUVHUVEUVIUVGBYDXTJXBXEXFXGZXHUVAXGUUBUUJUVLUVBUUJU
+        UKUVLUUHUVLTYAUUGUUCYAUTZUUEYFOUUGUVNUUDYEUUCYAYDKVBVCVDXKWRWSXIUVMYFOU
+        UGXJXLXMXNXO $.
+
+      weiunfrlem.5 $e |- E =
+          ( iota_ p e. ( F " r ) A. q e. ( F " r ) -. q R p ) $.
+      weiunfrlem.6 $e |- ( ph -> r C_ U_ x e. A B ) $.
+      weiunfrlem.7 $e |- ( ph -> r =/= (/) ) $.
+      $( Lemma for ~ weiunfr .  (Contributed by Matthew House, 23-Aug-2025.) $)
+      weiunfrlem $p |- ( ph -> ( E e. ( F " r ) /\ A. t e. r -. ( F ` t ) R E
+          /\ A. t e. ( r i^i [_ E / x ]_ B ) ( F ` t ) = E ) ) $=
+        ( vo vn vs cv cima wcel cfv wbr wn wral wceq csb cin crab crio wreu wwe
+        wa wse wss c0 wne ciun wf weiunlem2 simp1d fimassd cdm sseqtrrd sseqin2
+        sylib eqnetrd imadisjlnd wereu2 syl22anc riotacl2 syl weq simpr breq12d
+        fdmd simpl notbid cbvraldva cbvrabv 3eltr4g breq2 ralbidv simpld simprd
+        elrab wfn wb ffnd breq1 ralima syl2anc mpbid wel elin1d syl2an2r csbeq1
+        rspa raleqbidv simp3d sseldd rspcdva elin2d wor weso ffvelcdmd sotrieq2
+        adantr syl12anc mpbir2and ralrimiva 3jca ) ANOPUIZUJZUKZHUIZOULZNKUMZUN
+        ZHYCUOZYGNUPZHYCBNJUQZURZUOAYEUFUIZNKUMZUNZUFYDUOZANYNUGUIZKUMZUNZUFYDU
+        OZUGYDUSZUKYEYQVCAQUIZRUIZKUMZUNZQYDUOZRYDUTZUUGRYDUSZNUUBAUUGRYDVAZUUH
+        UUIUKAIKVBZIKVDYDIVEYDVFVGUUJUAUBABIJVHZIOYCAUULIOVIZYFBYGJUQUKHUULUOZU
+        HUIZYGKUMZUNZHBUUOJUQZUOZUHIUOZABCDEFGHIJKLMOUHSTUAUBVJZVKZVLZAOYCAOVMZ
+        YCURZYCVFAYCUVDVEUVEYCUPAYCUULUVDUDAUULIOUVBWFVNYCUVDVOVPUEVQVRRQIYDKVS
+        VTUUGRYDWAWBUCUUAUUGUGRYDUGRWCZYTUUFUFQYDUVFUFQWCZVCZYSUUEUVHYNUUCYRUUD
+        KUVFUVGWDUVFUVGWGWEWHWIWJWKUUAYQUGNYDYRNUPZYTYPUFYDUVIYSYOYRNYNKWLWHWMW
+        PVPZWNZAYQYJAYEYQUVJWOAOUULWQYCUULVEZYQYJWRAUULIOUVBWSUDYPYIUFHUULYCOYN
+        YGUPYOYHYNYGNKWTWHXAXBXCZAYKHYMAYFYMUKZVCZYKYINYGKUMZUNZAYJUVNHPXDYIUVM
+        UVOYCYLYFAUVNWDZXEZYIHYCXHXFAUVQHYLUOZUVNYFYLUKUVQAUUSUVTUHINUUONUPZUUQ
+        UVQHUURYLBUUONJXGUWAUUPUVPUUONYGKWTWHXIAUUMUUNUUTUVAXJAYDINUVCUVKXKZXLU
+        VOYCYLYFUVRXMUVQHYLXHXFUVOIKXNZYGIUKNIUKZYKYIUVQVCWRAUWCUVNAUUKUWCUAIKX
+        OWBXRUVOUULIYFOAUUMUVNUVBXRUVOYCUULYFAUVLUVNUDXRUVSXKXPAUWDUVNUWBXRIYGN
+        KXQXSXTYAYB $.
+    $}
+
     $( A partial ordering on an indexed union can be constructed from a
-       well-ordering on its index set and a collection of partial orderings on
-       its members.  (Contributed by Matthew House, 23-Aug-2025.) $)
+       well-ordering on its index class and a collection of partial orderings
+       on its members.  (Contributed by Matthew House, 23-Aug-2025.) $)
     weiunpo $p |- ( ( R We A /\ R Se A /\ A. x e. A S Po B ) ->
         T Po U_ x e. A B ) $=
-      ( vt wbr wa wcel wceq csbeq1d vp vq vr vs wwe wse wpo wral w3a cv wn ciun
-      wi cfv csb wo wor simpl1 syl wf simpl2 weiunlem2 syl2anc simp1d ffvelcdmd
-      weso simpr1 sonr csbeq1 poeq1 poeq2 bitrd simpl3 nfv nfcsb1v nfpo csbeq1a
-      wb weq cbvralw sylib rspcdva id fveq2 eleq12d simp2d poirr ioran sylanbrc
-      intnand simpl fveq2d simpr breq12d eqeq12d anbi12d orbi12d brab2a simprbi
-      breq123d nsyl simpr3 jca simpr2 sotr syl13anc imp orcd ex simprll eqbrtrd
-      simprr simprl simprrl breqtrd eqtrd simprlr simprrr breqd mpbird eleqtrrd
-      adantr potr mp2and ccased syl2ani biimpri syl6an ralrimivvva df-po sylibr
-      olcd ) GIUEZGIUFZHJUGZAGUHZUIZUAUJZYRKPZUKZYRUBUJZKPZUUAUCUJZKPZQZYRUUCKP
-      ZUMZQZUCAGHULZUHUBUUIUHUAUUIUHUUIKUGYQUUHUAUBUCUUIUUIUUIYQYRUUIRZUUAUUIRZ
-      UUCUUIRZUIZQZYTUUGUUNYRLUNZUUOIPZUUOUUOSZYRYRAUUOJUOZPZQZUPZYSUUNUUPUKZUU
-      TUKUVAUKUUNGIUQZUUOGRZUVBUUNYMUVCYMYNYPUUMURZGIVFUSZUUNUUIGYRLUUNUUIGLUTZ
-      OUJZAUVHLUNZHUOZRZOUUIUHZUVHAUDUJZHUOZRUVMUVIIPUKUMUDGUHOUUIUHZUUNYMYNUVG
-      UVLUVOUIUVEYMYNYPUUMVAADEFOGHILUDMVBVCZVDZYQUUJUUKUULVGZVEZGUUOIVHVCUUNUU
-      SUUQUUNAUUOHUOZUURUGZYRUVTRZUUSUKUUNUVNAUVMJUOZUGZUWAUDGUUOUVMUUOSZUWDUVN
-      UURUGZUWAUWEUWCUURSUWDUWFVRAUVMUUOJVIUVNUWCUURVJUSUWEUVNUVTSUWFUWAVRAUVMU
-      UOHVIUVNUVTUURVKUSVLUUNYPUWDUDGUHYMYNYPUUMVMYOUWDAUDGYOUDVNAUVNUWCAUVMJVO
-      AUVMHVOVPAUDVSZYOHUWCUGZUWDUWGJUWCSYOUWHVRAUVMJVQHJUWCVJUSUWGHUVNSUWHUWDV
-      RAUVMHVQHUVNUWCVKUSVLVTWAUVSWBZUUNUVKUWBOUUIYRUVHYRSZUVHYRUVJUVTUWJWCUWJA
-      UVIUUOHUVHYRLWDTWEUUNUVGUVLUVOUVPWFZUVRWBZUVTYRUURWGVCWJUUPUUTWHWIYSUUJUU
-      JQUVABUJZLUNZCUJZLUNZIPZUWNUWPSZUWMUWOAUWNJUOZPZQZUPZUVABCYRYRUUIUUIKBUAV
-      SZUWOYRSZQZUWQUUPUXAUUTUXEUWNUUOUWPUUOIUXEUWMYRLUXCUXDWKZWLZUXEUWOYRLUXCU
-      XDWMZWLZWNUXEUWRUUQUWTUUSUXEUWNUUOUWPUUOUXGUXIWOUXEUWMYRUWOYRUWSUURUXFUXE
-      AUWNUUOJUXGTUXHWTWPWQNWRWSXAUUNUUJUULQZUUEUUOUUCLUNZIPZUUOUXKSZYRUUCUURPZ
-      QZUPZUUFUUNUUJUULUVRYQUUJUUKUULXBZXCUUBUUNUUOUUALUNZIPZUUOUXRSZYRUUAUURPZ
-      QZUPZUXRUXKIPZUXRUXKSZUUAUUCAUXRJUOZPZQZUPZUXPUUDUUBUUJUUKQUYCUXBUYCBCYRU
-      UAUUIUUIKUXCUWOUUASZQZUWQUXSUXAUYBUYKUWNUUOUWPUXRIUYKUWMYRLUXCUYJWKZWLZUY
-      KUWOUUALUXCUYJWMZWLZWNUYKUWRUXTUWTUYAUYKUWNUUOUWPUXRUYMUYOWOUYKUWMYRUWOUU
-      AUWSUURUYLUYKAUWNUUOJUYMTUYNWTWPWQNWRWSUUDUUKUULQUYIUXBUYIBCUUAUUCUUIUUIK
-      UWMUUASZCUCVSZQZUWQUYDUXAUYHUYRUWNUXRUWPUXKIUYRUWMUUALUYPUYQWKZWLZUYRUWOU
-      UCLUYPUYQWMZWLZWNUYRUWRUYEUWTUYGUYRUWNUXRUWPUXKUYTVUBWOUYRUWMUUAUWOUUCUWS
-      UYFUYSUYRAUWNUXRJUYTTVUAWTWPWQNWRWSUUNUXSUYDUYBUYHUXPUUNUXSUYDQZUXPUUNVUC
-      QUXLUXOUUNVUCUXLUUNUVCUVDUXRGRUXKGRVUCUXLUMUVFUVSUUNUUIGUUALUVQYQUUJUUKUU
-      LXDZVEUUNUUIGUUCLUVQUXQVEGUUOUXRUXKIXEXFXGXHXIUUNUYBUYDQZUXPUUNVUEQZUXLUX
-      OVUFUUOUXRUXKIUUNUXTUYAUYDXJUUNUYBUYDXLXKXHXIUUNUXSUYHQZUXPUUNVUGQZUXLUXO
-      VUHUUOUXRUXKIUUNUXSUYHXMUUNUXSUYEUYGXNXOXHXIUUNUYBUYHQZUXPUUNVUIQZUXOUXLV
-      UJUXMUXNVUJUUOUXRUXKUUNUXTUYAUYHXJZUUNUYBUYEUYGXNXPZVUJUYAUUAUUCUURPZUXNU
-      UNUXTUYAUYHXQVUJVUMUYGUUNUYBUYEUYGXRVUJUURUYFUUAUUCVUJAUUOUXRJVUKTXSXTVUJ
-      UWAUWBUUAUVTRUUCUVTRUYAVUMQUXNUMUUNUWAVUIUWIYBUUNUWBVUIUWLYBVUJUUAAUXRHUO
-      ZUVTUUNUUAVUNRZVUIUUNUVKVUOOUUIUUAOUBVSZUVHUUAUVJVUNVUPWCVUPAUVIUXRHUVHUU
-      ALWDTWEUWKVUDWBYBVUJAUUOUXRHVUKTYAVUJUUCAUXKHUOZUVTUUNUUCVUQRZVUIUUNUVKVU
-      ROUUIUUCOUCVSZUVHUUCUVJVUQVUSWCVUSAUVIUXKHUVHUUCLWDTWEUWKUXQWBYBVUJAUUOUX
-      KHVULTYAUVTYRUUAUUCUURYCXFYDXCYLXIYEYFUUFUXJUXPQUXBUXPBCYRUUCUUIUUIKUXCUY
-      QQZUWQUXLUXAUXOVUTUWNUUOUWPUXKIVUTUWMYRLUXCUYQWKZWLZVUTUWOUUCLUXCUYQWMZWL
-      ZWNVUTUWRUXMUWTUXNVUTUWNUUOUWPUXKVVBVVDWOVUTUWMYRUWOUUCUWSUURVVAVUTAUWNUU
-      OJVVBTVVCWTWPWQNWRYGYHXCYIUAUBUCUUIKYJYK $.
-  $}
-
-  ${
-    $d A u v w x $.  $d A q s t x $.  $d A q r x y z $.  $d B u $.
-    $d B s t v w $.  $d B q r y z $.  $d F y z $.  $d F s t $.  $d R u $.
-    $d R r t $.  $d R s v w $.  $d R q r y z $.  $d S s $.  $d S q r y z $.
-    $d T q r $.
-    weiunso.1 $e |- F = ( w e. U_ x e. A B |-> ( iota_ u e.
-        { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) ) $.
-    weiunso.2 $e |- T = { <. y , z >. | ( ( y e. U_ x e. A B /\
-        z e. U_ x e. A B ) /\ ( ( F ` y ) R ( F ` z ) \/
-        ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) ) } $.
+      ( vt vs wbr wa wcel wceq vp vq vr wwe wse wpo wral w3a cv wn ciun cfv csb
+      wi wo wor simpl1 weso wf simpl2 weiunlem2 simp1d simpr1 ffvelcdmd syl2anc
+      syl sonr csbeq1 poeq1 poeq2 bitrd simpl3 nfv nfcsb1v nfpo csbeq1a cbvralw
+      wb weq sylib rspcdva id fveq2 csbeq1d eleq12d simp2d poirr ioran sylanbrc
+      intnand weiunlem1 simprbi nsyl simpr3 jca simpr2 sotr syl13anc orc simprr
+      syl6 simprll eqbrtrd orcd ex simprl simprrl breqtrd eqtrd simprlr simprrr
+      breqd mpbird adantr eleqtrrd potr mp2and olcd syl2ani biimpri ralrimivvva
+      ccased syl6an df-po sylibr ) GIUDZGIUEZHJUFZAGUGZUHZUAUIZYKKQZUJZYKUBUIZK
+      QZYNUCUIZKQZRZYKYPKQZUNZRZUCAGHUKZUGUBUUBUGUAUUBUGUUBKUFYJUUAUAUBUCUUBUUB
+      UUBYJYKUUBSZYNUUBSZYPUUBSZUHZRZYMYTUUGYKLULZUUHIQZUUHUUHTZYKYKAUUHJUMZQZR
+      ZUOZYLUUGUUIUJZUUMUJUUNUJUUGGIUPZUUHGSZUUOUUGYFUUPYFYGYIUUFUQZGIURVFZUUGU
+      UBGYKLUUGUUBGLUSZOUIZAUVALULZHUMZSZOUUBUGZPUIZUVBIQUJOAUVFHUMZUGPGUGZUUGA
+      BCDEFOGHIJKLPMNUURYFYGYIUUFUTVAZVBZYJUUCUUDUUEVCZVDZGUUHIVGVEUUGUULUUJUUG
+      AUUHHUMZUUKUFZYKUVMSZUULUJUUGUVGAUVFJUMZUFZUVNPGUUHUVFUUHTZUVQUVGUUKUFZUV
+      NUVRUVPUUKTUVQUVSVRAUVFUUHJVHUVGUVPUUKVIVFUVRUVGUVMTUVSUVNVRAUVFUUHHVHUVG
+      UVMUUKVJVFVKUUGYIUVQPGUGYFYGYIUUFVLYHUVQAPGYHPVMAUVGUVPAUVFJVNAUVFHVNVOAP
+      VSZYHHUVPUFZUVQUVTJUVPTYHUWAVRAUVFJVPHJUVPVIVFUVTHUVGTUWAUVQVRAUVFHVPHUVG
+      UVPVJVFVKVQVTUVLWAZUUGUVDUVOOUUBYKOUAVSZUVAYKUVCUVMUWCWBUWCAUVBUUHHUVAYKL
+      WCWDWEUUGUUTUVEUVHUVIWFZUVKWAZUVMYKUUKWGVEWJUUIUUMWHWIYLUUCUUCRUUNABCDEFG
+      HYKYKIJKLMNWKWLWMUUGUUCUUERZYRUUHYPLULZIQZUUHUWGTZYKYPUUKQZRZUOZYSUUGUUCU
+      UEUVKYJUUCUUDUUEWNZWOYOUUGUUHYNLULZIQZUUHUWNTZYKYNUUKQZRZUOZUWNUWGIQZUWNU
+      WGTZYNYPAUWNJUMZQZRZUOZUWLYQYOUUCUUDRUWSABCDEFGHYKYNIJKLMNWKWLYQUUDUUERUX
+      EABCDEFGHYNYPIJKLMNWKWLUUGUWOUWTUWRUXDUWLUUGUWOUWTRZUWHUWLUUGUUPUUQUWNGSU
+      WGGSUXFUWHUNUUSUVLUUGUUBGYNLUVJYJUUCUUDUUEWPZVDUUGUUBGYPLUVJUWMVDGUUHUWNU
+      WGIWQWRUWHUWKWSXAUUGUWRUWTRZUWLUUGUXHRZUWHUWKUXIUUHUWNUWGIUUGUWPUWQUWTXBU
+      UGUWRUWTWTXCXDXEUUGUWOUXDRZUWLUUGUXJRZUWHUWKUXKUUHUWNUWGIUUGUWOUXDXFUUGUW
+      OUXAUXCXGXHXDXEUUGUWRUXDRZUWLUUGUXLRZUWKUWHUXMUWIUWJUXMUUHUWNUWGUUGUWPUWQ
+      UXDXBZUUGUWRUXAUXCXGXIZUXMUWQYNYPUUKQZUWJUUGUWPUWQUXDXJUXMUXPUXCUUGUWRUXA
+      UXCXKUXMUUKUXBYNYPUXMAUUHUWNJUXNWDXLXMUXMUVNUVOYNUVMSYPUVMSUWQUXPRUWJUNUU
+      GUVNUXLUWBXNUUGUVOUXLUWEXNUXMYNAUWNHUMZUVMUUGYNUXQSZUXLUUGUVDUXROUUBYNOUB
+      VSZUVAYNUVCUXQUXSWBUXSAUVBUWNHUVAYNLWCWDWEUWDUXGWAXNUXMAUUHUWNHUXNWDXOUXM
+      YPAUWGHUMZUVMUUGYPUXTSZUXLUUGUVDUYAOUUBYPOUCVSZUVAYPUVCUXTUYBWBUYBAUVBUWG
+      HUVAYPLWCWDWEUWDUWMWAXNUXMAUUHUWGHUXOWDXOUVMYKYNYPUUKXPWRXQWOXRXEYBXSYSUW
+      FUWLRABCDEFGHYKYPIJKLMNWKXTYCWOYAUAUBUCUUBKYDYE $.
+
     $( A strict ordering on an indexed union can be constructed from a
-       well-ordering on its index set and a collection of strict orderings on
+       well-ordering on its index class and a collection of strict orderings on
        its members.  (Contributed by Matthew House, 23-Aug-2025.) $)
     weiunso $p |- ( ( R We A /\ R Se A /\ A. x e. A S Or B ) ->
         T Or U_ x e. A B ) $=
       ( vs vt wcel wa wbr wceq vq vr wwe wse wor wral w3a ciun wpo sopo weiunpo
-      ralimi syl3an3 cv cfv w3o csb simplrl simplrr animorrl simpl fveq2d simpr
-      breq12d eqeq12d csbeq1d breq123d anbi12d orbi12d brab2a syl21anbrc 3mix1d
-      wo wb csbeq1 soeq1 syl soeq2 simpll3 nfv nfcsb1v nfso weq csbeq1a cbvralw
-      bitrd sylib wf wn simpl1 simpl2 weiunlem2 syl2anc simp1d simprl ffvelcdmd
-      wi adantr rspcdva id fveq2 eleq12d simp2d eleqtrrd solin syl12anc simpllr
-      anim1i olcd sylanbrc ex idd simplr eqcomd breqdi jca 3orim123d mpd 3mix3d
-      weso simprr mpjao3dan issod ) GIUCZGIUDZHJUEZAGUFZUGZUAUBAGHUHZKYGYDYEHJU
-      IZAGUFYIKUIYFYJAGHJUJULABCDEFGHIJKLMNUKUMYHUAUNZYIQZUBUNZYIQZRZRZYKLUOZYM
-      LUOZISZYKYMKSZYKYMTZYMYKKSZUPZYQYRTZYRYQISZYPYSRZYTUUAUUBUUFYLYNYSUUDYKYM
-      AYQJUQZSZRZVMZYTYHYLYNYSURYHYLYNYSUSYPYSUUIUTBUNZLUOZCUNZLUOZISZUULUUNTZU
-      UKUUMAUULJUQZSZRZVMZUUJBCYKYMYIYIKUUKYKTZUUMYMTZRZUUOYSUUSUUIUVCUULYQUUNY
-      RIUVCUUKYKLUVAUVBVAZVBZUVCUUMYMLUVAUVBVCZVBZVDUVCUUPUUDUURUUHUVCUULYQUUNY
-      RUVEUVGVEUVCUUKYKUUMYMUUQUUGUVDUVCAUULYQJUVEVFUVFVGVHVINVJZVKVLYPUUDRZUUH
-      UUAYMYKUUGSZUPZUUCUVIAYQHUQZUUGUEZYKUVLQZYMUVLQUVKUVIAOUNZHUQZAUVOJUQZUEZ
-      UVMOGYQUVOYQTZUVRUVPUUGUEZUVMUVSUVQUUGTUVRUVTVNAUVOYQJVOUVPUVQUUGVPVQUVSU
-      VPUVLTUVTUVMVNAUVOYQHVOUVPUVLUUGVRVQWFUVIYGUVROGUFYDYEYGYOUUDVSYFUVRAOGYF
-      OVTAUVPUVQAUVOJWAAUVOHWAWBAOWCZYFHUVQUEZUVRUWAJUVQTYFUWBVNAUVOJWDHJUVQVPV
-      QUWAHUVPTUWBUVRVNAUVOHWDHUVPUVQVRVQWFWEWGYPYQGQZUUDYPYIGYKLYPYIGLWHZPUNZA
-      UWELUOZHUQZQZPYIUFZUWEUVPQUVOUWFISWIWQOGUFPYIUFZYPYDYEUWDUWIUWJUGYDYEYGYO
-      WJZYDYEYGYOWKADEFPGHILOMWLWMZWNZYHYLYNWOWPZWRWSUVIUWHUVNPYIYKPUAWCZUWEYKU
-      WGUVLUWOWTUWOAUWFYQHUWEYKLXAVFXBYPUWIUUDYPUWDUWIUWJUWLXCWRZYHYLYNUUDURZWS
-      UVIYMAYRHUQZUVLUVIUWHYMUWRQPYIYMPUBWCZUWEYMUWGUWRUWSWTUWSAUWFYRHUWEYMLXAV
-      FXBUWPYHYLYNUUDUSZWSUVIAYQYRHYPUUDVCZVFXDUVLYKYMUUGXEXFUVIUUHYTUUAUUAUVJU
-      UBUVIUUHYTUVIUUHRZYOUUJYTYHYOUUDUUHXGUXBUUIYSUVIUUDUUHUXAXHXIUVHXJXKUVIUU
-      AXLUVIUVJUUBUVIUVJRZYNYLUUEYRYQTZYMYKAYRJUQZSZRZVMZUUBUVIYNUVJUWTWRUVIYLU
-      VJUWQWRUXCUXGUUEUXCUXDUXFUXCYQYRYPUUDUVJXMZXNUXCUUGUXEYMYKUXCAYQYRJUXIVFU
-      VIUVJVCXOXPXIUUTUXHBCYMYKYIYIKUUKYMTZUUMYKTZRZUUOUUEUUSUXGUXLUULYRUUNYQIU
-      XLUUKYMLUXJUXKVAZVBZUXLUUMYKLUXJUXKVCZVBZVDUXLUUPUXDUURUXFUXLUULYRUUNYQUX
-      NUXPVEUXLUUKYMUUMYKUUQUXEUXMUXLAUULYRJUXNVFUXOVGVHVINVJZVKXKXQXRYPUUERZUU
-      BYTUUAUXRYNYLUXHUUBYHYLYNUUEUSYHYLYNUUEURYPUUEUXGUTUXQVKXSYPGIUEZUWCYRGQY
-      SUUDUUEUPYPYDUXSUWKGIXTVQUWNYPYIGYMLUWMYHYLYNYAWPGYQYRIXEXFYBYC $.
-  $}
-
-  ${
-    $d s x $.  $d r s t w $.  $d A s t w $.  $d A u v w x $.  $d B s $.
-    $d B u v w $.  $d C w $.  $d R u v $.  $d R s t w $.  $d F s t w $.
-    weiunfrlem1.1 $e |- F = ( w e. U_ x e. A B |-> ( iota_ u e.
-        { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) ) $.
-    weiunfrlem1.2 $e |- C = ( iota_ s e. ( F " r )
-        A. t e. ( F " r ) -. t R s ) $.
-    $( Lemma for ~ weiunfr .  (Contributed by Matthew House, 23-Aug-2025.) $)
-    weiunfrlem1 $p |- ( ( ( R We A /\ R Se A ) /\ ( r C_ U_ x e. A B /\
-        r =/= (/) ) ) -> ( C e. ( F " r ) /\ A. w e. r -. ( F ` w ) R C ) ) $=
-      ( wa cv wbr wn wral wcel wwe wse ciun wss c0 wne cfv cima crab crio simpl
-      wreu csb w3a weiunlem1 adantr simp1d fimassd cdm cin wceq simprl sseqtrrd
-      wf wi fdmd sseqin2 simprr eqnetrd imadisjlnd wereu2 syl12anc riotacl2 syl
-      sylib eqeltrid ffnd notbid ralima rabbidv syl2anc eleqtrd nfriota1 nfcxfr
-      wfn breq1 nfcv nfbr nfn nfralw breq2 ralbidv elrabf ) FIUAFIUBOZLPZAFGUCZ
-      UDZWOUEUFZOZOZHBPZJUGZKPZIQZRZBWOSZKJWOUHZUIZTHXGTXBHIQZRZBWOSZOWTHEPZXCI
-      QZRZEXGSZKXGUIZXHWTHXOKXGUJZXPNWTXOKXGULZXQXPTWTWNXGFUDXGUEUFXRWNWSUKWTWP
-      FJWOWTWPFJVDZXAAXBGUMTBWPSZXAACPZGUMTYAXBIQRVECFSBWPSZWNXSXTYBUNWSABCDFGI
-      JMUOUPUQZURWTJWOWTJUSZWOUTZWOUEWTWOYDUDYEWOVAWTWOWPYDWNWQWRVBZWTWPFJYCVFV
-      CWOYDVGVOWNWQWRVHVIVJKEFXGIVKVLXOKXGVMVNVPWTJWPWEZWQXPXHVAWTWPFJYCVQYFYGW
-      QOXOXFKXGXNXEEBWPWOJXLXBVAXMXDXLXBXCIWFVRVSVTWAWBXFXKKHXGKHXQNXOKXGWCWDZK
-      XGWGXJKBWOKWOWGXIKKXBHIKXBWGKIWGYHWHWIWJXCHVAZXEXJBWOYIXDXIXCHXBIWKVRWLWM
-      VO $.
-  $}
+      ralimi syl3an3 cv cfv weq w3o csb wo simplrl simplrr weiunlem1 syl21anbrc
+      animorrl 3mix1d csbeq1 soeq1 syl soeq2 bitrd simpll3 nfcsb1v nfso csbeq1a
+      wb nfv sylib wf wn simpl1 simpl2 weiunlem2 simp1d simprl ffvelcdmd adantr
+      cbvralw rspcdva fveq2 csbeq1d eleq12d simp2d simpr eleqtrrd solin simpllr
+      id syl12anc anim1i sylanbrc ex idd simplr eqcomd breqdi jca 3orim123d mpd
+      olcd 3mix3d weso simprr mpjao3dan issod ) GIUCZGIUDZHJUEZAGUFZUGZUAUBAGHU
+      HZKXRXOXPHJUIZAGUFXTKUIXQYAAGHJUJULABCDEFGHIJKLMNUKUMXSUAUNZXTQZUBUNZXTQZ
+      RZRZYBLUOZYDLUOZISZYBYDKSZUAUBUPZYDYBKSZUQZYHYITZYIYHISZYGYJRZYKYLYMYQYCY
+      EYJYOYBYDAYHJURZSZRZUSZYKXSYCYEYJUTXSYCYEYJVAYGYJYTVDABCDEFGHYBYDIJKLMNVB
+      ZVCVEYGYORZYSYLYDYBYRSZUQZYNUUCAYHHURZYRUEZYBUUFQZYDUUFQUUEUUCAOUNZHURZAU
+      UIJURZUEZUUGOGYHUUIYHTZUULUUJYRUEZUUGUUMUUKYRTUULUUNVOAUUIYHJVFUUJUUKYRVG
+      VHUUMUUJUUFTUUNUUGVOAUUIYHHVFUUJUUFYRVIVHVJUUCXRUULOGUFXOXPXRYFYOVKXQUULA
+      OGXQOVPAUUJUUKAUUIJVLAUUIHVLVMAOUPZXQHUUKUEZUULUUOJUUKTXQUUPVOAUUIJVNHJUU
+      KVGVHUUOHUUJTUUPUULVOAUUIHVNHUUJUUKVIVHVJWGVQYGYHGQZYOYGXTGYBLYGXTGLVRZPU
+      NZAUUSLUOZHURZQZPXTUFZUUIUUTISVSPUUJUFOGUFZYGABCDEFPGHIJKLOMNXOXPXRYFVTZX
+      OXPXRYFWAWBZWCZXSYCYEWDWEZWFWHUUCUVBUUHPXTYBPUAUPZUUSYBUVAUUFUVIWQUVIAUUT
+      YHHUUSYBLWIWJWKYGUVCYOYGUURUVCUVDUVFWLWFZXSYCYEYOUTZWHUUCYDAYIHURZUUFUUCU
+      VBYDUVLQPXTYDPUBUPZUUSYDUVAUVLUVMWQUVMAUUTYIHUUSYDLWIWJWKUVJXSYCYEYOVAZWH
+      UUCAYHYIHYGYOWMZWJWNUUFYBYDYRWOWRUUCYSYKYLYLUUDYMUUCYSYKUUCYSRZYFUUAYKXSY
+      FYOYSWPUVPYTYJUUCYOYSUVOWSXIUUBWTXAUUCYLXBUUCUUDYMUUCUUDRZYEYCYPYIYHTZYDY
+      BAYIJURZSZRZUSZYMUUCYEUUDUVNWFUUCYCUUDUVKWFUVQUWAYPUVQUVRUVTUVQYHYIYGYOUU
+      DXCZXDUVQYRUVSYDYBUVQAYHYIJUWCWJUUCUUDWMXEXFXIABCDEFGHYDYBIJKLMNVBZVCXAXG
+      XHYGYPRZYMYKYLUWEYEYCUWBYMXSYCYEYPVAXSYCYEYPUTYGYPUWAVDUWDVCXJYGGIUEZUUQY
+      IGQYJYOYPUQYGXOUWFUVEGIXKVHUVHYGXTGYDLUVGXSYCYEXLWEGYHYIIWOWRXMXN $.
 
-  ${
-    $d q x $.  $d A u v w x $.  $d A o r w x $.  $d A r s t w x $.
-    $d A p t x y z $.  $d B s $.  $d B q $.  $d B o r $.  $d B u v w $.
-    $d B p t y z $.  $d C o $.  $d C p v w $.  $d C p q t $.  $d F v $.
-    $d F s $.  $d F o w $.  $d F t y z $.  $d R s $.  $d R u v $.
-    $d R o r w $.  $d R p t x y z $.  $d S o r $.  $d S q r $.  $d S p t y z $.
-    $d T p r t $.
-    weiunfrlem2.1 $e |- F = ( w e. U_ x e. A B |-> ( iota_ u e.
-        { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) ) $.
-    weiunfrlem2.2 $e |- T = { <. y , z >. | ( ( y e. U_ x e. A B /\
-        z e. U_ x e. A B ) /\ ( ( F ` y ) R ( F ` z ) \/
-        ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) ) } $.
-    weiunfrlem2.3 $e |- C = ( iota_ s e. ( F " r )
-        A. t e. ( F " r ) -. t R s ) $.
-    $( Lemma for ~ weiunfr .  (Contributed by Matthew House, 23-Aug-2025.) $)
-    weiunfrlem2 $p |- ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) ->
-        T Fr U_ x e. A B ) $=
-      ( wcel vp vq vo wwe wse wfr wral w3a cv ciun wss c0 wne wa wbr wn wrex wi
-      wal csb cin cvv vex inex1 a1i cima wf cfv weiunlem1 adantr simp1d fimassd
-      3adantl3 weiunfrlem1 simpld sseldd simpl3 crio crab cmpt nfiu1 nfrab1 nfv
-      nfralw nfriota nfmpt nfcxfr nfcv nfima nfra1 nffr nfim wceq csbeq1a freq1
-      nfcsb1 wb syl freq2 bitrd imbi2d rsp com12 vtoclgaf sylc inss2 wfun ffund
-      fvelima syl2anc simprl simplrl simp2d fveq2 csbeq1d rspcv csbeq1 ad2antll
-      id eleq12d eleqtrd elind ne0d rexlimddv fri syl22anc elin1d wo simprd weq
-      breq1d notbid mpan9 simp3d simpl simpr fveq2d breq12d ad2antrr ex imbi12d
-      rspc2gv mp2d wor simpll1 weso ffvelcdmd sotrieq2 syl12anc mpbir2and breq2
-      elin2d mpbird simplr sselda eqtrd simprr breq1 breqd mtbird pm4.56 biimpi
-      imnan intnand eqeq12d breq123d anbi12d orbi12d brab2a ralrimiva reximssdv
-      sylib sylnibr alrimiv df-fr sylibr ) HKUDZHKUEZILUFZAHUGZUHZPUIZAHIUJZUKZ
-      UWBULUMZUNZGUIZUAUIZMUOZUPZGUWBUGZUAUWBUQZURZPUSUWCMUFUWAUWMPUWAUWFUWLUWA
-      UWFUNZUBUIZUWHAJLUTZUOZUPZUBUWBAJIUTZVAZUGZUWKUAUWBUWTUWNUWTVBTZUWSUWPUFZ
-      UWTUWSUKZUWTULUMZUXAUAUWTUQUXBUWNUWBUWSPVCVDVEUWNJHTZUVTUXCUWNNUWBVFZHJUW
-      NUWCHNUWBUWNUWCHNVGZDUIZAUXINVHZIUTZTZDUWCUGZUXIAEUIZIUTZTZUXNUXJKUOZUPZU
-      RZEHUGDUWCUGZUVQUVRUWFUXHUXMUXTUHZUVTUVQUVRUNUYAUWFADEFHIKNQVIVJVMZVKZVLU
-      WNJUXGTZUXJJKUOZUPZDUWBUGZUVQUVRUWFUYDUYGUNZUVTADEFGHIJKNOPQSVNVMZVOZVPZU
-      VQUVRUVTUWFVQUVTUVSURUVTUXCURAJHAJUWGOUIKUOUPZGUXGUGZOUXGVRSUYMAOUXGUYLAG
-      UXGANUWBANDUWCUXNFUIKUOUPZEUXIITZAHVSZUGZFUYPVRZVTQADUWCUYRAHIWAUYQAFUYPU
-      YNAEUYPUYOAHWBZUYNAWCWDUYSWEWFWGAUWBWHWIZUYLAWCWDUYTWEWGZUVTUXCAUVSAHWJAU
-      WSUWPAJLVUAWPAJIVUAWPWKWLAUIZJWMZUVSUXCUVTVUCUVSIUWPUFZUXCVUCLUWPWMUVSVUD
-      WQAJLWNILUWPWOWRVUCIUWSWMVUDUXCWQAJIWNIUWSUWPWSWRWTXAUVTVUBHTUVSUVSAHXBXC
-      XDXEUXDUWNUWBUWSXFVEUWNUCUIZNVHZJWMZUXEUCUWBUWNNXGUYDVUGUCUWBUQUWNUWCHNUY
-      CXHUYJUCJUWBNXIXJUWNVUEUWBTZVUGUNZUNZUWTVUEVUJUWBUWSVUEUWNVUHVUGXKZVUJVUE
-      AVUFIUTZUWSVUJVUEUWCTUXMVUEVULTZVUJUWBUWCVUEUWAUWDUWEVUIXLVUKVPUWNUXMVUIU
-      WNUXHUXMUXTUYBXMZVJUXLVUMDVUEUWCUXIVUEWMZUXIVUEUXKVULVUOXSVUOAUXJVUFIUXIV
-      UENXNXOXTXPXEVUGVULUWSWMUWNVUHAVUFJIXQXRYAYBYCYDUAUBUWSUWTVBUWPYEYFUWNUWH
-      UWTTZUXAUNZUNZUWBUWSUWHUWNVUPUXAXKZYGZVURUWJGUWBVURUWGUWBTZUNZUWGUWCTZUWH
-      UWCTZUNZUWGNVHZUWHNVHZKUOZVVFVVGWMZUWGUWHAVVFLUTZUOZUNZYHZUNUWIVVBVVMVVEV
-      VBVVHUPZVVLUPZVVMUPZVVBVVNVVFJKUOZUPZVURUYGVVAVVRVURUYDUYGUWNUYHVUQUYIVJY
-      IZUYFVVRDUWGUWBDGYJZUYEVVQVVTUXJVVFJKUXIUWGNXNZYKYLXPYMVVBVVGJWMZVVNVVRWQ
-      VURVWBVVAVURVWBVVGJKUOZUPZJVVGKUOZUPZVURUWHUWBTUYGVWDVUTVVSUYFVWDDUWHUWBU
-      XIUWHWMZUYEVWCVWGUXJVVGJKUXIUWHNXNYKYLXPXEVURUXTUWHUWSTZVWFVURUXHUXMUXTUW
-      NUYAVUQUYBVJYNVURUWBUWSUWHVUSUULVURVVDUXFUXTVWHVWFURZURVURUWBUWCUWHUWAUWD
-      UWEVUQXLZVUTVPZUWNUXFVUQUYKVJZUXSVWIDEUWHJUWCHVWGUXNJWMZUNZUXPVWHUXRVWFVW
-      NUXIUWHUXOUWSVWGVWMYOZVWNAUXNJIVWGVWMYPZXOXTVWNUXQVWEVWNUXNJUXJVVGKVWPVWN
-      UXIUWHNVWOYQYRYLUUAUUBXJUUCVURHKUUDZVVGHTUXFVWBVWDVWFUNWQVURUVQVWQUVQUVRU
-      VTUWFVUQUUEHKUUFWRVURUWCHUWHNUWNUXHVUQUYCVJVWKUUGVWLHVVGJKUUHUUIUUJVJZVWB
-      VVHVVQVVGJVVFKUUKYLWRUUMVVBVVIVVKUPZURVVOVVBVVIVWSVVBVVIUNZVVKUWGUWHUWPUO
-      ZVWTUWGUWTTUXAVXAUPZVWTUWBUWSUWGVURVVAVVIUUNVWTUWGAVVFIUTZUWSVVBUWGVXCTZV
-      VIVVBVVCUXMVXDVURUWBUWCUWGVWJUUOUWNUXMVUQVVAVUNYSUXLVXDDUWGUWCVVTUXIUWGUX
-      KVXCVVTXSVVTAUXJVVFIVWAXOXTXPXEVJVWTAVVFJIVWTVVFVVGJVVBVVIYPVVBVWBVVIVWRV
-      JUUPZXOYAYBVURUXAVVAVVIUWNVUPUXAUUQYSUWRVXBUBUWGUWTUWOUWGWMUWQVXAUWOUWGUW
-      HUWPUURYLXPXEVWTVVJUWPUWGUWHVWTAVVFJLVXEXOUUSUUTYTVVIVVKUVCUVLVVNVVOUNVVP
-      VVHVVLUVAUVBXJUVDBUIZNVHZCUIZNVHZKUOZVXGVXIWMZVXFVXHAVXGLUTZUOZUNZYHVVMBC
-      UWGUWHUWCUWCMBGYJZCUAYJZUNZVXJVVHVXNVVLVXQVXGVVFVXIVVGKVXQVXFUWGNVXOVXPYO
-      ZYQZVXQVXHUWHNVXOVXPYPZYQZYRVXQVXKVVIVXMVVKVXQVXGVVFVXIVVGVXSVYAUVEVXQVXF
-      UWGVXHUWHVXLVVJVXRVXQAVXGVVFLVXSXOVXTUVFUVGUVHRUVIUVMUVJUVKYTUVNPUAGUWCMU
-      VOUVP $.
-  $}
-
-  ${
-    $d A n r s x $.  $d A l o p t x $.  $d A k m u v w x $.
-    $d A l o p x y z $.  $d A k l m n v w x $.  $d B n $.  $d B m u v w $.
-    $d B k l r s t $.  $d B l o p y z $.  $d F n $.  $d F k q s t $.
-    $d F o p y z $.  $d R n q $.  $d R m u v w $.  $d R k q r s t $.
-    $d R l o p y z $.  $d S l r t $.  $d S l o p y z $.  $d T r t $.
-    weiunfr.1 $e |- F = ( w e. U_ x e. A B |-> ( iota_ u e.
-        { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) ) $.
-    weiunfr.2 $e |- T = { <. y , z >. | ( ( y e. U_ x e. A B /\
-        z e. U_ x e. A B ) /\ ( ( F ` y ) R ( F ` z ) \/
-        ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) ) } $.
     $( A well-founded relation on an indexed union can be constructed from a
-       well-ordering on its index set and a collection of well-founded
+       well-ordering on its index class and a collection of well-founded
        relations on its members.  (Contributed by Matthew House,
        23-Aug-2025.) $)
     weiunfr $p |- ( ( R We A /\ R Se A /\ A. x e. A S Fr B ) ->
         T Fr U_ x e. A B ) $=
-      ( vl vk vm cv wbr wcel vo vp vn vt vq vs vr wwe wse csb wfr wral w3a ciun
-      wn cima crio crab cmpt weq breq2 notbid ralbidv cbvriotavw nfcv nfv nfcri
-      nfcsb1v csbeq1a eleq2d cbvrabw eleq1w rabbidv eqtrid wb breq1 adantl wceq
-      adantr cbvraldva2 riotaeqbidv cbvmptv cbviun 3eqtri wa cfv wo copab simpl
-      mpteq1i a1i eleq12d anbi12d fveq2d breq12d eqeq12d csbeq1d csbcow eqtr4di
-      simpr breq123d orbi12d cbvopabv eqtri cbvralvw riotabiia weiunfrlem2 nffr
-      freq1 syl freq2 bitrd cbvralw 3anbi3i ax-mp 3imtr4i ) GIUHZGIUIZAORZHUJZA
-      XSJUJZUKZOGULZUMOGXTUNZKUKZXQXRHJUKZAGULZUMAGHUNZKUKZOUAUBPUCQUDGXTUERZUF
-      RZISZUOZUELUGRUPZULZUFYNUQIYAKLUFUGLDYHERZFRZISZUOZEDRZHTZAGURZULZFUUBUQZ
-      USPYHUCRZQRZISZUOZUCPRXTTZOGURZULZQUUJUQZUSPYDUULUSMDPYHUUDUULDPUTZUUDYPU
-      UFISZUOZEUUBULZQUUBUQUULUUCUUPFQUUBFQUTZYSUUOEUUBUUQYRUUNYQUUFYPIVAVBVCVD
-      UUMUUPUUKQUUBUUJUUMUUBYTXTTZOGURUUJUUAUURAOGAGVEOGVEUUAOVFADXTAXSHVHZVGAO
-      UTZHXTYTAXSHVIZVJVKUUMUURUUIOGDPXTVLVMVNZUUMUUOUUHEUCUUBUUJEUCUTZUUOUUHVO
-      UUMUVCUUNUUGYPUUEUUFIVPVBVQUUMUUBUUJVRUVCUVBVSVTWAVNWBPYHYDUULAOGHXTOHVEU
-      USUVAWCZWJWDKBRZYHTZCRZYHTZWEZUVELWFZUVGLWFZISZUVJUVKVRZUVEUVGAUVJJUJZSZW
-      EZWGZWEZBCWHUARZYDTZUBRZYDTZWEZUVSLWFZUWALWFZISZUWDUWEVRZUVSUWAOUWDYAUJZS
-      ZWEZWGZWEZUAUBWHNUVRUWLBCUAUBBUAUTZCUBUTZWEZUVIUWCUVQUWKUWOUVFUVTUVHUWBUW
-      OUVEUVSYHYDUWMUWNWIZYHYDVRZUWOUVDWKZWLUWOUVGUWAYHYDUWMUWNWTZUWRWLWMUWOUVL
-      UWFUVPUWJUWOUVJUWDUVKUWEIUWOUVEUVSLUWPWNZUWOUVGUWALUWSWNZWOUWOUVMUWGUVOUW
-      IUWOUVJUWDUVKUWEUWTUXAWPUWOUVEUVSUVGUWAUVNUWHUWPUWOUVNAUWDJUJUWHUWOAUVJUW
-      DJUWTWQAOUWDJWRWSUWSXAWMXBWMXCXDYOUDRZYKISZUOZUDYNULZUFYNYOUXEVOYKYNTYMUX
-      DUEUDYNUEUDUTYLUXCYJUXBYKIVPVBXEWKXFXGYGYCXQXRYFYBAOGYFOVFAXTYAAXSJVHUUSX
-      HUUTYFHYAUKZYBUUTJYAVRYFUXFVOAXSJVIHJYAXIXJUUTHXTVRUXFYBVOUVAHXTYAXKXJXLX
-      MXNUWQYIYEVOUVDYHYDKXKXOXP $.
-  $}
-
-  ${
-    $d A u v w x $.  $d A q s t x $.  $d A p q r s $.  $d A p q x y z $.
-    $d B u $.  $d B s t v w $.  $d B p q y z $.  $d F r $.  $d F s t $.
-    $d F q y z $.  $d R u $.  $d R r $.  $d R s t v w $.  $d R p q y z $.
-    $d S y z $.  $d T p q $.  $d V p q $.
-    weiunse.1 $e |- F = ( w e. U_ x e. A B |-> ( iota_ u e.
-        { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) ) $.
-    weiunse.2 $e |- T = { <. y , z >. | ( ( y e. U_ x e. A B /\
-        z e. U_ x e. A B ) /\ ( ( F ` y ) R ( F ` z ) \/
-        ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) ) } $.
+      ( vr vt wral wa wbr wn vo vn vm vq vp vs wwe wse wfr w3a cv ciun wss wrex
+      c0 wne wi wal cima crio csb cin cvv wceq wb csbeq1 freq1 syl freq2 simpl3
+      bitrd nfv nfcsb1v nffr weq csbeq1a cbvralw sylib wf wcel simpl1 weiunlem2
+      cfv simpl2 simp1d fimassd eqid simprl simprr weiunfrlem rspcdva inss2 a1i
+      sseldd vex inex1 ffund fvelima syl2anc wel simplrl simp2d r19.21bi syldan
+      wfun csbeq1d eleqtrd elind ne0d rexlimddv elin1d wo fveq2 breq1d ad2antrr
+      frd notbid simpr fveqeq2 simp3d breq2d mtbird simplr id eleq12d ad3antrrr
+      breq1 adantr eqtrd breqd ex imnan pm4.56 biimpi intnand weiunlem1 sylnibr
+      ralrimiva reximssdv alrimiv df-fr sylibr ) GIUGZGIUHZHJUIZAGQZUJZOUKZAGHU
+      LZUMZUUHUOUPZRZUAUKZUBUKZKSZTZUAUUHQZUBUUHUNZUQZOURUUIKUIUUGUUSOUUGUULUUR
+      UUGUULRZUCUKZUUNAUDUKUEUKISTUDLUUHUSZQUEUVBUTZJVAZSZTZUCUUHAUVCHVAZVBZQZU
+      UQUBUUHUVHUUTUBUCUVGUVHUVDVCUUTAUFUKZHVAZAUVJJVAZUIZUVGUVDUIZUFGUVCUVJUVC
+      VDZUVMUVKUVDUIZUVNUVOUVLUVDVDUVMUVPVEAUVJUVCJVFUVKUVLUVDVGVHUVOUVKUVGVDUV
+      PUVNVEAUVJUVCHVFUVKUVGUVDVIVHVKUUTUUFUVMUFGQUUCUUDUUFUULVJUUEUVMAUFGUUEUF
+      VLAUVKUVLAUVJJVMAUVJHVMVNAUFVOZUUEHUVLUIZUVMUVQJUVLVDUUEUVRVEAUVJJVPHJUVL
+      VGVHUVQHUVKVDUVRUVMVEAUVJHVPHUVKUVLVIVHVKVQVRUUTUVBGUVCUUTUUIGLUUHUUTUUIG
+      LVSZPUKZAUVTLWCZHVAZVTZPUUIQZUVJUWAISTPUVKQUFGQZUUTABCDEFPGHIJKLUFMNUUCUU
+      DUUFUULWAZUUCUUDUUFUULWDZWBZWEZWFUUTUVCUVBVTZUWAUVCISZTZPUUHQZUWAUVCVDZPU
+      VHQZUUTABCDEFPGHIJKUVCLOUDUEMNUWFUWGUVCWGUUGUUJUUKWHZUUGUUJUUKWIWJZWEZWNW
+      KUVHUVGUMUUTUUHUVGWLWMUVHVCVTUUTUUHUVGOWOWPWMUUTUWNUVHUOUPPUUHUUTLXEUWJUW
+      NPUUHUNUUTUUIGLUWIWQUWRPUVCUUHLWRWSUUTPOWTZUWNRZRZUVHUVTUXAUUHUVGUVTUUTUW
+      SUWNWHZUXAUVTUWBUVGUUTUWTUVTUUIVTUWCUXAUUHUUIUVTUUGUUJUUKUWTXAUXBWNUUTUWC
+      PUUIUUTUVSUWDUWEUWHXBZXCXDUXAAUWAUVCHUUTUWSUWNWIXFXGXHXIXJXPUUTUUNUVHVTZU
+      VIRZRZUUHUVGUUNUUTUXDUVIWHXKUXFUUPUAUUHUXFUAOWTZRZUUMUUIVTZUUNUUIVTRZUUML
+      WCZUUNLWCZISZUXKUXLVDZUUMUUNAUXKJVAZSZRZXLZRUUOUXHUXRUXJUXHUXMTZUXQTZUXRT
+      ZUXHUXMUXKUVCISZUXHUWLUYBTPUUHUUMPUAVOZUWKUYBUYCUWAUXKUVCIUVTUUMLXMZXNXQU
+      XHUWJUWMUWOUUTUWJUWMUWOUJUXEUXGUWQXOZXBUXFUXGXRZWKUXHUXLUVCUXKIUXHUWNUXLU
+      VCVDZPUVHUUNUVTUUNUVCLXSUXHUWJUWMUWOUYEXTUUTUXDUVIUXGXAWKZYAYBUXHUXNUXPTZ
+      UQUXTUXHUXNUYIUXHUXNRZUXPUUMUUNUVDSZUYJUVFUYKTUCUVHUUMUCUAVOUVEUYKUVAUUMU
+      UNUVDYGXQUXFUVIUXGUXNUUTUXDUVIWIXOUYJUUHUVGUUMUXFUXGUXNYCUYJUUMAUXKHVAZUV
+      GUYJUWCUUMUYLVTPUUIUUMUYCUVTUUMUWBUYLUYCYDUYCAUWAUXKHUYDXFYEUUTUWDUXEUXGU
+      XNUXCYFUXHUXIUXNUXHUUHUUIUUMUUTUUJUXEUXGUWPXOUYFWNYHWKUYJAUXKUVCHUYJUXKUX
+      LUVCUXHUXNXRUXHUYGUXNUYHYHYIZXFXGXHWKUYJUXOUVDUUMUUNUYJAUXKUVCJUYMXFYJYBY
+      KUXNUXPYLVRUXSUXTRUYAUXMUXQYMYNWSYOABCDEFGHUUMUUNIJKLMNYPYQYRYSYKYTOUBUAU
+      UIKUUAUUB $.
+
     $( The relation constructed in ~ weiunpo , ~ weiunso , ~ weiunfr , and
        ~ weiunwe is set-like if all members of the indexed union are sets.
        (Contributed by Matthew House, 23-Aug-2025.) $)
     weiunse $p |- ( ( R We A /\ R Se A /\ A. x e. A B e. V ) ->
         T Se U_ x e. A B ) $=
-      ( vs wcel wral cv cvv vq vp vr vt wwe wse w3a wbr ciun wa cfv csn cun csb
-      crab simpl2 wf wn wi simpl1 weiunlem2 syl2anc simp1d simpr ffvelcdmd seex
-      snex unexg sylancl wss ssrab2 a1i snssd unssd simpl3 elex syl nfv nfcsb1v
-      ralimi nfel1 weq csbeq1a eleq1d cbvralw sylib ssralv sylc iunexg 3ad2ant1
-      wceq simp2 breq1 elrab elun1 sylbir sylan fvex elsn elun2 ad2antrl fveq2d
-      wo simpl breq12d eqeq12d csbeq1d breq123d anbi12d orbi12d brab2a 3ad2ant3
-      simprbi mpjaodan fveq2 eleq12d simp2d rspcdva csbeq1 eliuni rabssdv ssexd
-      id ralrimiva df-se sylibr ) GIUEZGIUFZHMQZAGRZUGZUASZUBSZKUHZUAAGHUIZUOZT
-      QZUBYORYOKUFYKYQUBYOYKYMYOQZUJZYPPUCSZYMLUKZIUHZUCGUOZUUAULZUMZAPSZHUNZUI
-      ZTYSUUETQZUUGTQZPUUERZUUHTQYSUUCTQZUUDTQUUIYSYHUUAGQUULYGYHYJYRUPZYSYOGYM
-      LYSYOGLUQZUDSZAUUOLUKZHUNZQZUDYORZUUOUUGQUUFUUPIUHURUSPGRUDYORZYSYGYHUUNU
-      USUUTUGYGYHYJYRUTUUMADEFUDGHILPNVAVBZVCZYKYRVDVEZUCGUUAIVFVBUUAVGUUCUUDTT
-      VHVIYSUUEGVJUUJPGRZUUKYSUUCUUDGUUCGVJYSUUBUCGVKVLYSUUAGUVCVMVNYSHTQZAGRZU
-      VDYSYJUVFYGYHYJYRVOYIUVEAGHMVPVTVQUVEUUJAPGUVEPVRAUUGTAUUFHVSWAAPWBHUUGTA
-      UUFHWCWDWEWFUUJPUUEGWGWHPUUEUUGTTWIVBYSYNUAYOUUHYSYLYOQZYNUGZYLLUKZUUEQZY
-      LAUVIHUNZQZYLUUHQUVHUVIUUAIUHZUVJUVIUUAWKZYLYMAUVIJUNZUHZUJZUVHUVIGQZUVMU
-      VJUVHYOGYLLYSUVGUUNYNUVBWJYSUVGYNWLZVEUVRUVMUJUVIUUCQUVJUUBUVMUCUVIGYTUVI
-      UUAIWMWNUVIUUCUUDWOWPWQUVNUVJUVHUVPUVNUVIUUDQUVJUVIUUAYLLWRWSUVIUUDUUCWTW
-      PXAYNYSUVMUVQXCZUVGYNUVGYRUJUVTBSZLUKZCSZLUKZIUHZUWBUWDWKZUWAUWCAUWBJUNZU
-      HZUJZXCUVTBCYLYMYOYOKBUAWBZCUBWBZUJZUWEUVMUWIUVQUWLUWBUVIUWDUUAIUWLUWAYLL
-      UWJUWKXDZXBZUWLUWCYMLUWJUWKVDZXBZXEUWLUWFUVNUWHUVPUWLUWBUVIUWDUUAUWNUWPXF
-      UWLUWAYLUWCYMUWGUVOUWMUWLAUWBUVIJUWNXGUWOXHXIXJOXKXMXLXNUVHUURUVLUDYOYLUU
-      OYLWKZUUOYLUUQUVKUWQYCUWQAUUPUVIHUUOYLLXOXGXPYSUVGUUSYNYSUUNUUSUUTUVAXQWJ
-      UVSXRPUVIUUGUVKUUEYLAUUFUVIHXSXTVBYAYBYDUBUAYOKYEYF $.
-  $}
-
-  ${
-    $d A x y z $.  $d A u v w x $.  $d B y z $.  $d B u v w $.  $d F y z $.
-    $d R y z $.  $d R u v w $.  $d S y z $.
-    weiunwe.1 $e |- F = ( w e. U_ x e. A B |-> ( iota_ u e.
-        { x e. A | w e. B } A. v e. { x e. A | w e. B } -. v R u ) ) $.
-    weiunwe.2 $e |- T = { <. y , z >. | ( ( y e. U_ x e. A B /\
-        z e. U_ x e. A B ) /\ ( ( F ` y ) R ( F ` z ) \/
-        ( ( F ` y ) = ( F ` z ) /\ y [_ ( F ` y ) / x ]_ S z ) ) ) } $.
+      ( vs vt wcel wral cvv vq vp vr wwe wse w3a cv wbr ciun wa cfv csn cun csb
+      crab simpl2 wf simpl1 weiunlem2 simp1d simpr ffvelcdmd seex syl2anc unexg
+      wn snex sylancl wss ssrab2 a1i snssd unssd simpl3 elex ralimi syl nfcsb1v
+      nfv nfel1 weq csbeq1a eleq1d sylib ssralv sylc iunexg wceq 3ad2ant1 simp2
+      cbvralw breq1 elrab elun1 sylbir sylan fvex elsn elun2 ad2antrl weiunlem1
+      wo simprbi 3ad2ant3 mpjaodan csbeq1d eleq12d simp2d rspcdva csbeq1 eliuni
+      id fveq2 rabssdv ssexd ralrimiva df-se sylibr ) GIUDZGIUEZHMRZAGSZUFZUAUG
+      ZUBUGZKUHZUAAGHUIZUOZTRZUBYGSYGKUEYCYIUBYGYCYEYGRZUJZYHPUCUGZYELUKZIUHZUC
+      GUOZYMULZUMZAPUGZHUNZUIZTYKYQTRZYSTRZPYQSZYTTRYKYOTRZYPTRUUAYKXTYMGRUUDXS
+      XTYBYJUPZYKYGGYELYKYGGLUQZQUGZAUUGLUKZHUNZRZQYGSZYRUUHIUHVFQYSSPGSZYKABCD
+      EFQGHIJKLPNOXSXTYBYJURUUEUSZUTZYCYJVAVBZUCGYMIVCVDYMVGYOYPTTVEVHYKYQGVIUU
+      BPGSZUUCYKYOYPGYOGVIYKYNUCGVJVKYKYMGUUOVLVMYKHTRZAGSZUUPYKYBUURXSXTYBYJVN
+      YAUUQAGHMVOVPVQUUQUUBAPGUUQPVSAYSTAYRHVRVTAPWAHYSTAYRHWBWCWKWDUUBPYQGWEWF
+      PYQYSTTWGVDYKYFUAYGYTYKYDYGRZYFUFZYDLUKZYQRZYDAUVAHUNZRZYDYTRUUTUVAYMIUHZ
+      UVBUVAYMWHZYDYEAUVAJUNUHZUJZUUTUVAGRZUVEUVBUUTYGGYDLYKUUSUUFYFUUNWIYKUUSY
+      FWJZVBUVIUVEUJUVAYORUVBYNUVEUCUVAGYLUVAYMIWLWMUVAYOYPWNWOWPUVFUVBUUTUVGUV
+      FUVAYPRUVBUVAYMYDLWQWRUVAYPYOWSWOWTYFYKUVEUVHXBZUUSYFUUSYJUJUVKABCDEFGHYD
+      YEIJKLNOXAXCXDXEUUTUUJUVDQYGYDQUAWAZUUGYDUUIUVCUVLXLUVLAUUHUVAHUUGYDLXMXF
+      XGYKUUSUUKYFYKUUFUUKUULUUMXHWIUVJXIPUVAYSUVCYQYDAYRUVAHXJXKVDXNXOXPUBUAYG
+      KXQXR $.
+
     $( A well-ordering on an indexed union can be constructed from a
-       well-ordering on its index set and a collection of well-orderings on its
-       members.  (Contributed by Matthew House, 23-Aug-2025.) $)
+       well-ordering on its index class and a collection of well-orderings on
+       its members.  (Contributed by Matthew House, 23-Aug-2025.) $)
     weiunwe $p |- ( ( R We A /\ R Se A /\ A. x e. A S We B ) ->
         T We U_ x e. A B ) $=
       ( wwe wral wfr wor ralimi syl3an3 wse w3a ciun wefr weiunfr weiunso df-we