Add MndToCat and other related theorems (#4242)

* Move moel to main; add ThinCat and indiscrete category

* add thincc

* Add catcone0 to main; add catprs, prsthinc and related theorems

* remove ax-un dependency in f1omo

* remove ax-un for 2oexw and prsthinc

* remove ax-un and ax-pow for indthinc

* shorten 2oexw

* add mo0sn

* add mofasn2 and related

* add mofsn3 and rename theorems xxfa* -> xxf*

* add setcthin and setc2othin

* shorten proof by mof02

* rename mofsn3 -> mofmo; and fix description

* Add ProsetToCat defining and important properties

* added two redundant hypotheses to prstchom for explicitness

* add prstchom2ALT

* add thincn0eu and prstchom2

* revive ALT theorems

* prevent basendx usage

* shorten prstchomval

* sylibda->sylbida

* Add idmon and idepi

* add MndToCat

* add grptcmon and grptcepi

* add dtrucor3

* fix description based on PR comments

* mndtcco2: .xb -> .o. ; add monepilem to factor out common proof steps

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".
@@ -15447,6 +15455,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).
@@ -17247,6 +17256,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 "moexex" is discouraged (2 uses).

set.mm

@@ -444302,6 +444302,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 */
@@ -776046,6 +776049,46 @@ coordinates of the intersection points of a (nondegenerate) line and a
       ( wa wi impexp 3bitr3g ) ABCIDJEFIGJBCDJJEFGJJHBCDKEFGKL $.
   $}
 
+  ${
+    monepilem.1 $e |- ( ph -> ( ps <-> ( ch /\ th ) ) ) $.
+    monepilem.2 $e |- ( ( ph /\ ch ) -> th ) $.
+    $( Common lemmas for proving monomorphisms, epimorphisms, and potentially
+       others.  (Contributed by Zhi Wang, 24-Sep-2024.) $)
+    monepilem $p |- ( ph -> ( ps <-> ch ) ) $=
+      ( simprbda ex wa ancld sylibrd impbid ) ABCABCABCDEGHACCDIBACDACDFHJEKL
+      $.
+  $}
+
+
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  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 $.
+  $}
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -777551,6 +777594,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
@@ -778098,6 +778183,210 @@ 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 built from a monoid.  (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 built from a monoid.  (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 built from a monoid 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 built from a monoid 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 of the category built from a monoid 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 -> .o. = ( <. X , Y >. .x. Z ) ) $.
+    $( The composition of the category built from a monoid is the monoid
+       operation.  (Contributed by Zhi Wang, 22-Sep-2024.) $)
+    mndtcco2 $p |- ( ph -> ( G .o. F ) = ( G ( +g ` M ) F ) ) $=
+      ( cplusg cfv cop co mndtcco eqtrd oveqd ) AJGTUAZFEAJHIUBKDUCUGSABCDGHIKL
+      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, of the category built from a
+       monoid 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 w3a cplusg cmndtc simpr1 eleqtrrd
+        wa cmnd eqidd mndtcco2 eqeq12d wb simpr2 mndtchom simpr3 simplr grplcan
+        cgrp syl13anc bitrd biimpd ralrimivvva monepilem eqrdv oveqd 3eqtr4d )
+        AGHCUEPZQZGHCUFPZQZGHFQGHEQAUAWDWFAUAULZWDRWGWFRZWGUBULZUCULZGUGHCUHPZQ
+        ZQZWGUDULZWLQZUIZWIWNUIZUMZUDWJGWEQZUJUBWSUJUCCUKPZUJAUCWTCWKUBUDWGWEWC
+        GHWTSWESWKSWCSACDIADJUNZUOAGBWTLKUPAHBWTMKUPUQAWHVCZWRUCUBUDWTWSWSXBWJW
+        TRZWIWSRZWNWSRZURZVCZWPWQXGWPWGWIDUSPZQZWGWNXHQZUIZWQXGWMXIWOXJXGBCWKWI
+        WGDWJGWLHACDUTPUIWHXFITZADVDRWHXFXATZABWTUIWHXFKTZXGWJWTBXBXCXDXEVAXNVB
+        ZAGBRWHXFLTZAHBRWHXFMTZXGWKVEZXGWLVEZVFXGBCWKWNWGDWJGWLHXLXMXNXOXPXQXRX
+        SVFVGXGDVNRZWIDUKPZRWNYARWGYARXKWQVHAXTWHXFJTXGWIWSYAXBXCXDXEVIXGBCWEDW
+        JGXLXMXNXOXPXGWEVEZVJZUPXGWNWSYAXBXCXDXEVKYCUPXGWGWFYAAWHXFVLXGBCWEDGHX
+        LXMXNXPXQYBVJUPYAXHDWIWNWGYASXHSVMVOVPVQVRVSVTAFWCGHOWAAEWEGHNWAWB $.
+    $}
+
+    ${
+      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 w3a cplusg cmndtc simpr1 eleqtrrd
+        wa cmnd eqidd mndtcco2 eqeq12d wb simpr2 mndtchom simpr3 simplr grprcan
+        cgrp syl13anc bitrd biimpd ralrimivvva monepilem eqrdv oveqd 3eqtr4d )
+        AGHCUEPZQZGHCUFPZQZGHDQGHFQAUAWDWFAUAULZWDRWGWFRZUBULZWGGHUGUCULZCUHPZQ
+        ZQZUDULZWGWLQZUIZWIWNUIZUMZUDHWJWEQZUJUBWSUJUCCUKPZUJAUCWTCWKUBUDWCWGWE
+        GHWTSWESWKSWCSACEIAEJUNZUOAGBWTLKUPAHBWTMKUPUQAWHVCZWRUCUBUDWTWSWSXBWJW
+        TRZWIWSRZWNWSRZURZVCZWPWQXGWPWIWGEUSPZQZWNWGXHQZUIZWQXGWMXIWOXJXGBCWKWG
+        WIEGHWLWJACEUTPUIWHXFITZAEVDRWHXFXATZABWTUIWHXFKTZAGBRWHXFLTZAHBRWHXFMT
+        ZXGWJWTBXBXCXDXEVAXNVBZXGWKVEZXGWLVEZVFXGBCWKWGWNEGHWLWJXLXMXNXOXPXQXRX
+        SVFVGXGEVNRZWIEUKPZRWNYARWGYARXKWQVHAXTWHXFJTXGWIWSYAXBXCXDXEVIXGBCWEEH
+        WJXLXMXNXPXQXGWEVEZVJZUPXGWNWSYAXBXCXDXEVKYCUPXGWGWFYAAWHXFVLXGBCWEEGHX
+        LXMXNXOXPYBVJUPYAXHEWIWNWGYASXHSVMVOVPVQVRVSVTADWCGHOWAAFWEGHNWAWB $.
+    $}
+  $}
+
 $( (End of Zhi Wang's mathbox.) $)
 $( End $[ set-mbox-zw.mm $] $)