[add] funcel1; [propose] funcel2

Author: zwang123

set.mm

@@ -835491,6 +835491,33 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
           GHZCGHZADEBCIJZKZDELZUAHZSTMFUBUDDEUANOBCUCPQR $.
   $}
 
+  ${
+    funcel1.b $e |- B = ( Base ` D ) $.
+    funcel1.f $e |- ( ph -> F ( D Func E ) G ) $.
+    funcel1.x $e |- ( ph -> X e. B ) $.
+
+    ${
+    funcel1.c $e |- C = ( Base ` E ) $.
+    $( The object part of a functor maps into the base set.
+            (Contributed by Zhi Wang,
+       17-Sep-2025.) $)
+    funcel1 $p |- ( ph -> ( F ` X ) e. C ) $=
+    ( funcf1 ffvelcdmd ) ABCHFABCDEFGILJMKN $.
+    $}
+
+    ${
+    funcel2.h $e |- H = ( Hom ` D ) $.
+    funcel2.j $e |- J = ( Hom ` E ) $.
+    funcel2.y $e |- ( ph -> Y e. B ) $.
+    funcel2.m $e |- ( ph -> M e. ( X H Y ) ) $.
+    $( The morphism part of a functor maps into the hom set.
+            (Contributed by Zhi Wang,
+       17-Sep-2025.) $)
+    funcel2 $p |- ( ph -> ( ( X G Y ) ` M ) e. ( ( F ` X ) J ( F ` Y ) ) ) $=
+    ( ) ? $.
+    $}
+  $}
+
   ${
     $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".