Add MndToCat and other related theorems

discouraged

@@ -4824,6 +4824,7 @@
 "df-mndo" is used by "ismndo".
 "df-mndo" is used by "mndoisexid".
 "df-mndo" is used by "mndoissmgrpOLD".
+"df-mndtc" is used by "mndtcval".
 "df-mnf" is used by "mnfnre".
 "df-mnf" is used by "mnfxr".
 "df-mnf" is used by "pnfnemnf".
@@ -9699,6 +9700,13 @@
 "mndomgmid" is used by "isdrngo2".
 "mndomgmid" is used by "ismndo2".
 "mndomgmid" is used by "rngoidmlem".
+"mndtcbasval" is used by "mndtcbas".
+"mndtcbasval" is used by "mndtcob".
+"mndtcob" is used by "mndtcco".
+"mndtcob" is used by "mndtchom".
+"mndtcval" is used by "mndtcbasval".
+"mndtcval" is used by "mndtcco".
+"mndtcval" is used by "mndtchom".
 "moexex" is used by "2moswap".
 "moexex" is used by "moexexv".
 "mpv" is used by "mulcompr".
@@ -15448,6 +15456,7 @@ New usage of "df-md" is discouraged (1 uses).
 New usage of "df-mgmOLD" is discouraged (1 uses).
 New usage of "df-mi" is discouraged (2 uses).
 New usage of "df-mndo" is discouraged (3 uses).
+New usage of "df-mndtc" is discouraged (1 uses).
 New usage of "df-mnf" is discouraged (3 uses).
 New usage of "df-mp" is discouraged (11 uses).
 New usage of "df-mpq" is discouraged (3 uses).
@@ -17245,6 +17254,9 @@ New usage of "mndoisexid" is discouraged (2 uses).
 New usage of "mndoismgmOLD" is discouraged (3 uses).
 New usage of "mndoissmgrpOLD" is discouraged (1 uses).
 New usage of "mndomgmid" is discouraged (3 uses).
+New usage of "mndtcbasval" is discouraged (2 uses).
+New usage of "mndtcob" is discouraged (2 uses).
+New usage of "mndtcval" is discouraged (3 uses).
 New usage of "mo4OLD" is discouraged (0 uses).
 New usage of "mobidvALT" is discouraged (0 uses).
 New usage of "mobiiOLD" is discouraged (0 uses).

set.mm

@@ -444031,6 +444031,9 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the
 htmldef "ProsetToCat" as "ProsetToCat";
   althtmldef "ProsetToCat" as "ProsetToCat";
   latexdef "ProsetToCat" as "\mathrm{ProsetToCat}";
+htmldef "MndToCat" as "MndToCat";
+  althtmldef "MndToCat" as "MndToCat";
+  latexdef "MndToCat" as "\mathrm{MndToCat}";
 /* End of Zhi Wang's mathbox */
 
 /* Mathbox of Emmett Weisz */
@@ -775773,6 +775776,36 @@ coordinates of the intersection points of a (nondegenerate) line and a
   $}
 
 
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Predicate calculus with equality
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+  Axiom scheme ax-5 (Distinctness)
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+$)
+
+  ${
+    $d x y $.
+    dtrucor3.1 $e |- -. A. x x = y $.
+    dtrucor3.2 $e |- ( x = y -> A. x x = y ) $.
+    $( An example of how ~ ax-5 without a distinct variable condition causes
+       paradox in models of at least two objects.  The hypothesis "dtrucor3.1"
+       is provable from ~ dtru in the ZF set theory. ~ axc16nf and ~ euae
+       demonstrate that the violation of ~ dtru leads to a model with only one
+       object assuming its existence ( ~ ax-6 ).  The conclusion is also
+       provable in the empty model ( see ~ emptyal ).  See also ~ nf5 and
+       ~ nf5i for the relation between unconditional ~ ax-5 and being not free.
+       (Contributed by Zhi Wang, 23-Sep-2024.) $)
+    dtrucor3 $p |- A. x x = y $=
+      ( weq wex wal ax6ev mto nex pm2.24ii ) ABEZAFLAGZABHLALMCDIJK $.
+  $}
+
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   ZF Set Theory - start with the Axiom of Extensionality
@@ -777277,6 +777310,48 @@ separated by (open) neighborhoods.  See ~ sepnsepo for the equivalence
   $}
 
 
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Monomorphisms and epimorphisms
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+  ${
+    $d .1. g h z $.  $d B g h z $.  $d C g h z $.  $d H g h z $.  $d X g h z $.
+    $d g h ph z $.
+    idmon.b $e |- B = ( Base ` C ) $.
+    idmon.h $e |- H = ( Hom ` C ) $.
+    idmon.i $e |- .1. = ( Id ` C ) $.
+    idmon.c $e |- ( ph -> C e. Cat ) $.
+    idmon.x $e |- ( ph -> X e. B ) $.
+    ${
+      idmon.m $e |- M = ( Mono ` C ) $.
+      $( An identity arrow, or an identity morphism, is a monomorphism.
+         (Contributed by Zhi Wang, 21-Sep-2024.) $)
+      idmon $p |- ( ph -> ( .1. ` X ) e. ( X M X ) ) $=
+        ( vg vz vh co wcel cv wral cfv cop cco wceq wi catidcl wa adantr simpr1
+        w3a ccat eqid simpr2 catlid simpr3 eqeq12d biimpd ralrimivvva mpbir2and
+        ismon2 ) AGDUAZGGFQRVAGGEQRVANSZOSZGUBGCUCUAZQZQZVAPSZVEQZUDZVBVGUDZUEZ
+        PVCGEQZTNVLTOBTABCDEGHIJKLUFAVKONPBVLVLAVCBRZVBVLRZVGVLRZUJZUGZVIVJVQVF
+        VBVHVGVQBCVDDVBEVCGHIJACUKRVPKUHZAVMVNVOUIZVDULZAGBRVPLUHZAVMVNVOUMUNVQ
+        BCVDDVGEVCGHIJVRVSVTWAAVMVNVOUOUNUPUQURAOBCVDNPVAEFGGHIVTMKLLUTUS $.
+    $}
+
+    ${
+      idepi.e $e |- E = ( Epi ` C ) $.
+      $( An identity arrow, or an identity morphism, is an epimorphism.
+         (Contributed by Zhi Wang, 21-Sep-2024.) $)
+      idepi $p |- ( ph -> ( .1. ` X ) e. ( X E X ) ) $=
+        ( vg vz vh co wcel cv wral cfv cop cco wceq wi catidcl w3a wa ccat eqid
+        adantr simpr1 simpr2 catrid simpr3 eqeq12d biimpd ralrimivvva mpbir2and
+        isepi2 ) AGDUAZGGEQRVAGGFQRNSZVAGGUBOSZCUCUAZQZQZPSZVAVEQZUDZVBVGUDZUEZ
+        PGVCFQZTNVLTOBTABCDFGHIJKLUFAVKONPBVLVLAVCBRZVBVLRZVGVLRZUGZUHZVIVJVQVF
+        VBVHVGVQBCVDDVBFGVCHIJACUIRVPKUKZAGBRVPLUKZVDUJZAVMVNVOULZAVMVNVOUMUNVQ
+        BCVDDVGFGVCHIJVRVSVTWAAVMVNVOUOUNUPUQURAOBCVDNPEVAFGGHIVTMKLLUTUS $.
+    $}
+  $}
+
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Examples of categories
@@ -777824,6 +777899,211 @@ mean the category of preordered sets (classes).  However, "ProsetToCat"
     $}
   $}
 
+
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+  Monoids as categories
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+$)
+
+  $c MndToCat $.
+
+  $( Class function defining monoids as categories. $)
+  cmndtc $a class MndToCat $.
+
+  ${
+    $d B x $.  $d M m x $.  $d m ph $.
+    $( Definition of the function converting a monoid to a category.  Example
+       3.3(4.e) of [Adamek] p. 24.
+
+       The definition of the base set is arbitrary.  The whole extensible
+       structure becomes the object here (see ~ mndtcbasval ) , instead of just
+       the base set, as is the case in Example 3.3(4.e) of [Adamek] p. 24.
+
+       The resulting category is defined entirely, up to isomorphism, by
+       ~ mndtcbas , ~ mndtchom , ~ mndtcco .  Use those instead.
+
+       See example 3.26(3) of [Adamek] p. 33 for more on isomorphism.
+
+       "MndToCat" was taken instead of "MndCat" because the latter might mean
+       the category of monoids.  (Contributed by Zhi Wang, 22-Sep-2024.)
+       (New usage is discouraged.) $)
+    df-mndtc $a |- MndToCat = ( m e. Mnd |-> { <. ( Base ` ndx ) , { m } >. ,
+          <. ( Hom ` ndx ) , { <. m , m , ( Base ` m ) >. } >. ,
+          <. ( comp ` ndx ) , { <. <. m , m , m >. , ( +g ` m ) >. } >. } ) $.
+
+    mndtcbas.c $e |- ( ph -> C = ( MndToCat ` M ) ) $.
+    mndtcbas.m $e |- ( ph -> M e. Mnd ) $.
+    $( Value of the category.  (Contributed by Zhi Wang, 22-Sep-2024.)
+       (New usage is discouraged.) $)
+    mndtcval $p |- ( ph -> C = { <. ( Base ` ndx ) , { M } >. ,
+          <. ( Hom ` ndx ) , { <. M , M , ( Base ` M ) >. } >. ,
+          <. ( comp ` ndx ) , { <. <. M , M , M >. , ( +g ` M ) >. } >. } ) $=
+      ( vm cmndtc cfv cnx cbs csn cop cotp cplusg ctp cmnd wceq opeq2d oteq123d
+      fveq2 chom cco wcel cv sneq id sneqd opeq12d tpeq123d df-mndtc tpex fvmpt
+      syl eqtrd ) ABCGHZIJHZCKZLZIUAHZCCCJHZMZKZLZIUBHZCCCMZCNHZLZKZLZOZDACPUCU
+      OVJQEFCUPFUDZKZLZUSVKVKVKJHZMZKZLZVDVKVKVKMZVKNHZLZKZLZOVJPGVKCQZVMURVQVC
+      WBVIWCVLUQUPVKCUERWCVPVBUSWCVOVAWCVKCVKCVNUTWCUFZWDVKCJTSUGRWCWAVHVDWCVTV
+      GWCVRVEVSVFWCVKCVKCVKCWDWDWDSVKCNTUHUGRUIFUJURVCVIUKULUMUN $.
+
+    mndtcbas.b $e |- ( ph -> B = ( Base ` C ) ) $.
+    $( The base set of the category.  (Contributed by Zhi Wang, 22-Sep-2024.)
+       (New usage is discouraged.) $)
+    mndtcbasval $p |- ( ph -> B = { M } ) $=
+      ( cbs cfv cnx csn cop chom cotp cco cplusg ctp mndtcval cvv c1 fveq2d cdc
+      wcel wceq snex c5 catstr baseid snsstp1 strfv mp1i 3eqtr4d ) ACHIJHIDKZLZ
+      JMIDDDHINKZLZJOIDDDNDPILKZLZQZHIZBUMACUSHACDEFRUAGUMSUCUMUTUDADUEUMUSHSTT
+      UFUBLUQUMUOUGUHUNUPURUIUJUKUL $.
+
+    $( The category contains precisely one object.  (Contributed by Zhi Wang,
+       22-Sep-2024.) $)
+    mndtcbas $p |- ( ph -> E! x x e. B ) $=
+      ( cv csn wceq wex wcel weu cmnd mndtcbasval sneq eqeq2d spcedv eusn
+      sylibr ) ACBIZJZKZBLUBCMBNAUDCEJZKBOEGACDEFGHPUBEKUCUECUBEQRSBCTUA $.
+
+    mndtchom.x $e |- ( ph -> X e. B ) $.
+    $( Lemma for ~ mndtchom and ~ mndtcco .  (Contributed by Zhi Wang,
+       22-Sep-2024.)  (New usage is discouraged.) $)
+    mndtcob $p |- ( ph -> X = M ) $=
+      ( csn wcel wceq mndtcbasval eleqtrd wb elsng syl mpbid ) AEDJZKZEDLZAEBSI
+      ABCDFGHMNAEBKTUAOIEDBPQR $.
+
+    mndtchom.y $e |- ( ph -> Y e. B ) $.
+    ${
+      mndtchom.h $e |- ( ph -> H = ( Hom ` C ) ) $.
+      $( The only hom-set of the category is the base set of the monoid.
+         (Contributed by Zhi Wang, 22-Sep-2024.) $)
+      mndtchom $p |- ( ph -> ( X H Y ) = ( Base ` M ) ) $=
+        ( co cbs cfv csn chom cnx cop cotp cco cplusg ctp c1 c5 mndtcval catstr
+        cvv cdc homid snsstp2 wcel snex a1i strfv3 eqtrd mndtcob oveq123d df-ot
+        eqid sneqi oveqi df-ov opex fvex fvsn 3eqtri eqtrdi ) AFGDNEEEEEOPZUAZQ
+        ZNZVJAFEGEDVLADCRPZVLMAVNVLSOPEQZTZSRPVLTZSUBPEEEUAEUCPTQZTZUDCRUIUEUEU
+        FUJTACEHIUGVRVOVLUHUKVPVQVSULVLUIUMAVKUNUOVNVAUPUQABCEFHIJKURABCEGHIJLU
+        RUSVMEEEETZVJTZQZNVTWBPVJVLWBEEVKWAEEVJUTVBVCEEWBVDVTVJEEVEEOVFVGVHVI
+        $.
+    $}
+
+    mndtcco.z $e |- ( ph -> Z e. B ) $.
+    mndtcco.o $e |- ( ph -> .x. = ( comp ` C ) ) $.
+    $( The composition is the monoid operation.  (Contributed by Zhi Wang,
+       22-Sep-2024.) $)
+    mndtcco $p |- ( ph -> ( <. X , Y >. .x. Z ) = ( +g ` M ) ) $=
+      ( cop cfv csn cco cnx co cotp cplusg cbs chom ctp cvv cdc mndtcval catstr
+      c1 ccoid snsstp3 wcel snex a1i eqid strfv3 eqtrd mndtcob opeq12d oveq123d
+      c5 df-ov df-ot fveq2i otex fvex fvsn 3eqtr2i eqtrdi ) AFGPZHDUAEEPZEEEEUB
+      ZEUCQZPZRZUAZVOAVLVMHEDVQADCSQZVQOAVSVQTUDQERZPZTUEQEEEUDQUBRZPZTSQVQPZUF
+      CSUGUKUKVCUHPACEIJUIVQVTWBUJULWAWCWDUMVQUGUNAVPUOUPVSUQURUSAFEGEABCEFIJKL
+      UTABCEGIJKMUTVAABCEHIJKNUTVBVRVMEPZVQQVNVQQVOVMEVQVDVNWEVQEEEVEVFVNVOEEEV
+      GEUCVHVIVJVK $.
+
+    mndtcco2.o2 $e |- ( ph -> .xb = ( <. X , Y >. .x. Z ) ) $.
+    $( The composition is the monoid operation.  (Contributed by Zhi Wang,
+       22-Sep-2024.) $)
+    mndtcco2 $p |- ( ph -> ( G .xb F ) = ( G ( +g ` M ) F ) ) $=
+      ( cplusg cfv cop co mndtcco eqtrd oveqd ) ADHTUAZGFADIJUBKEUCUGSABCEHIJKL
+      MNOPQRUDUEUF $.
+  $}
+
+  ${
+    $d C f g k w x y z $.  $d M f g k w x z $.  $d X f g k w x y z $.
+    $d f g k ph w x y z $.
+    mndtccat.c $e |- ( ph -> C = ( MndToCat ` M ) ) $.
+    mndtccat.m $e |- ( ph -> M e. Mnd ) $.
+    $( Lemma for ~ mndtccat and ~ mndtcid .  (Contributed by Zhi Wang,
+       22-Sep-2024.) $)
+    mndtccatid $p |- ( ph -> ( C e. Cat /\ ( Id ` C ) =
+                ( y e. ( Base ` C ) |-> ( 0g ` M ) ) ) ) $=
+      ( cv cfv wcel wa co eqidd eqid adantr wceq mndtchom mndtcco oveqd eleqtrd
+      cop vx vz vw vf vg vk cbs chom w3a cco c0g cmndtc fvexd eqeltrd biid cmnd
+      cvv mndidcl syl simpr cplusg simpr1l simpr1r simpr31 mndlid syl2anc eqtrd
+      eleqtrrd simpr2l simpr32 mndrid syl3anc 3eltr4d simpr33 syl13anc oveq123d
+      mndcl simpr2r mndass 3eqtr4d iscatd2 ) AUAGZCUGHZIZBGZWCIZJZUBGZWCIZUCGZW
+      CIZJZUDGZWBWECUHHZKZIZUEGZWEWHWNKZIZUFGZWHWJWNKZIZUIZUIZUABUBUCWCCCUJHZDU
+      KHZUDUEUFWNUQAWCLAWNLAXELACDULHZUQEADULUMUNXDUOAWFJZXFDUGHZWEWEWNKAXFXIIZ
+      WFADUPIZXJFXIDXFXIMZXFMZURUSNXHWCCWNDWEWEACXGOZWFENAXKWFFNXHWCLAWFUTZXOXH
+      WNLPVHAXDJZXFWMWBWETZWEXEKZKXFWMDVAHZKZWMXPXRXSXFWMXPWCCXEDWBWEWEAXNXDENZ
+      AXKXDFNZXPWCLZWDWFWLXCAVBZWDWFWLXCAVCZYEXPXELZQRXPXKWMXIIZXTWMOYBXPWMWOXI
+      WPWSXBWGWLAVDXPWCCWNDWBWEYAYBYCYDYEXPWNLZPSZXIXSDWMXFXLXSMZXMVEVFVGXPWQXF
+      WEWETWHXEKZKWQXFXSKZWQXPYKXSWQXFXPWCCXEDWEWEWHYAYBYCYEYEWIWKWGXCAVIZYFQRX
+      PXKWQXIIZYLWQOYBXPWQWRXIWPWSXBWGWLAVJXPWCCWNDWEWHYAYBYCYEYMYHPSZXIXSDWQXF
+      XLYJXMVKVFVGXPWQWMXSKZXIWQWMXQWHXEKZKZWBWHWNKXPXKYNYGYPXIIYBYOYIXIXSDWQWM
+      XLYJVQVLXPYQXSWQWMXPWCCXEDWBWEWHYAYBYCYDYEYMYFQRZXPWCCWNDWBWHYAYBYCYDYMYH
+      PVMXPWTWQXSKZWMXSKZWTYPXSKZWTWQWEWHTWJXEKZKZWMXQWJXEKZKWTYRWBWHTWJXEKZKXP
+      XKWTXIIYNYGUUAUUBOYBXPWTXAXIWPWSXBWGWLAVNXPWCCWNDWHWJYAYBYCYMWIWKWGXCAVRZ
+      YHPSYOYIXIXSDWTWQWMXLYJVSVOXPUUDYTWMWMUUEXSXPWCCXEDWBWEWJYAYBYCYDYEUUGYFQ
+      XPUUCXSWTWQXPWCCXEDWEWHWJYAYBYCYEYMUUGYFQRXPWMLVPXPWTWTYRYPUUFXSXPWCCXEDW
+      BWHWJYAYBYCYDYMUUGYFQXPWTLYSVPVTWA $.
+
+    $( The function value is a category.  (Contributed by Zhi Wang,
+       22-Sep-2024.) $)
+    mndtccat $p |- ( ph -> C e. Cat ) $=
+      ( vy ccat wcel ccid cfv cbs c0g cmpt wceq mndtccatid simpld ) ABGHBIJFBKJ
+      CLJMNAFBCDEOP $.
+
+    mndtcid.b $e |- ( ph -> B = ( Base ` C ) ) $.
+    mndtcid.x $e |- ( ph -> X e. B ) $.
+    mndtcid.i $e |- ( ph -> .1. = ( Id ` C ) ) $.
+    $( The identity morphism, or identity arrow, is the identity element of the
+       monoid.  (Contributed by Zhi Wang, 22-Sep-2024.) $)
+    mndtcid $p |- ( ph -> ( .1. ` X ) = ( 0g ` M ) ) $=
+      ( vx c0g cfv cbs cvv ccid cmpt ccat wceq mndtccatid simprd eqtrd cv eqidd
+      wcel wa eleqtrd fvexd fvmptd ) ALFEMNZUKCONZDPADCQNZLULUKRZKACSUFUMUNTALC
+      EGHUAUBUCALUDFTUGUKUEAFBULJIUHAEMUIUJ $.
+  $}
+
+  ${
+    $d B f g h z $.  $d C f g h z $.  $d E f g h z $.  $d G f g h z $.
+    $d H f g h z $.  $d M f g h z $.  $d X f g h z $.  $d Y f g h z $.
+    $d f g h ph z $.
+    grptcmon.c $e |- ( ph -> C = ( MndToCat ` G ) ) $.
+    grptcmon.g $e |- ( ph -> G e. Grp ) $.
+    grptcmon.b $e |- ( ph -> B = ( Base ` C ) ) $.
+    grptcmon.x $e |- ( ph -> X e. B ) $.
+    grptcmon.y $e |- ( ph -> Y e. B ) $.
+    grptcmon.h $e |- ( ph -> H = ( Hom ` C ) ) $.
+    ${
+      grptcmon.m $e |- ( ph -> M = ( Mono ` C ) ) $.
+      $( All morphisms in a category converted from a group are monomorphisms.
+         (Contributed by Zhi Wang, 23-Sep-2024.) $)
+      grptcmon $p |- ( ph -> ( X M Y ) = ( X H Y ) ) $=
+        ( cfv co wcel eqid ad2antrr vf vg vz vh cmon chom cop cco wceq wral cbs
+        cv wi grpmndd mndtccat eleqtrd ismon2 simprbda ex wa cplusg cmndtc cmnd
+        w3a simpr1 eleqtrrd eqidd mndtcco2 eqeq12d cgrp wb simpr2 simpr3 simplr
+        mndtchom grplcan syl13anc bitrd biimpd ralrimivvva ancld sylibrd impbid
+        eqrdv oveqd 3eqtr4d ) AGHCUEPZQZGHCUFPZQZGHFQGHEQAUAWHWJAUAULZWHRZWKWJR
+        ZAWLWMAWLWMWKUBULZUCULZGUGHCUHPZQZQZWKUDULZWQQZUIZWNWSUIZUMZUDWOGWIQZUJ
+        UBXDUJUCCUKPZUJZAUCXECWPUBUDWKWIWGGHXESWISWPSWGSACDIADJUNZUOAGBXELKUPAH
+        BXEMKUPUQZURUSAWMWMXFUTWLAWMXFAWMXFAWMUTZXCUCUBUDXEXDXDXIWOXERZWNXDRZWS
+        XDRZVDZUTZXAXBXNXAWKWNDVAPZQZWKWSXOQZUIZXBXNWRXPWTXQXNBCWQWPWNWKDWOGHAC
+        DVBPUIWMXMITZADVCRWMXMXGTZABXEUIWMXMKTZXNWOXEBXIXJXKXLVEYAVFZAGBRWMXMLT
+        ZAHBRWMXMMTZXNWPVGZXNWQVGZVHXNBCWQWPWSWKDWOGHXSXTYAYBYCYDYEYFVHVIXNDVJR
+        ZWNDUKPZRWSYHRWKYHRXRXBVKAYGWMXMJTXNWNXDYHXIXJXKXLVLXNBCWIDWOGXSXTYAYBY
+        CXNWIVGZVOZUPXNWSXDYHXIXJXKXLVMYJUPXNWKWJYHAWMXMVNXNBCWIDGHXSXTYAYCYDYI
+        VOUPYHXODWNWSWKYHSXOSVPVQVRVSVTUSWAXHWBWCWDAFWGGHOWEAEWIGHNWEWF $.
+    $}
+
+    ${
+      grptcepi.e $e |- ( ph -> E = ( Epi ` C ) ) $.
+      $( All morphisms in a category converted from a group are epimorphisms.
+         (Contributed by Zhi Wang, 23-Sep-2024.) $)
+      grptcepi $p |- ( ph -> ( X E Y ) = ( X H Y ) ) $=
+        ( cfv co wcel eqid ad2antrr vf vg vz vh cepi chom cop cco wceq wral cbs
+        cv wi grpmndd mndtccat eleqtrd isepi2 simprbda ex wa cplusg cmndtc cmnd
+        w3a simpr1 eleqtrrd eqidd mndtcco2 eqeq12d cgrp wb simpr2 simpr3 simplr
+        mndtchom grprcan syl13anc bitrd biimpd ralrimivvva ancld sylibrd impbid
+        eqrdv oveqd 3eqtr4d ) AGHCUEPZQZGHCUFPZQZGHDQGHFQAUAWHWJAUAULZWHRZWKWJR
+        ZAWLWMAWLWMUBULZWKGHUGUCULZCUHPZQZQZUDULZWKWQQZUIZWNWSUIZUMZUDHWOWIQZUJ
+        UBXDUJUCCUKPZUJZAUCXECWPUBUDWGWKWIGHXESWISWPSWGSACEIAEJUNZUOAGBXELKUPAH
+        BXEMKUPUQZURUSAWMWMXFUTWLAWMXFAWMXFAWMUTZXCUCUBUDXEXDXDXIWOXERZWNXDRZWS
+        XDRZVDZUTZXAXBXNXAWNWKEVAPZQZWSWKXOQZUIZXBXNWRXPWTXQXNBCWQWPWKWNEGHWOAC
+        EVBPUIWMXMITZAEVCRWMXMXGTZABXEUIWMXMKTZAGBRWMXMLTZAHBRWMXMMTZXNWOXEBXIX
+        JXKXLVEYAVFZXNWPVGZXNWQVGZVHXNBCWQWPWKWSEGHWOXSXTYAYBYCYDYEYFVHVIXNEVJR
+        ZWNEUKPZRWSYHRWKYHRXRXBVKAYGWMXMJTXNWNXDYHXIXJXKXLVLXNBCWIEHWOXSXTYAYCY
+        DXNWIVGZVOZUPXNWSXDYHXIXJXKXLVMYJUPXNWKWJYHAWMXMVNXNBCWIEGHXSXTYAYBYCYI
+        VOUPYHXOEWNWSWKYHSXOSVPVQVRVSVTUSWAXHWBWCWDADWGGHOWEAFWIGHNWEWF $.
+    $}
+  $}
+
 $( (End of Zhi Wang's mathbox.) $)
 $( End $[ set-mbox-zw.mm $] $)