[add] upeu

Author: zwang123

set.mm

@@ -835584,33 +835584,57 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
     $}
 
     ${
-      $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 $.
+      $d B p q v $.  $d B p q w $.  $d D p q r $.  $d F f k p q w $.
+      $d F g l p q v $.  $d F p q r $.  $d G f k p q w $.  $d G g l p q v $.
+      $d G p q r $.  $d H f k p q w $.  $d H g l p q v $.  $d H p q r $.
+      $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 r $.  $d N f k $.  $d N g l v $.  $d N p q r $.
+      $d O f k p q w $.  $d O g l p q v $.  $d O p q r $.  $d X f k p q w $.
+      $d X g l p q v $.  $d X p q r $.  $d Y f k p q w $.  $d Y g l p q v $.
+      $d Y p q r $.  $d Z f k p q w $.  $d Z g l p q v $.  $d Z p q r $.
+      $d p ph q $.
       upcic.n $e |- ( ph -> N e. ( Z J ( F ` Y ) ) ) $.
       upcic.2 $e |- ( ph -> A. v e. B A. g e. ( Z J ( F ` v ) )
            E! l e. ( Y H v )
            g = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) ) $.
+      $( Lemma for ~ upcic and ~ upeu .  (Contributed by Zhi Wang,
+         19-Sep-2025.) $)
+      upciclem3 $p |- ( ph -> ( X ( ~=c ` D ) Y /\ E. r e. ( X ( Iso ` D ) Y )
+         N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) $=
+        ( vp vq ccic cfv wbr cv co cop wceq ciso wrex wreu upciclem1 reurex syl
+        wcel wa simpl 3syl eqid cfunc ad2antrr funcrcl2 cco ccid simplrl simprl
+        simprr simplrr upciclem2 isisod brcici rexlimddv reximssdv fveq2 oveq1d
+        wral eqeq2d cbvrexvw sylib jca ) ARSFURUSUTZPUAVAZRSLVBZUSZOTRKUSZVCZSK
+        USZQVBZVBZVDZUARSFVEUSZVBZVFZAPUPVAZWSUSZOXDVBZVDZWQUPRSMVBZAXMUPXNVGXM
+        UPXNVFABDIGKLMNOPQRSTUPUMUJUNVHXMUPXNVIVJZAXJXNVKZXMVLZVLZOUQVAZSRLVBUS
+        PTXCVCZXAQVBVBVDZWQUQSRMVBZXRAYAUQYBVGYAUQYBVFAXQVMACDUBHKLMNPOQSRTUQUO
+        UIULVHYAUQYBVIVNZXRXSYBVKZYAVLZVLZDFXJXGRSXGVOZUCYFFJKLAKLFJVPVBUTXQYEU
+        HVQZVRZARDVKXQYEUIVQZASDVKXQYEUJVQZYFDFFVSUSZFVTUSZXJXSMXGRSUCUEYLVOZYG
+        YMVOYIYJYKAXPXMYEWAZXRYDYAWBZYFBDEFYLGIJKLMNXJXSOPQRSTUCUDUEUFUGYHYJYKA
+        TEVKXQYEUKVQZAOTXANVBVKXQYEULVQAGVAIVARBVAZLVBUSOXBYRKUSZQVBVBVDIRYRMVB
+        VGGTYSNVBWLBDWLXQYEUMVQYNYOYPXRYDYAWCZAXPXMYEWDZWEYFCDEFYLHUBJKLMNXSXJP
+        OQSRTUCUDUEUFUGYHYKYJYQAPTXCNVBVKXQYEUNVQAHVAUBVASCVAZLVBUSPXTUUBKUSZQV
+        BVBVDUBSUUBMVBVGHTUUCNVBWLCDWLXQYEUOVQYNYPYOUUAYTWEWFZWGWHWHAXMUPXHVFXI
+        AXMXMUPXHXNXOXRYAXJXHVKUQYBYCUUDWHAXPXMWCWIXMXFUPUAXHXJWRVDZXLXEPUUEXKW
+        TOXDXJWRWSWJWKWMWNWOWP $.
+
       $( A universal property defines an object up to isomorphism given its
          existence.  (Contributed by Zhi Wang, 17-Sep-2025.) $)
       upcic $p |- ( ph -> X ( ~=c ` D ) Y ) $=
-        ( vp vq cv co cfv cop wceq ccic wbr wreu wrex upciclem1 reurex syl wcel
-        wa simpl 3syl ciso eqid cfunc ad2antrr funcrcl2 cco ccid simplrl simprl
-        wral simprr simplrr upciclem2 isisod brcici rexlimddv ) APUOUQZRSLURUSO
-        TRKUSZUTZSKUSZQURURVAZRSFVBUSVCZUORSMURZAWMUOWOVDWMUOWOVEABDIGKLMNOPQRS
-        TUOULUIUMVFWMUOWOVGVHAWIWOVIZWMVJZVJZOUPUQZSRLURUSPTWLUTZWJQURURVAZWNUP
-        SRMURZWRAXAUPXBVDXAUPXBVEAWQVKACDUAHKLMNPOQSRTUPUNUHUKVFXAUPXBVGVLWRWSX
-        BVIZXAVJZVJZDFWIFVMUSZRSXFVNZUBXEFJKLAKLFJVOURVCWQXDUGVPZVQZARDVIWQXDUH
-        VPZASDVIWQXDUIVPZXEDFFVRUSZFVSUSZWIWSMXFRSUBUDXLVNZXGXMVNXIXJXKAWPWMXDV
-        TZWRXCXAWAZXEBDEFXLGIJKLMNWIWSOPQRSTUBUCUDUEUFXHXJXKATEVIWQXDUJVPZAOTWJ
-        NURVIWQXDUKVPAGUQIUQRBUQZLURUSOWKXRKUSZQURURVAIRXRMURVDGTXSNURWBBDWBWQX
-        DULVPXNXOXPWRXCXAWCZAWPWMXDWDZWEXECDEFXLHUAJKLMNWSWIPOQSRTUBUCUDUEUFXHX
-        KXJXQAPTWLNURVIWQXDUMVPAHUQUAUQSCUQZLURUSPWTYBKUSZQURURVAUASYBMURVDHTYC
-        NURWBCDWBWQXDUNVPXNXPXOYAXTWEWFWGWHWH $.
+        ( vr ccic cfv wbr cv co cop wceq ciso wrex upciclem3 simpld ) ARSFUPUQU
+        RPUOUSRSLUTUQOTRKUQVASKUQQUTUTVBUORSFVCUQUTVDABCDEFGHIJKLMNOPQRSTUOUAUB
+        UCUDUEUFUGUHUIUJUKULUMUNVEVF $.
+
+      $( A universal property defines an essentially unique (strong form)
+         object if it exists.  (Contributed by Zhi Wang, 19-Sep-2025.) $)
+      upeu $p |- ( ph -> E! r e. ( X ( Iso ` D ) Y )
+           N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) $=
+        ( cv co cfv cop wceq ciso wrex wrmo wreu ccic wbr upciclem3 simprd eqid
+        wss funcrcl2 isohom upciclem1 reurmo syl nfcv ssrmof sylc reu5 sylanbrc
+        ) APUAUPRSLUQUROTRKURUSSKURQUQUQUTZUARSFVAURZUQZVBZWAUAWCVCZWAUAWCVDARS
+        FVEURVFWDABCDEFGHIJKLMNOPQRSTUAUBUCUDUEUFUGUHUIUJUKULUMUNUOVGVHAWCRSMUQ
+        ZVJWAUAWFVCZWEADFMWBRSUCUEWBVIAFJKLUHVKUIUJVLAWAUAWFVDWGABDIGKLMNOPQRST
+        UAUMUJUNVMWAUAWFVNVOWAUAWCWFUAWCVPUAWFVPVQVRWAUAWCVSVT $.
     $}
   $}