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

Author: zwang123

changes-set.txt

@@ -92,6 +92,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+16-Sep-25 reueqdv   [same]      Moved from GG's mathbox to main set.mm
 11-Sep-25 cascl     [same]      revised - algSc may be non-injective
 24-Aug-25 elrab2w   [same]      Moved from SN's mathbox to main set.mm
 24-Aug-25 elab2gw   [same]      Moved from SN's mathbox to main set.mm

set.mm

@@ -31921,6 +31921,16 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       ( wceq wreu reueq1 reubidv bitrd ) DEGZACDHACEHBCEHACDEILABCEFJK $.
   $}
 
+  ${
+    $d A x $.  $d B x $.
+    reueqdv.1 $e |- ( ph -> A = B ) $.
+    $( Formula-building rule for restricted existential uniqueness quantifier.
+       Deduction form.  (Contributed by GG, 1-Sep-2025.) $)
+    reueqdv $p |- ( ph -> ( E! x e. A ps <-> E! x e. B ps ) ) $=
+      ( wceq wreu wb reueq1 syl ) ADEGBCDHBCEHIFBCDEJK $.
+    $( $j usage 'reueqdv' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
+  $}
+
   ${
     rmoeq1f.1 $e |- F/_ x A $.
     rmoeq1f.2 $e |- F/_ x B $.
@@ -579686,16 +579696,6 @@ conditions of the Five Segment Axiom ( ~ ax5seg ).  See ~ brofs and
     $( $j usage 'rmoeqbidv' avoids 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
   $}
 
-  ${
-    $d A x $.  $d B x $.
-    reueqdv.1 $e |- ( ph -> A = B ) $.
-    $( Formula-building rule for restricted existential uniqueness quantifier.
-       Deduction form.  (Contributed by GG, 1-Sep-2025.) $)
-    reueqdv $p |- ( ph -> ( E! x e. A ps <-> E! x e. B ps ) ) $=
-      ( wceq wreu wb reueq1 syl ) ADEGBCDHBCEHIFBCDEJK $.
-    $( $j usage 'reueqdv' avoids 'ax-8' 'ax-10' 'ax-11' 'ax-12' 'ax-13'; $)
-  $}
-
   ${
     $d ph x $.
     reueqbidv.1 $e |- ( ph -> A = B ) $.
@@ -835438,6 +835438,38 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
   $}
 
 
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+  Sections, inverses, isomorphisms
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+$)
+
+  ${
+    $d .1. g $.  $d .x. g $.  $d B g $.  $d C g $.  $d F g $.  $d G g $.
+    $d H g $.  $d I g $.  $d X g $.  $d Y g $.  $d g ph $.
+    isisod.b $e |- B = ( Base ` C ) $.
+    isisod.h $e |- H = ( Hom ` C ) $.
+    isisod.o $e |- .x. = ( comp ` C ) $.
+    isisod.i $e |- I = ( Iso ` C ) $.
+    isisod.1 $e |- .1. = ( Id ` C ) $.
+    isisod.c $e |- ( ph -> C e. Cat ) $.
+    isisod.x $e |- ( ph -> X e. B ) $.
+    isisod.y $e |- ( ph -> Y e. B ) $.
+    isisod.f $e |- ( ph -> F e. ( X H Y ) ) $.
+    isisod.g $e |- ( ph -> G e. ( Y H X ) ) $.
+    isisod.gf $e |- ( ph -> ( G ( <. X , Y >. .x. X ) F ) = ( .1. ` X ) ) $.
+    isisod.fg $e |- ( ph -> ( F ( <. Y , X >. .x. Y ) G ) = ( .1. ` Y ) ) $.
+    $( The predicate "is an isomorphism" (deduction form).  (Contributed by Zhi
+       Wang, 16-Sep-2025.) $)
+    isisod $p |- ( ph -> F e. ( X I Y ) ) $=
+      ( vg co wcel cv cop cfv wceq wa wrex oveq1d eqeq1d oveq2d anbi12d rspcedv
+      simpr mp2and cco oveqi dfiso2 mpbird ) AFJKIUEUFUDUGZFJKUHZJDUEZUEZJEUIZU
+      JZFVDKJUHZKDUEZUEZKEUIZUJZUKZUDKJHUEZULZAGFVFUEZVHUJZFGVKUEZVMUJZVQUBUCAV
+      OVSWAUKUDGVPUAAVDGUJZUKZVIVSVNWAWCVGVRVHWCVDGFVFAWBURZUMUNWCVLVTVMWCVDGFV
+      KWDUOUNUPUQUSABCEUDFHIVKJKVFLMQORSTPDCUTUIZVEJNVADWEVJKNVAVBVC $.
+  $}
+
+
 $(
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
   Functors
@@ -835487,6 +835519,38 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
   $}
 
   ${
+    upciclem2.b $e |- B = ( Base ` D ) $.
+    upciclem2.c $e |- C = ( Base ` E ) $.
+    upciclem2.h $e |- H = ( Hom ` D ) $.
+    upciclem2.j $e |- J = ( Hom ` E ) $.
+    upciclem2.od $e |- .x. = ( comp ` D ) $.
+    upciclem2.o $e |- O = ( comp ` E ) $.
+    upciclem2.f $e |- ( ph -> F ( D Func E ) G ) $.
+    upciclem2.x $e |- ( ph -> X e. B ) $.
+    upciclem2.y $e |- ( ph -> Y e. B ) $.
+    upciclem2.z $e |- ( ph -> Z e. C ) $.
+    upciclem2.k $e |- ( ph -> K e. ( X H Y ) ) $.
+    upciclem2.l $e |- ( ph -> L e. ( Y H X ) ) $.
+    upciclem2.m $e |- ( ph -> M e. ( Z J ( F ` X ) ) ) $.
+    upciclem2.n $e |- ( ph -> N e. ( Z J ( F ` Y ) ) ) $.
+    upciclem2.mn $e |- ( ph -> M = ( ( G ` L )
+                               ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) $.
+    upciclem2.nm $e |- ( ph -> N = ( ( G ` K )
+                               ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) $.
+    $( Lemma for ~ upcic .  (Contributed by Zhi Wang, 16-Sep-2025.) $)
+    upciclem2 $p |- ( ph -> ( L ( <. X , Y >. .x. X ) K )
+                          = ( ( Id ` D ) ` X ) ) $=
+      (  ) ? $.
+  $}
+
+  ${
+    $d B p q v $.  $d B p q w $.  $d D p q $.  $d F f k p q w $.
+    $d F g l p q v $.  $d G f k p q w $.  $d G g l p q v $.  $d H f k p q w $.
+    $d H g l p q v $.  $d J f p q w $.  $d J g p q v $.  $d M f k w $.
+    $d M g l $.  $d M p q $.  $d N f k $.  $d N g l v $.  $d N p q $.
+    $d O f k p q w $.  $d O g l p q v $.  $d X f k p q w $.  $d X g l p q v $.
+    $d Y f k p q w $.  $d Y g l p q v $.  $d Z f k p q w $.  $d Z g l p q v $.
+    $d p ph q $.
     upcic.b $e |- B = ( Base ` D ) $.
     upcic.c $e |- C = ( Base ` E ) $.
     upcic.h $e |- H = ( Hom ` D ) $.
@@ -835500,12 +835564,23 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
             f = ( ( G ` k ) ( <. Z , ( F ` X ) >. O ( F ` w ) ) M ) ) $.
     upcic.y $e |- ( ph -> Y e. B ) $.
     upcic.n $e |- ( ph -> N e. ( Z J ( F ` Y ) ) ) $.
-    upcic.2 $e |- ( ph -> A. w e. B A. f e. ( Z J ( F ` w ) ) E! k e. ( Y H w )
-            f = ( ( G ` k ) ( <. Z , ( F ` Y ) >. O ( F ` w ) ) N ) ) $.
+    upcic.2 $e |- ( ph -> A. v e. B A. g e. ( Z J ( F ` v ) ) E! l e. ( Y H v )
+            g = ( ( G ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) ) $.
     $( A universal property defines an object up to isomorphism given its
-       existence.  (Contributed by Zhi Wang, XX-Sep-2025.) $)
+       existence.  (Contributed by Zhi Wang, 16-Sep-2025.) $)
     upcic $p |- ( ph -> X ( ~=c ` D ) Y ) $=
-      (  ) ? $.
+      ( vp vq cv cfv cop co wceq ccic wbr wreu wrex upciclem1 reurex wcel simpl
+      syl wa 3syl ciso eqid cfunc ccat simpll df-br sylib funcrcl 4syl ad2antrr
+      cco ccid simplrl simprl simprr simplrr upciclem2 isisod brcici rexlimddv
+      ) APUOUQZLUROTRKURZUSSKURZQUTUTVAZRSFVBURVCZUORSMUTZAWPUOWRVDWPUOWRVEABDI
+      GKLMNOPQRSTUOUKULUMVFWPUOWRVGVJAWMWRVHZWPVKZVKZOUPUQZLURPTWOUSWNQUTUTVAZW
+      QUPSRMUTZXAAXCUPXDVDXCUPXDVEAWTVIACDUAHKLMNPOQSRTUPUNUIUJVFXCUPXDVGVLXAXB
+      XDVHZXCVKZVKZDFWMFVMURZRSXHVNZUBXGAKLUSZFJVOUTZVHZFVPVHZJVPVHZVKXMAWTXFVQ
+      AKLXKVCZXLUGKLXKVRVSFJXJVTXMXNVIWAZARDVHWTXFUIWBZASDVHWTXFULWBZXGDFFWCURZ
+      FWDURZWMXBMXHRSUBUDXSVNZXIXTVNXPXQXRAWSWPXFWEZXAXEXCWFZXGDEFXSJKLMNWMXBOP
+      QRSTUBUCUDUEYAUFAXOWTXFUGWBZXQXRATEVHWTXFUHWBZYBYCAOTWNNUTVHWTXFUJWBZAPTW
+      ONUTVHWTXFUMWBZXAXEXCWGZAWSWPXFWHZWIXGDEFXSJKLMNXBWMPOQSRTUBUCUDUEYAUFYDX
+      RXQYEYCYBYGYFYIYHWIWJWKWLWL $.
   $}