Correspondence between ODual(order dual)/oppG(opposite monoid) and oppCat (opposite category) (#5022)

* [add] assa2ass2; [shorten] assa2ass

* [add] asclcom

* [add] elmgpcntrd

* [prove] asclcntr; [add] asclelbas

* [minimize] asclcom

* [delete] assascacom and assascacrng

* [improve] explanation of asclcom

* [rename] structure map of associative algebra might be non-injective; [fix] algebraic scalars map -> algebra scalars map

* [add] upcic (empty proof), upciclem1

* [change] upciclem1: var change

* [add] isisod; [prove] upcic; [propose] upciclem2; [move] reueqdv to main

* [add] funcrcl2, funcrcl3; [update] upcic, upciclem2

* [shorten] upcic with funcrcl2

* [fix] functor

* [add] funcel1; [propose] funcel2

* Revert "[add] funcel1; [propose] funcel2"

This reverts commit 5fb5705.

* [prove] upciclem2

* [remove] upciclem2.n; [reformat] hypotheses; [trivial] formatting

* [trivial] formatting

* [add] a section for Universal property

* [add] upeu

* [fix] upeu description

* [add] upeu2lem, reuxfr1dd, upciclem2; [shorten] upciclem3; [propose] upeu2

* [prove] upeu2

* [move] reuxfr1dd; [fix] upciclem1 description

* [move and fix] upeu2lem and description and line length

* [propose] oppgtoppc

* [fix] oppgtoppc; [formatting]

* [add] oppgoppchom

* [add] oppgoppcco

* [add] oppgoppcid

* [add] oppgoppc comments; [fix] format

* [add] thinccisod, oduoppcbas; [propose] oduoppcciso, oduoppc, oduoppccom

* [move] oduprs from AV's mathbox to main

* [prove] oduoppcciso

* [fix] oduprs from TA's mathbox

Author: zwang123

changes-set.txt

@@ -96,6 +96,7 @@ Date      Old       New         Notes
 23-Sep-25 coecj     [same]      Removed unneeded hypothesis
 23-Sep-25 plycj     [same]      Removed unneeded hypothesis
 23-Sep-25 elfzolem1 [same]      moved from GS's mathbox to main set.mm
+22-Sep-25 oduprs    [same]      Moved from TA's mathbox to main set.mm
 17-Sep-25 psdmul    [same]      Removed unneeded hypothesis
 17-Sep-25 psdvsca   [same]      Removed unneeded hypothesis
 17-Sep-25 psdadd    [same]      Removed unneeded hypothesis

set.mm

@@ -225405,6 +225405,25 @@ that F(A') is isomorphic to B'.".  Therefore, the category of sets and
       CLMZDFCLZRSMDDCLTUANABCDEFGHOPQ $.
   $}
 
+  ${
+    $d x y z D $.  $d x y z K $.
+    oduprs.d $e |- D = ( ODual ` K ) $.
+    $( Being a proset is a self-dual property.  (Contributed by Thierry Arnoux,
+       13-Sep-2018.) $)
+    oduprs $p |- ( K e. Proset -> D e. Proset ) $=
+      ( vx vy vz cproset wcel cvv cv wbr wa wral isprs r19.21bi vex brcnv an32s
+      wi ralrimiva cple cfv ccnv cbs eqid simprbi simpld sylibr simprd anbi12ci
+      ex imp 3imtr4g jca codu fvexi jctil odubas oduleval ) BGHZAIHZDJZVBBUAUBZ
+      UCZKZVBEJZVDKZVFFJZVDKZLZVBVHVDKZSZLZFBUDUBZMZEVNMZDVNMZLAGHUTVQVAUTVPDVN
+      UTVBVNHZLZVOEVNVSVFVNHZLZVMFVNWAVHVNHZLZVEVLWCVBVBVCKZVEWCWDVBVFVCKVFVHVC
+      KLVBVHVCKSZWAWDWELZFVNVSWFFVNMZEVNUTWGEVNMZDVNUTBIHZWHDVNMDEFVNBVCVNUEZVC
+      UEZNUFOOOUGVBVBVCDPZWLQUHWCVHVFVCKZVFVBVCKZLZVHVBVCKZVJVKVSWBVTWOWPSZVSWB
+      LVTWQUTWBVRVTWQSUTWBLZVRLVTWQWRVTVRWQWRVTLZVRLVHVHVCKZWQWSWTWQLZDVNWRXADV
+      NMZEVNUTXBEVNMZFVNUTWIXCFVNMFEDVNBVCWJWKNUFOOOUIRUKRULRVGWNVIWMVBVFVCWLEP
+      ZQVFVHVCXDFPZQUJVBVHVCWLXEQUMUNTTTABUOCUPUQDEFVNAVDVNABCWJURAVCBCWKUSNUH
+      $.
+  $}
+
   ${
     $d K f b r x y z $.  $d B f b r x y z $.  $d .<_ f b r x y z $.
     $d X x y z $.  $d Y x y z $.
@@ -509531,25 +509550,6 @@ Splicing words (substring replacement)
       RTVLWKVPVRVTXRTVEVLWKVPVOVTXRTVFVEQQQVGVHEFGWFVMVPWFNVPNUOVI $.
   $}
 
-  ${
-    $d x y z D $.  $d x y z K $.
-    oduprs.d $e |- D = ( ODual ` K ) $.
-    $( Being a proset is a self-dual property.  (Contributed by Thierry Arnoux,
-       13-Sep-2018.) $)
-    oduprs $p |- ( K e. Proset -> D e. Proset ) $=
-      ( vx vy vz cproset wcel cvv cv wbr wa wral isprs r19.21bi vex brcnv an32s
-      wi ralrimiva cple cfv ccnv cbs eqid simprbi simpld sylibr simprd anbi12ci
-      ex imp 3imtr4g jca codu fvexi jctil odubas oduleval ) BGHZAIHZDJZVBBUAUBZ
-      UCZKZVBEJZVDKZVFFJZVDKZLZVBVHVDKZSZLZFBUDUBZMZEVNMZDVNMZLAGHUTVQVAUTVPDVN
-      UTVBVNHZLZVOEVNVSVFVNHZLZVMFVNWAVHVNHZLZVEVLWCVBVBVCKZVEWCWDVBVFVCKVFVHVC
-      KLVBVHVCKSZWAWDWELZFVNVSWFFVNMZEVNUTWGEVNMZDVNUTBIHZWHDVNMDEFVNBVCVNUEZVC
-      UEZNUFOOOUGVBVBVCDPZWLQUHWCVHVFVCKZVFVBVCKZLZVHVBVCKZVJVKVSWBVTWOWPSZVSWB
-      LVTWQUTWBVRVTWQSUTWBLZVRLVTWQWRVTVRWQWRVTLZVRLVHVHVCKZWQWSWTWQLZDVNWRXADV
-      NMZEVNUTXBEVNMZFVNUTWIXCFVNMFEDVNBVCWJWKNUFOOOUIRUKRULRVGWNVIWMVBVFVCWLEP
-      ZQVFVHVCXDFPZQUJVBVHVCWLXEQUMUNTTTABUOCUPUQDEFVNAVDVNABCWJURAVCBCWKUSNUH
-      $.
-  $}
-
   ${
     posrasymb.b $e |- B = ( Base ` K ) $.
     posrasymb.l $e |- .<_ = ( ( le ` K ) i^i ( B X. B ) ) $.
@@ -838272,6 +838272,38 @@ preorders induced by the categories are considered ( ~ catprs2 ).
       LUUGUUJUWHYLYMYOYPYQFGUUJUWHXCYRXKXMXLYSYT $.
   $}
 
+  ${
+    $d C f x y $.  $d F f x y $.  $d H f x y $.  $d J f x y $.  $d R f x y $.
+    $d S f $.  $d U f $.  $d V f $.  $d X f x y $.  $d Y f x y $.
+    $d f ph x y $.
+    thinccisod.c $e |- C = ( CatCat ` U ) $.
+    thinccisod.r $e |- R = ( Base ` X ) $.
+    thinccisod.s $e |- S = ( Base ` Y ) $.
+    thinccisod.h $e |- H = ( Hom ` X ) $.
+    thinccisod.j $e |- J = ( Hom ` Y ) $.
+    thinccisod.u $e |- ( ph -> U e. V ) $.
+    thinccisod.x $e |- ( ph -> X e. U ) $.
+    thinccisod.y $e |- ( ph -> Y e. U ) $.
+    thinccisod.xt $e |- ( ph -> X e. ThinCat ) $.
+    thinccisod.yt $e |- ( ph -> Y e. ThinCat ) $.
+    thinccisod.f $e |- ( ph -> F : R -1-1-onto-> S ) $.
+    thinccisod.1 $e |- ( ( ph /\ ( x e. R /\ y e. R ) ) ->
+            ( ( x H y ) = (/) <-> ( ( F ` x ) J ( F ` y ) ) = (/) ) ) $.
+    $( Two thin categories are isomorphic if the induced preorders are
+       order-isomorphic (deduction form).  Example 3.26(2) of [Adamek] p. 33.
+       (Contributed by Zhi Wang, 22-Sep-2025.) $)
+    thinccisod $p  |- ( ph -> X ( ~=c ` C ) Y ) $=
+      ( vf ccic cfv wbr cv co c0 wceq wb wral wf1o wa wex cvv wf f1of syl fvexd
+      cbs eqeltrid fexd ralrimivva fveq1 oveq12d eqeq1d bibi2d 2ralbidv anbi12d
+      jca f1oeq1 spcedv eqid ccat cin thinccd catcbas eleqtrrd thincciso mpbird
+      elind ) ALMDUGUHUIBUJZCUJZIUKULUMZWFUFUJZUHZWGWIUHZJUKZULUMZUNZCEUOBEUOZE
+      FWIUPZUQZUFURAWQWHWFHUHZWGHUHZJUKZULUMZUNZCEUOBEUOZEFHUPZUQUFUSHAEFUSHAXD
+      EFHUTUDEFHVAVBAELVDUHUSOALVDVCVEVFAXCXDAXBBCEEUEVGUDVNWIHUMZWOXCWPXDXEWNX
+      BBCEEXEWMXAWHXEWLWTULXEWJWRWKWSJWFWIHVHWGWIHVHVIVJVKVLEFWIHVOVMVPABCDVDUH
+      ZDEFGUFIJKLMNXFVQZOPQRSALGVRVSZXFAGVRLTALUBVTWEAXFDGKNXGSWAZWBAMXHXFAGVRM
+      UAAMUCVTWEXIWBUBUCWCWD $.
+  $}
+
   ${
     $d C f x y $.
     $( Any structure with an empty set of objects is a thin category.
@@ -838659,8 +838691,64 @@ mean the category of preordered sets (classes).  However, "ProsetToCat"
         GUKZPQOAULRZPSTAUMRZUNUOVJPQUPUQCVJURUSVLAVJSTZVIVLVKCUTVSVKCVBCVJVCVDA
         VIVSAGHFDQPVPVQVRVEVFVGVH $.
     $}
+
+    oduoppcbas.d $e |- ( ph -> D = ( ProsetToCat ` ( ODual ` K ) ) ) $.
+    oduoppcbas.o $e |- O = ( oppCat ` C ) $.
+    $( The dual of a preordered set and the opposite category have the same set
+       of objects.  (Contributed by Zhi Wang, 22-Sep-2025.) $)
+    oduoppcbas $p |- ( ph -> ( Base ` D ) = ( Base ` O ) ) $=
+      ( cbs cfv codu cproset wcel eqid oduprs syl wceq odubas prstcbas oppcbas
+      a1i eqcomd eqtrdi ) ACJKZBJKZEJKAUEBDFGADJKZUEAUGCDLKZHADMNUHMNGUHDUHOZPQ
+      UGUHJKRAUGUHDUIUGOSUBTUCTUFBEIUFOUAUD $.
+
+    ${
+      $d C x y $.  $d D x y $.  $d K x y $.  $d O x y $.  $d U x y $.
+      $d V x y $.  $d ph x y $.
+      oduoppcciso.u $e |- ( ph -> U e. V ) $.
+      oduoppcciso.d $e |- ( ph -> D e. U ) $.
+      oduoppcciso.o $e |- ( ph -> O e. U ) $.
+      $( The dual of a preordered set and the opposite category are
+         category-isomorphic.  Example 3.6(1) of [Adamek] p. 25.  (Contributed
+         by Zhi Wang, 22-Sep-2025.) $)
+      oduoppcciso $p |- ( ph -> D ( ~=c ` ( CatCat ` U ) ) O ) $=
+        ( cfv eqid wcel co c0 wceq vx vy ccatc cbs cid cres chom cproset oduprs
+        codu prstcthin cthinc oppcthin wf1o f1oi oduoppcbas f1oeq3d mpbii cv wa
+        syl cple wbr wne wb oduleg adantl cprstc adantr eqidd prstcleval simprl
+        simprr prstchom oppcbas eqtr4di eleqtrd 3bitr3d fvresi ad2antrl oveq12d
+        necon4bid ad2antll oppchom eqtrdi eqeq1d bitr4d thinccisod ) AUAUBDUCOZ
+        CUDOZFUDOZDUEWJUFZCUGOZFUGOZGCFWIPWJPWKPWMPWNPLMNACEUJOZJAEUHQZWOUHQZIW
+        OEWOPZUIZVAUKABULQFULQABEHIUKBFKUMVAAWJWJWLUNWJWKWLUNWJUOAWJWKWJWLABCEF
+        HIJKUPZUQURAUAUSZWJQZUBUSZWJQZUTZUTZXAXCWMRZSTXCXABUGOZRZSTXAWLOZXCWLOZ
+        WNRZSTXFXGSXISXFXAXCWOVBOZVCZXCXAEVBOZVCZXGSVDXISVDXEXNXPVEAXAXCWOXMXOE
+        WJWJWRXOPXMPVFVGXFCWMWOXMXAXCACWOVHOTXEJVIZXFWPWQAWPXEIVIZWSVAZXFCWOXMX
+        QXSXFXMVJVKXFWMVJAXBXDVLZAXBXDVMZVNXFBXHEXOXCXAABEVHOTXEHVIZXRXFBEXOYBX
+        RXFXOVJVKXFXHVJXFXCWJBUDOZYAAWJYCTXEAWJWKYCWTYCBFKYCPVOVPVIZVQXFXAWJYCX
+        TYDVQVNVRWBXFXLXISXFXLXAXCWNRXIXFXJXAXKXCWNXBXJXATAXDWJXAVSVTXDXKXCTAXB
+        WJXCVSWCWABXHFXAXCXHPKWDWEWFWGWH $.
+    $}
+
+$(
+    The following cannot be proved without using discouraged theorems such as
+    ~ prstchomval .
+    @( The dual of a preordered set and the opposite category have the same set
+       of objects, morphisms, and compositions.  Example 3.6(1) of [Adamek]
+       p. 25.  (Contributed by Zhi Wang, XX-Sep-2025.) @)
+    oduoppc @p |- ( ph -> ( ( Homf ` D ) = ( Homf ` O )
+                         /\ ( comf ` D ) = ( comf ` O ) ) ) @=
+      (  ) ? @.
+$)
   $}
 
+$(
+    The following cannot be proved without using discouraged theorems such as
+    ~ prstchomval .
+  @( The correspondence between order dual and opposite category.  Example
+     3.6(1) of [Adamek] p. 25.  (Contributed by Zhi Wang, XX-Sep-2025.) @)
+  oduoppccom @p |- ( ProsetToCat o. ( ODual |` Proset ) )
+                   = ( ODual o. ( oppCat o. ProsetToCat ) ) @=
+    (  ) ? @.
+$)
+
   ${
     $d B x y $.  $d C x y $.  $d ph x y $.
     postc.c $e |- ( ph -> C = ( ProsetToCat ` K ) ) $.
@@ -838849,16 +838937,77 @@ structure becomes the object here (see ~ mndtcbasval ), instead of just
       ( 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 $.
+    ${
+      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 wcel mndtccatid eqtrd cv eqidd
+        simprd wa eleqtrd fvexd fvmptd ) ALFEMNZUKCONZDPADCQNZLULUKRZKACSUAUMUN
+        TALCEGHUBUFUCALUDFTUGUKUEAFBULJIUHAEMUIUJ $.
+    $}
+
+    ${
+      oppgoppchom.d $e |- ( ph -> D = ( MndToCat ` ( oppG ` M ) ) ) $.
+      oppgoppchom.o $e |- O = ( oppCat ` C ) $.
+      oppgoppchom.x $e |- ( ph -> X e. ( Base ` D ) ) $.
+      oppgoppchom.y $e |- ( ph -> Y e. ( Base ` O ) ) $.
+      ${
+        oppgoppchom.h $e |- ( ph -> H = ( Hom ` D ) ) $.
+        oppgoppchom.j $e |- ( ph -> J = ( Hom ` O ) ) $.
+        $( The converted opposite monoid has the same hom-set as that of the
+           opposite category.  Example 3.6(2) of [Adamek] p. 25.  (Contributed
+           by Zhi Wang, 21-Sep-2025.) $)
+        oppgoppchom $p |- ( ph -> ( X H X ) = ( Y J Y ) ) $=
+          ( co cfv cbs chom coppg wceq eqid oppgbas a1i oppcbas eqcomi mndtchom
+          eqidd cmnd wcel oppgmnd syl 3eqtr4rd oppchom eqtr4di oveqd eqtr4d ) A
+          HHDRZIIGUASZRZIIERAUTIIBUASZRZVBAFTSZFUBSZTSZVDUTVEVGUCAVEFVFVFUDZVEU
+          DUEUFAGTSZBVCFIIJKVIBTSZUCAVJVIVJBGMVJUDUGUHUFOOAVCUJUIACTSZCDVFHHLAF
+          UKULVFUKULKFVFVHUMUNAVKUJNNPUIUOBVCGIIVCUDMUPUQAEVAIIQURUS $.
+      $}
+
+      ${
+        oppgoppcco.o $e |- ( ph -> .x. = ( comp ` D ) ) $.
+        oppgoppcco.x $e |- ( ph -> .xb = ( comp ` O ) ) $.
+        $( The converted opposite monoid has the same composition as that of
+           the opposite category.  Example 3.6(2) of [Adamek] p. 25.
+           (Contributed by Zhi Wang, 22-Sep-2025.) $)
+        oppgoppcco $p |- ( ph -> ( <. X , X >. .x. X ) =
+                  ( <. Y , Y >. .xb Y ) ) $=
+          ( co cfv eqid cop cco ctpos cplusg cbs wceq oppcbas a1i eqidd mndtcco
+          eqcomi tposeqd oppccofval coppg cmnd wcel oppgmnd oppgplusfval eqtrdi
+          syl 3eqtr4rd oveqd eqtr4d ) AHHUAHERZIIUAZIGUBSZRZVEIDRAVEIBUBSZRZUCF
+          UDSZUCZVGVDAVIVJAGUESZBVHFIIIJKVLBUESZUFAVMVLVMBGMVMTUGUKZUHOOOAVHUIU
+          JULAVLBVHGIIIVNVHTMOOOUMAVDFUNSZUDSZVKACUESZCEVOHHHLAFUOUPVOUOUPKFVOV
+          OTZUQUTAVQUINNNPUJVJVPFVOVJTVRVPTURUSVAADVFVEIQVBVC $.
+      $}
+
+      $( The converted opposite monoid has the same identity morphism as that
+         of the opposite category.  Example 3.6(2) of [Adamek] p. 25.
+         (Contributed by Zhi Wang, 22-Sep-2025.) $)
+      oppgoppcid $p |- ( ph -> ( ( Id ` D ) ` X ) = ( ( Id ` O ) ` Y ) ) $=
+        ( c0g cfv ccid wceq eqid cbs wcel coppg oppgid a1i eqcomi ccat mndtccat
+        oppcbas oppcid syl mndtcid cmnd oppgmnd eqidd 3eqtr4rd ) ADNOZDUAOZNOZG
+        EPOZOFCPOZOUOUQQADUPUOUPRZUORUBUCAESOZBURDGHIVABSOZQAVBVAVBBEKVBRUGUDUC
+        MABUETURBPOZQABDHIUFVCBEKVCRUHUIUJACSOZCUSUPFJADUKTUPUKTIDUPUTULUIAVDUM
+        LAUSUMUJUN $.
+    $}
+
+$(
+    The following is not true yet because base set of converted category
+    depends on the original monoid in the current definition.
+    @{
+      oppgtoppc.o @e |- O = ( oppG ` M ) @.
+      oppgtoppc.d @e |- ( ph -> D = ( MndToCat ` O ) ) @.
+      @( An opposite monoid is converted to an opposite category.  Example
+         3.6(2) of [Adamek] p. 25.  (Contributed by Zhi Wang, XX-Sep-2025.) @)
+      oppgtoppc @p |- ( ph -> D = ( oppCat ` C ) ) @=
+        (  ) ? @.
+    @}
+$)
   $}
 
   ${