[add] funcrcl2, funcrcl3; [update] upcic, upciclem2

Author: zwang123

set.mm

@@ -835476,6 +835476,21 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
 $)
 
+  ${
+    funcrcl2.f $e |- ( ph -> F ( D Func E ) G ) $.
+    $( 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 $.
+
+    $( 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 $.
+  $}
+
   ${
     $d B x y z $.  $d F x y z $.  $d G x y z $.  $d H x y z $.  $d J x y z $.
     $( A utility theorem for proving equivalence of "is a functor".
@@ -835533,11 +835548,13 @@ 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 )
+            f = ( ( G ` k ) ( <. Z , ( F ` X ) >. O ( F ` w ) ) M ) ) $.
     upciclem2.mn $e |- ( ph -> M = ( ( G ` L )
                                ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) $.
     upciclem2.nm $e |- ( ph -> N = ( ( G ` K )
                                ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) $.
-    $( Lemma for ~ upcic .  (Contributed by Zhi Wang, 16-Sep-2025.) $)
+    $( Lemma for ~ upcic .  (Contributed by Zhi Wang, XX-Sep-2025.) $)
     upciclem2 $p |- ( ph -> ( L ( <. X , Y >. .x. X ) K )
                           = ( ( Id ` D ) ` X ) ) $=
       (  ) ? $.
@@ -835571,16 +835588,18 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
     upcic $p |- ( ph -> X ( ~=c ` D ) Y ) $=
       ( vp vq cv cfv cop co wceq ccic wbr wreu wrex upciclem1 reurex wcel simpl
       syl wa 3syl ciso eqid cfunc ccat simpll df-br sylib funcrcl 4syl ad2antrr
-      cco ccid simplrl simprl simprr simplrr upciclem2 isisod brcici rexlimddv
-      ) APUOUQZLUROTRKURZUSSKURZQUTUTVAZRSFVBURVCZUORSMUTZAWPUOWRVDWPUOWRVEABDI
-      GKLMNOPQRSTUOUKULUMVFWPUOWRVGVJAWMWRVHZWPVKZVKZOUPUQZLURPTWOUSWNQUTUTVAZW
-      QUPSRMUTZXAAXCUPXDVDXCUPXDVEAWTVIACDUAHKLMNPOQSRTUPUNUIUJVFXCUPXDVGVLXAXB
-      XDVHZXCVKZVKZDFWMFVMURZRSXHVNZUBXGAKLUSZFJVOUTZVHZFVPVHZJVPVHZVKXMAWTXFVQ
-      AKLXKVCZXLUGKLXKVRVSFJXJVTXMXNVIWAZARDVHWTXFUIWBZASDVHWTXFULWBZXGDFFWCURZ
-      FWDURZWMXBMXHRSUBUDXSVNZXIXTVNXPXQXRAWSWPXFWEZXAXEXCWFZXGDEFXSJKLMNWMXBOP
-      QRSTUBUCUDUEYAUFAXOWTXFUGWBZXQXRATEVHWTXFUHWBZYBYCAOTWNNUTVHWTXFUJWBZAPTW
-      ONUTVHWTXFUMWBZXAXEXCWGZAWSWPXFWHZWIXGDEFXSJKLMNXBWMPOQSRTUBUCUDUEYAUFYDX
-      RXQYEYCYBYGYFYIYHWIWJWKWLWL $.
+      ccid simplrl simprl wral simprr simplrr upciclem2 isisod brcici rexlimddv
+      cco ) APUOUQZLUROTRKURZUSZSKURZQUTUTVAZRSFVBURVCZUORSMUTZAWRUOWTVDWRUOWTV
+      EABDIGKLMNOPQRSTUOUKULUMVFWRUOWTVGVJAWNWTVHZWRVKZVKZOUPUQZLURPTWQUSZWOQUT
+      UTVAZWSUPSRMUTZXCAXFUPXGVDXFUPXGVEAXBVIACDUAHKLMNPOQSRTUPUNUIUJVFXFUPXGVG
+      VLXCXDXGVHZXFVKZVKZDFWNFVMURZRSXKVNZUBXJAKLUSZFJVOUTZVHZFVPVHZJVPVHZVKXPA
+      XBXIVQAKLXNVCZXOUGKLXNVRVSFJXMVTXPXQVIWAZARDVHXBXIUIWBZASDVHXBXIULWBZXJDF
+      FWMURZFWCURZWNXDMXKRSUBUDYBVNZXLYCVNXSXTYAAXAWRXIWDZXCXHXFWEZXJBDEFYBGIJK
+      LMNWNXDOPQRSTUBUCUDUEYDUFAXRXBXIUGWBZXTYAATEVHXBXIUHWBZYEYFAOTWONUTVHXBXI
+      UJWBZAPTWQNUTVHXBXIUMWBZAGUQIUQLUROWPBUQZKURZQUTUTVAIRYKMUTVDGTYLNUTWFBDW
+      FXBXIUKWBXCXHXFWGZAXAWRXIWHZWIXJCDEFYBHUAJKLMNXDWNPOQSRTUBUCUDUEYDUFYGYAX
+      TYHYFYEYJYIAHUQUAUQLURPXECUQZKURZQUTUTVAUASYOMUTVDHTYPNUTWFCDWFXBXIUNWBYN
+      YMWIWJWKWLWL $.
   $}