Merge branch 'develop' into upcic

Author: zwang123

set.mm

@@ -57567,6 +57567,27 @@ of the relation (see ~ op1stb ).  (Contributed by NM, 28-Jul-2004.) $)
       UDUBUCQUAMAUBUCUANABCOPRST $.
   $}
 
+  ${
+    $d x y A $.
+    $( Upper bound for the range of a restricted class of ordered pairs.
+       (Contributed by Eric Schmidt, 16-Sep-2025.) $)
+    rnopabss $p |- ran { <. x , y >. | ( y e. A /\ ph ) } C_ A $=
+      ( cv wcel wa copab crn wex cab rnopab 19.42v abbii ssab2 eqsstri ) CEDFZA
+      GZBCHIRBJZCKZDRBCLTQABJZGZCKDSUBCQABMNUACDOPP $.
+  $}
+
+  ${
+    $d x y A $.
+    $( The range of a restricted class of ordered pairs.  (Contributed by Eric
+       Schmidt, 16-Sep-2025.) $)
+    rnopab3 $p |- ( A. y e. A E. x ph <->
+               ran { <. x , y >. | ( y e. A /\ ph ) } = A ) $=
+      ( wex wral cv wcel wi wal wa wb copab crn wceq df-ral pm4.71 albii rnopab
+      cab 19.42v abbii eqtri eqeq1i eqcom eqabb 3bitr2ri 3bitri ) ABEZCDFCGDHZU
+      IIZCJUJUJUIKZLZCJZUJAKZBCMNZDOZUICDPUKUMCUJUIQRUQULCTZDODUROUNUPURDUPUOBE
+      ZCTURUOBCSUSULCUJABUAUBUCUDDURUEULCDUFUGUH $.
+  $}
+
   ${
     $d y z A $.  $d y z B $.  $d x y z C $.
     rnmpt.1 $e |- F = ( x e. A |-> B ) $.