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

Author: zwang123

set.mm

@@ -835481,14 +835481,14 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
     $( Reverse closure for a functor.  (Contributed by Zhi Wang,
        17-Sep-2025.) $)
     funcrcl2 $p |- ( ph -> D e. Cat ) $=
-          ( ccat wcel cfunc co wbr cop wa df-br biimpi funcrcl 3syl simpld ) AB
-          GHZCGHZADEBCIJZKZDELZUAHZSTMFUBUDDEUANOBCUCPQR $.
+      ( ccat wcel cfunc co wbr cop wa df-br biimpi funcrcl 3syl simpld ) ABGHZC
+      GHZADEBCIJZKZDELZUAHZSTMFUBUDDEUANOBCUCPQR $.
 
     $( Reverse closure for a functor.  (Contributed by Zhi Wang,
        17-Sep-2025.) $)
     funcrcl3 $p |- ( ph -> E e. Cat ) $=
-          ( ccat wcel cfunc co wbr cop wa df-br biimpi funcrcl 3syl simprd ) AB
-          GHZCGHZADEBCIJZKZDELZUAHZSTMFUBUDDEUANOBCUCPQR $.
+      ( ccat wcel cfunc co wbr cop wa df-br biimpi funcrcl 3syl simprd ) ABGHZC
+      GHZADEBCIJZKZDELZUAHZSTMFUBUDDEUANOBCUCPQR $.
   $}
 
   ${
@@ -835536,90 +835536,76 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
   $}
 
   ${
-    $d .x. p $.  $d B w $.  $d D p $.  $d F f k w $.  $d F p $.
-    $d G f k w $.  $d G p $.  $d H f k w $.  $d H p $.  $d J f w $.
-    $d K p $.  $d L p $.  $d M f k w $.  $d M p $.  $d O f k w $.
-    $d O p $.  $d X f k w $.  $d X p $.  $d Y p $.
-    $d Z f k w $.  $d Z p $.
-    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.1 $e |- ( ph -> A. w e. B
-           A. f e. ( Z J ( F ` w ) ) E! k e. ( X H w )
-           f = ( ( ( X G w ) ` k ) ( <. Z , ( F ` X ) >. O ( F ` w ) ) M ) ) $.
-    upciclem2.mn $e |- ( ph -> M = ( ( ( Y G X ) ` L )
-                               ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) $.
-    upciclem2.nm $e |- ( ph -> N = ( ( ( X G Y ) ` K )
-                               ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) $.
-    $( Lemma for ~ upcic .  (Contributed by Zhi Wang, 17-Sep-2025.) $)
-    upciclem2 $p |- ( ph -> ( L ( <. X , Y >. .x. X ) K )
-                          = ( ( Id ` D ) ` X ) ) $=
-      ( vp cv co cfv wceq ccid fveq2 oveq1d eqeq2d upciclem1 funcrcl2
-      cop catcocl eqid funcrcl3 funcf1 ffvelcdmd funcf2 catass funcco
-      catidcl oveq2d eqtrd 3eqtr4rd funcid catlid eqtr2d reu2eqd ) AP
-      USUTZSSKVAZVBZPUASJVBZVJZWJRVAZVAZVCPONSTVJSFVAVAZWHVBZPWLVAZVC
-      PSEVDVBZVBZWHVBZPWLVAZVCUSSSLVAWNWRWGWNVCZWMWPPXAWIWOPWLWGWNWHV
-      EVFVGWGWRVCZWMWTPXBWIWSPWLWGWRWHVEVFVGABCHGJKLMPPRSSUAUSUPUIUNV
-      HACEFNOLSTSUBUDUFAEIJKUHVIZUIUJUIULUMVKACEWQLSUBUDWQVLZXCUIVSAO
-      TSKVAZVBZNSTKVAZVBZWJTJVBZVJWJRVAVAZPWLVAXFXHPWKXIRVAVAZUAXIVJW
-      JRVAZVAZWPPADIRPXHMXFWJUAWJXIUCUEUGAEIJKUHVMZUKACDSJACDEIJKUBUC
-      UHVNZUIVOZACDTJXOUJVOUNASTLVAWJXIMVANXGACEIJKLMSTUBUDUEUHUIUJVP
-      ULVOXPATSLVAXIWJMVAOXEACEIJKLMTSUBUDUEUHUJUIVPUMVOVQAWOXJPWLACE
-      FIJKLNORSTSUBUDUFUGUHUIUJUIULUMVRVFAPXFQXLVAXMUQAQXKXFXLURVTWAW
-      BAWTWJIVDVBZVBZPWLVAPAWSXRPWLACEWQIJKXQSUBXDXQVLZUHUIWCVFADIRXQ
-      PMUAWJUCUEXSXNUKUGXPUNWDWEWF $.
-  $}
-
-  ${
-    $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 ) $.
     upcic.j $e |- J = ( Hom ` E ) $.
     upcic.o $e |- O = ( comp ` E ) $.
     upcic.f $e |- ( ph -> F ( D Func E ) G ) $.
-    upcic.z $e |- ( ph -> Z e. C ) $.
     upcic.x $e |- ( ph -> X e. B ) $.
+    upcic.y $e |- ( ph -> Y e. B ) $.
+    upcic.z $e |- ( ph -> Z e. C ) $.
     upcic.m $e |- ( ph -> M e. ( Z J ( F ` X ) ) ) $.
     upcic.1 $e |- ( ph -> A. w e. B A. f e. ( Z J ( F ` w ) ) E! k e. ( X H w )
            f = ( ( ( X G w ) ` 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. v e. B A. g e. ( Z J ( F ` v ) ) E! l e. ( Y H v )
+
+    ${
+      $d .x. p $.  $d B p w $.  $d D p $.  $d F f p k w $.  $d G f p k w $.
+      $d H f p k w $.  $d J f p w $.  $d K p $.  $d L p $.  $d M f p k w $.
+      $d O f p k w $.  $d X f p k w $.  $d Y p $.  $d Z f p k w $.
+      upciclem2.od $e |- .x. = ( comp ` D ) $.
+      upciclem2.k $e |- ( ph -> K e. ( X H Y ) ) $.
+      upciclem2.l $e |- ( ph -> L e. ( Y H X ) ) $.
+      upciclem2.mn $e |- ( ph -> M = ( ( ( Y G X ) ` L )
+                             ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) $.
+      upciclem2.nm $e |- ( ph -> N = ( ( ( X G Y ) ` K )
+                             ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) $.
+      $( Lemma for ~ upcic .  (Contributed by Zhi Wang, 17-Sep-2025.) $)
+      upciclem2 $p |- ( ph -> ( L ( <. X , Y >. .x. X ) K )
+                          = ( ( Id ` D ) ` X ) ) $=
+        ( vp cv co cfv wceq ccid fveq2 oveq1d eqeq2d upciclem1 funcrcl2 catcocl
+        cop catidcl funcrcl3 funcf1 ffvelcdmd funcf2 catass funcco oveq2d eqtrd
+        eqid 3eqtr4rd funcid catlid eqtr2d reu2eqd ) APURUSZSSKUTZVAZPUASJVAZVJ
+        ZWIRUTZUTZVBPONSTVJSFUTUTZWGVAZPWKUTZVBPSEVCVAZVAZWGVAZPWKUTZVBURSSLUTW
+        MWQWFWMVBZWLWOPWTWHWNPWKWFWMWGVDVEVFWFWQVBZWLWSPXAWHWRPWKWFWQWGVDVEVFAB
+        CHGJKLMPPRSSUAURULUHUKVGACEFNOLSTSUBUDUMAEIJKUGVHZUHUIUHUNUOVIACEWPLSUB
+        UDWPVTZXBUHVKAOTSKUTZVAZNSTKUTZVAZWITJVAZVJWIRUTUTZPWKUTXEXGPWJXHRUTUTZ
+        UAXHVJWIRUTZUTZWOPADIRPXGMXEWIUAWIXHUCUEUFAEIJKUGVLZUJACDSJACDEIJKUBUCU
+        GVMZUHVNZACDTJXNUIVNUKASTLUTWIXHMUTNXFACEIJKLMSTUBUDUEUGUHUIVOUNVNXOATS
+        LUTXHWIMUTOXDACEIJKLMTSUBUDUEUGUIUHVOUOVNVPAWNXIPWKACEFIJKLNORSTSUBUDUM
+        UFUGUHUIUHUNUOVQVEAPXEQXKUTXLUPAQXJXEXKUQVRVSWAAWSWIIVCVAZVAZPWKUTPAWRX
+        QPWKACEWPIJKXPSUBXCXPVTZUGUHWBVEADIRXPPMUAWIUCUEXRXMUJUFXOUKWCWDWE $.
+    $}
+
+    ${
+      $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.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 ) ) $.
-    $( A universal property defines an object up to isomorphism given its
-       existence.  (Contributed by Zhi Wang, 16-Sep-2025.) $)
-    upcic $p |- ( ph -> X ( ~=c ` D ) Y ) $=
-      ( vp vq cv co cfv cop wceq ccic wbr wreu wrex upciclem1 reurex wcel simpl
-      syl 3syl ciso eqid cfunc ad2antrr funcrcl2 cco ccid simplrl simprl simprr
-      wa wral simplrr upciclem2 isisod brcici rexlimddv ) APUOUQZRSLURUSOTRKUSZ
-      UTZSKUSZQURURVAZRSFVBUSVCZUORSMURZAWMUOWOVDWMUOWOVEABDIGKLMNOPQRSTUOUKULU
-      MVFWMUOWOVGVJAWIWOVHZWMWBZWBZOUPUQZSRLURUSPTWLUTZWJQURURVAZWNUPSRMURZWRAX
-      AUPXBVDXAUPXBVEAWQVIACDUAHKLMNPOQSRTUPUNUIUJVFXAUPXBVGVKWRWSXBVHZXAWBZWBZ
-      DFWIFVLUSZRSXFVMZUBXEFJKLAKLFJVNURVCWQXDUGVOZVPZARDVHWQXDUIVOZASDVHWQXDUL
-      VOZXEDFFVQUSZFVRUSZWIWSMXFRSUBUDXLVMZXGXMVMXIXJXKAWPWMXDVSZWRXCXAVTZXEBDE
-      FXLGIJKLMNWIWSOPQRSTUBUCUDUEXNUFXHXJXKATEVHWQXDUHVOZXOXPAOTWJNURVHWQXDUJV
-      OZAPTWLNURVHWQXDUMVOZAGUQIUQRBUQZLURUSOWKXTKUSZQURURVAIRXTMURVDGTYANURWCB
-      DWCWQXDUKVOWRXCXAWAZAWPWMXDWDZWEXECDEFXLHUAJKLMNWSWIPOQSRTUBUCUDUEXNUFXHX
-      KXJXQXPXOXSXRAHUQUAUQSCUQZLURUSPWTYDKUSZQURURVAUASYDMURVDHTYENURWCCDWCWQX
-      DUNVOYCYBWEWFWGWHWH $.
+      $( 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 $.
+    $}
   $}