[change] upciclem1: var change

Author: zwang123

set.mm

@@ -835462,22 +835462,28 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
   $}
 
   ${
-    $d B y $.  $d F n y $.  $d G n y $.  $d H k n y $.  $d J n y $.
-    $d M n y $.  $d N k n $.  $d O n y $.  $d X k n y $.  $d Y k n y $.
-    $d Z n y $.  $d n ph y $.
+    $d B y $.  $d F k m $.  $d F l m $.  $d F k n y $.  $d G k m $.
+    $d G l m $.  $d G k n y $.  $d H k m $.  $d H l m $.  $d H k n y $.
+    $d J n y $.  $d M k m $.  $d M l m $.  $d M k n y $.  $d N k m $.
+    $d N l m $.  $d N k n $.  $d O k m $.  $d O l m $.  $d O k n y $.
+    $d X k m $.  $d X l m $.  $d X k n y $.  $d Y k m $.  $d Y l m $.
+    $d Y k n y $.  $d Z k m $.  $d Z l m $.  $d Z k n y $.
     upciclem1.1 $e |- ( ph -> A. y e. B A. n e. ( Z J ( F ` y ) )
             E! k e. ( X H y )
             n = ( ( G ` k ) ( <. Z , ( F ` X ) >. O ( F ` y ) ) M ) ) $.
     upciclem1.y $e |- ( ph -> Y e. B ) $.
     upciclem1.n $e |- ( ph -> N e. ( Z J ( F ` Y ) ) ) $.
     $( Lemma for ~ upcic .  (Contributed by Zhi Wang, 16-Sep-2025.) $)
-    upciclem1 $p |- ( ph -> E! k e. ( X H Y )
-                   N = ( ( G ` k ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) $=
-      ( co wceq cfv cop wreu eqeq1 reubidv wral fveq2 oveq2d oveqd eqeq2d oveq2
-      cv reueqdv bitrd raleqbidv rspcdva ) AEULZDULGUAZJOMFUAUBZNFUAZLSZSZTZDMN
-      HSZUCZKVBTZDVDUCEOUTISZKUQKTVCVFDVDUQKVBUDUEAUQURJUSBULZFUAZLSZSZTZDMVHHS
-      ZUCZEOVIISZUFVEEVGUFBCNVHNTZVNVEEVOVGVPVIUTOIVHNFUGZUHVPVNVCDVMUCVEVPVLVC
-      DVMVPVKVBUQVPVJVAURJVPVIUTUSLVQUHUIUJUEVPVCDVMVDVHNMHUKUMUNUOPQUPRUP $.
+    upciclem1 $p |- ( ph -> E! l e. ( X H Y )
+                   N = ( ( G ` l ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) $=
+      ( co vm cv cfv cop wceq wreu eqeq1 reubidv wral fveq2 oveq2d oveqd eqeq2d
+      oveq2 reueqdv bitrd raleqbidv rspcdva oveq1d cbvreuvw bitri sylib ) AKDUB
+      ZGUCZJOMFUCUDZNFUCZLTZTZUEZDMNHTZUFZKPUBZGUCZJVGTZUEZPVJUFZAEUBZVHUEZDVJU
+      FZVKEOVFITZKVQKUEVRVIDVJVQKVHUGUHAVQVDJVEBUBZFUCZLTZTZUEZDMWAHTZUFZEOWBIT
+      ZUIVSEVTUIBCNWANUEZWGVSEWHVTWIWBVFOIWANFUJZUKWIWGVRDWFUFVSWIWEVRDWFWIWDVH
+      VQWIWCVGVDJWIWBVFVELWJUKULUMUHWIVRDWFVJWANMHUNUOUPUQQRURSURVKKUAUBZGUCZJV
+      GTZUEZUAVJUFVPVIWNDUAVJVCWKUEZVHWMKWOVDWLJVGVCWKGUJUSUMUTWNVOUAPVJWKVLUEZ
+      WMVNKWPWLVMJVGWKVLGUJUSUMUTVAVB $.
   $}
 
   ${