Add dvbsssg to iset.mm

This is dvbsss from set.mm with additional conditions that we are
evaluating _D within its domain (the set.mm proof uses excluded middle
to combine the within-domain and outside-domain cases). The proof is
easy from dvbss .

Author: jkingdon

iset.mm

@@ -136589,6 +136589,18 @@ S C_ ( P ( ball ` D ) T ) ) $=
       VCUPUQURBVCVGVGMUSUTVA $.
   $}
 
+  ${
+    $d f s x z w F $.  $d s w S $.
+    $( The set of differentiable points is a subset of the ambient topology.
+       (Contributed by Mario Carneiro, 18-Mar-2015.)  (Revised by Jim Kingdon,
+       28-Jun-2023.) $)
+    dvbsssg $p |- ( ( S C_ CC /\ F e. ( CC ^pm S ) )
+        -> dom ( S _D F ) C_ S ) $=
+      ( cc wss cpm co wcel wa cdv cdm simpl wf elpmi simpld adantl simprd dvbss
+      sstrd ) ACDZBCAEFGZHZABIFJBJZAUAUBABSTKTUBCBLZSTUCUBADZCABMZNOTUDSTUCUDUE
+      POZQUFR $.
+  $}
+
 
 $(
 ###############################################################################

mmil.raw.html

@@ -10254,6 +10254,11 @@
   <td>changes the notation for the topology on the complex numbers</td>
 </tr>
 
+<tr>
+  <td>dvbsss</td>
+  <td>~ dvbsssg</td>
+</tr>
+
 </TABLE>
 
 <HR NOSHADE SIZE=1><A NAME="bib"></A><B><FONT