[prove] upciclem2

Author: zwang123

set.mm

@@ -835536,6 +835536,11 @@ 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 ) $.
@@ -835550,16 +835555,30 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
     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 )
+    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, XX-Sep-2025.) $)
+    $( 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 $.
   $}
 
   ${