[fix] functor

Author: zwang123

set.mm

@@ -835516,21 +835516,23 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
     $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 ) ) $.
+           E! k e. ( X H y )
+           n = ( ( ( X G y ) ` 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! 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 $.
+                            N = ( ( ( X G Y ) ` l )
+                            ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) $=
+      ( co vm cv cfv cop wceq wreu eqeq1 reubidv wral fveq2 oveq2d oveq2 fveq1d
+      eqidd oveq123d eqeq2d reueqdv bitrd raleqbidv oveq1d cbvreuvw bitri sylib
+      rspcdva ) AKDUBZMNGTZUCZJOMFUCUDZNFUCZLTZTZUEZDMNHTZUFZKPUBZVFUCZJVJTZUEZ
+      PVMUFZAEUBZVKUEZDVMUFZVNEOVIITZKVTKUEWAVLDVMVTKVKUGUHAVTVEMBUBZGTZUCZJVHW
+      DFUCZLTZTZUEZDMWDHTZUFZEOWGITZUIWBEWCUIBCNWDNUEZWLWBEWMWCWNWGVIOIWDNFUJZU
+      KWNWLWADWKUFWBWNWJWADWKWNWIVKVTWNWFVGJJWHVJWNWGVIVHLWOUKWNVEWEVFWDNMGULUM
+      WNJUNUOUPUHWNWADWKVMWDNMHULUQURUSQRVDSVDVNKUAUBZVFUCZJVJTZUEZUAVMUFVSVLWS
+      DUAVMVEWPUEZVKWRKWTVGWQJVJVEWPVFUJUTUPVAWSVRUAPVMWPVOUEZWRVQKXAWQVPJVJWPV
+      OVFUJUTUPVAVBVC $.
   $}
 
   ${
@@ -835549,10 +835551,10 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
     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 = ( ( G ` k ) ( <. Z , ( F ` X ) >. O ( F ` w ) ) M ) ) $.
-    upciclem2.mn $e |- ( ph -> M = ( ( G ` L )
+           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 = ( ( G ` K )
+    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.) $)
     upciclem2 $p |- ( ph -> ( L ( <. X , Y >. .x. X ) K )
@@ -835578,27 +835580,27 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
     upcic.x $e |- ( ph -> X e. B ) $.
     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 = ( ( G ` k ) ( <. Z , ( F ` X ) >. O ( F ` w ) ) M ) ) $.
+           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 )
-            g = ( ( G ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) ) $.
+           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 cfv cop co wceq ccic wbr wreu wrex upciclem1 reurex wcel simpl
+      ( 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 ) APUOUQZLUROTRKURZUSZS
-      KURZQUTUTVAZRSFVBURVCZUORSMUTZAWMUOWOVDWMUOWOVEABDIGKLMNOPQRSTUOUKULUMVFW
-      MUOWOVGVJAWIWOVHZWMWBZWBZOUPUQZLURPTWLUSZWJQUTUTVAZWNUPSRMUTZWRAXAUPXBVDX
-      AUPXBVEAWQVIACDUAHKLMNPOQSRTUPUNUIUJVFXAUPXBVGVKWRWSXBVHZXAWBZWBZDFWIFVLU
-      RZRSXFVMZUBXEFJKLAKLFJVNUTVCWQXDUGVOZVPZARDVHWQXDUIVOZASDVHWQXDULVOZXEDFF
-      VQURZFVRURZWIWSMXFRSUBUDXLVMZXGXMVMXIXJXKAWPWMXDVSZWRXCXAVTZXEBDEFXLGIJKL
-      MNWIWSOPQRSTUBUCUDUEXNUFXHXJXKATEVHWQXDUHVOZXOXPAOTWJNUTVHWQXDUJVOZAPTWLN
-      UTVHWQXDUMVOZAGUQIUQLUROWKBUQZKURZQUTUTVAIRXTMUTVDGTYANUTWCBDWCWQXDUKVOWR
-      XCXAWAZAWPWMXDWDZWEXECDEFXLHUAJKLMNWSWIPOQSRTUBUCUDUEXNUFXHXKXJXQXPXOXSXR
-      AHUQUAUQLURPWTCUQZKURZQUTUTVAUASYDMUTVDHTYENUTWCCDWCWQXDUNVOYCYBWEWFWGWHW
-      H $.
+      wa wral simplrr upciclem2 isisod brcici rexlimddv ) APUOUQZRSLURUSOTRKUSZ
+      UTZSKUSZQURURVAZRSFVBUSVCZUORSMURZAWMUOWOVDWMUOWOVEABDIGKLMNOPQRSTUOUKULU
+      MVFWMUOWOVGVJAWIWOVHZWMWBZWBZOUPUQZSRLURUSPTWLUTZWJQURURVAZWNUPSRMURZWRAX
+      AUPXBVDXAUPXBVEAWQVIACDUAHKLMNPOQSRTUPUNUIUJVFXAUPXBVGVKWRWSXBVHZXAWBZWBZ
+      DFWIFVLUSZRSXFVMZUBXEFJKLAKLFJVNURVCWQXDUGVOZVPZARDVHWQXDUIVOZASDVHWQXDUL
+      VOZXEDFFVQUSZFVRUSZWIWSMXFRSUBUDXLVMZXGXMVMXIXJXKAWPWMXDVSZWRXCXAVTZXEBDE
+      FXLGIJKLMNWIWSOPQRSTUBUCUDUEXNUFXHXJXKATEVHWQXDUHVOZXOXPAOTWJNURVHWQXDUJV
+      OZAPTWLNURVHWQXDUMVOZAGUQIUQRBUQZLURUSOWKXTKUSZQURURVAIRXTMURVDGTYANURWCB
+      DWCWQXDUKVOWRXCXAWAZAWPWMXDWDZWEXECDEFXLHUAJKLMNWSWIPOQSRTUBUCUDUEXNUFXHX
+      KXJXQXPXOXSXRAHUQUAUQSCUQZLURUSPWTYDKUSZQURURVAUASYDMURVDHTYENURWCCDWCWQX
+      DUNVOYCYBWEWFWGWHWH $.
   $}