[move and fix] upeu2lem and description and line length

Author: zwang123

set.mm

@@ -835492,6 +835492,40 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
       KWDUOUNUPUQUSABCEUDFHIVKJKVFLMQORSTPDCUTUIZVEJNVADWEVJKNVAVBVC $.
   $}
 
+  ${
+    $d .x. k $.  $d C k $.  $d F k $.  $d G k $.  $d H k $.  $d X k $.
+    $d Y k $.  $d Z k $.  $d k ph $.
+    upeu2lem.b $e |- B = ( Base ` C ) $.
+    upeu2lem.h $e |- H = ( Hom ` C ) $.
+    upeu2lem.o $e |- .x. = ( comp ` C ) $.
+    upeu2lem.i $e |- I = ( Iso ` C ) $.
+    upeu2lem.c $e |- ( ph -> C e. Cat ) $.
+    upeu2lem.x $e |- ( ph -> X e. B ) $.
+    upeu2lem.y $e |- ( ph -> Y e. B ) $.
+    upeu2lem.z $e |- ( ph -> Z e. B ) $.
+    upeu2lem.f $e |- ( ph -> F e. ( X I Y ) ) $.
+    upeu2lem.g $e |- ( ph -> G e. ( X H Z ) ) $.
+    $( Lemma for ~ upeu2 .  There exists a unique morphism from ` Y ` to ` Z `
+       that commutes if ` F : X --> Y ` is an isomorphism.  (Contributed by Zhi
+       Wang, 20-Sep-2025.) $)
+    upeu2lem $p |- ( ph -> E! k e. ( Y H Z )
+            G = ( k ( <. X , Y >. .x. Z ) F ) ) $=
+      ( cinv cfv co wcel cv wceq wb wral wreu isohom eqid invf ffvelcdmd sseldd
+      cop catcocl wa oveq1 adantl ccid adantr simpr catass cco oveqi isocoinvid
+      oveq2d catrid 3eqtrd eqtr2d invcoisoid impbida ralrimiva reu6i syl2anc
+      ccat ) AGFJKCUCUDZUEZUDZKJUQZLDUEZUEZKLHUEZUFGEUGZFJKUQZLDUEZUEZUHZWFWDUH
+      ZUIZEWEUJWJEWEUKABCDWAGHKJLMNOQSRTAKJIUEZKJHUEZWAABCHIKJMNPQSRULAJKIUEZWM
+      FVTABCIVSJKMVSUMZQRSPUNUAUOUPZUBURAWLEWEAWFWEUFZUSZWJWKWSWJUSWDWIWAWCUEZW
+      FWJWDWTUHWSGWIWAWCUTVAWSWTWFUHWJWSWTWFFWAWBKDUEZUEZKKUQLDUEZUEWFKCVBUDZUD
+      ZXCUEWFWSBCDWAFHWFLKJKMNOACVRUFWRQVCZAKBUFWRSVCZAJBUFWRRVCZXGAWAWNUFWRWQV
+      CZAFJKHUEZUFWRAWOXJFABCHIJKMNPQRSULUAUPVCZALBUFWRTVCZAWRVDZVEWSXBXEWFXCWS
+      BCXDFIVSJKXAMPWPXFXHXGAFWOUFWRUAVCZXDUMZDCVFUDZWBKOVGVHVIWSBCDXDWFHKLMNXO
+      XFXGOXLXMVJVKVCVLWSWKUSWIWDFWHUEZGWKWIXQUHWSWFWDFWHUTVAWSXQGUHWKWSXQGWAFW
+      GJDUEZUEZJJUQLDUEZUEGJXDUDZXTUEGWSBCDFWAHGLJKJMNOXFXHXGXHXKXIXLAGJLHUEUFW
+      RUBVCZVEWSXSYAGXTWSBCXDFIVSJKXRMPWPXFXHXGXNXODXPWGJOVGVMVIWSBCDXDGHJLMNXO
+      XFXHOXLYBVJVKVCVLVNVOWJEWEWDVPVQ $.
+  $}
+
 
 $(
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
@@ -835566,37 +835600,6 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
       OVFUJUTUPVAVBVC $.
   $}
 
-  ${
-    $d .x. k $.  $d C k $.  $d F k $.  $d G k $.  $d H k $.  $d X k $.
-    $d Y k $.  $d Z k $.  $d k ph $.
-    upeu2lem.b $e |- B = ( Base ` C ) $.
-    upeu2lem.h $e |- H = ( Hom ` C ) $.
-    upeu2lem.o $e |- .x. = ( comp ` C ) $.
-    upeu2lem.i $e |- I = ( Iso ` C ) $.
-    upeu2lem.c $e |- ( ph -> C e. Cat ) $.
-    upeu2lem.x $e |- ( ph -> X e. B ) $.
-    upeu2lem.y $e |- ( ph -> Y e. B ) $.
-    upeu2lem.z $e |- ( ph -> Z e. B ) $.
-    upeu2lem.f $e |- ( ph -> F e. ( X I Y ) ) $.
-    upeu2lem.g $e |- ( ph -> G e. ( X H Z ) ) $.
-    $( Lemma for ~ upeu2 .  (Contributed by Zhi Wang, 20-Sep-2025.) $)
-    upeu2lem $p |- ( ph -> E! k e. ( Y H Z ) G = ( k ( <. X , Y >. .x. Z ) F ) ) $=
-      ( cinv cfv co wcel cv wceq wb wral wreu isohom eqid invf ffvelcdmd sseldd
-      cop catcocl wa oveq1 adantl ccid adantr simpr catass cco oveqi isocoinvid
-      oveq2d catrid 3eqtrd eqtr2d invcoisoid impbida ralrimiva reu6i syl2anc
-      ccat ) AGFJKCUCUDZUEZUDZKJUQZLDUEZUEZKLHUEZUFGEUGZFJKUQZLDUEZUEZUHZWFWDUH
-      ZUIZEWEUJWJEWEUKABCDWAGHKJLMNOQSRTAKJIUEZKJHUEZWAABCHIKJMNPQSRULAJKIUEZWM
-      FVTABCIVSJKMVSUMZQRSPUNUAUOUPZUBURAWLEWEAWFWEUFZUSZWJWKWSWJUSWDWIWAWCUEZW
-      FWJWDWTUHWSGWIWAWCUTVAWSWTWFUHWJWSWTWFFWAWBKDUEZUEZKKUQLDUEZUEWFKCVBUDZUD
-      ZXCUEWFWSBCDWAFHWFLKJKMNOACVRUFWRQVCZAKBUFWRSVCZAJBUFWRRVCZXGAWAWNUFWRWQV
-      CZAFJKHUEZUFWRAWOXJFABCHIJKMNPQRSULUAUPVCZALBUFWRTVCZAWRVDZVEWSXBXEWFXCWS
-      BCXDFIVSJKXAMPWPXFXHXGAFWOUFWRUAVCZXDUMZDCVFUDZWBKOVGVHVIWSBCDXDWFHKLMNXO
-      XFXGOXLXMVJVKVCVLWSWKUSWIWDFWHUEZGWKWIXQUHWSWFWDFWHUTVAWSXQGUHWKWSXQGWAFW
-      GJDUEZUEZJJUQLDUEZUEGJXDUDZXTUEGWSBCDFWAHGLJKJMNOXFXHXGXHXKXIXLAGJLHUEUFW
-      RUBVCZVEWSXSYAGXTWSBCXDFIVSJKXRMPWPXFXHXGXNXODXPWGJOVGVMVIWSBCDXDGHJLMNXO
-      XFXHOXLYBVJVKVCVLVNVOWJEWEWDVPVQ $.
-  $}
-
   ${
     upcic.b $e |- B = ( Base ` D ) $.
     upcic.c $e |- C = ( Base ` E ) $.