Add new theorems related to restricted class abstraction, mappings, and measurable functions

set.mm

@@ -698971,6 +698971,19 @@ not even needed (it can be any class).  (Contributed by Glauco
       ZUEUIDABCPQUHBDERUMUGBDOZULKUHBDOUJUKUNULBDCEFSTUGABDUAUHBDUBUCUD $.
   $}
 
+  ${
+    ssrabdf.1 $e |- F/_ x A $.
+    ssrabdf.2 $e |- F/_ x B $.
+    ssrabdf.3 $e |- F/ x ph $.
+    ssrabdf.4 $e |- ( ph -> B C_ A ) $.
+    ssrabdf.5 $e |- ( ( ph /\ x e. B ) -> ps ) $.
+    $( Subclass of a restricted class abstraction (deduction form).
+       (Contributed by Glauco Siliprandi, 5-Jan-2025.) $)
+    ssrabdf $p |- ( ph -> B C_ { x e. A | ps } ) $=
+      ( wss wral crab ralrimia ssrabf sylanbrc ) AEDKBCELEBCDMKIABCEHJNBCDEGFOP
+      $.
+  $}
+
   ${
     $d A x $.  $d B x $.
     $( Membership in indexed intersection.  See ~ eliincex for a counterexample
@@ -701137,6 +701150,53 @@ not even needed (it can be any class).  (Contributed by Glauco
       ( mpteq2da ) ABCDEFGH $.
   $}
 
+  ${
+    dmmpt1.x $e |- F/ x ph $.
+    dmmpt1.1 $e |- F/_ x B $.
+    dmmpt1.c $e |- ( ( ph /\ x e. B ) -> C e. V ) $.
+    $( The domain of the mapping operation, deduction form.  (Contributed by
+       Glauco Siliprandi, 5-Jan-2025.) $)
+    dmmpt1 $p |- ( ph -> dom ( x e. B |-> C ) = B ) $=
+      ( cmpt eqid dmmptdff ) ABBCDIZCDEFGLJHK $.
+  $}
+
+  ${
+    $d A y $.  $d B y $.  $d C y $.  $d x y $.
+    fmptff.1 $e |- F/_ x A $.
+    fmptff.2 $e |- F/_ x B $.
+    fmptff.3 $e |- F = ( x e. A |-> C ) $.
+    $( Functionality of the mapping operation.  (Contributed by Glauco
+       Siliprandi, 5-Jan-2025.) $)
+    fmptff $p |- ( A. x e. A C e. B <-> F : A --> B ) $=
+      ( vy wcel wral cv csb wf nfcv nfv nfcsb1v nfel weq cmpt eleq1d eqtri fmpt
+      csbeq1a cbvralfw cbvmptf bitri ) DCJZABKAILZDMZCJZIBKBCENUHUKAIBFIBOZUHIP
+      AUJCAUIDQZGRAISDUJCAUIDUDZUAUEIBCUJEEABDTIBUJTHAIBDUJFULIDOUMUNUFUBUCUG
+      $.
+  $}
+
+  ${
+    fvmptelcdmf.a $e |- F/_ x A $.
+    fvmptelcdmf.c $e |- F/_ x C $.
+    fvmptelcdmf.f $e |- ( ph -> ( x e. A |-> B ) : A --> C ) $.
+    $( The value of a function at a point of its domain belongs to its
+       codomain.  (Contributed by Glauco Siliprandi, 5-Jan-2025.) $)
+    fvmptelcdmf $p |- ( ( ph /\ x e. A ) -> B e. C ) $=
+      ( wcel cmpt wf wral eqid fmptff sylibr r19.21bi ) ADEIZBCACEBCDJZKQBCLHBC
+      EDRFGRMNOP $.
+  $}
+
+  ${
+    fmptdff.1 $e |- F/ x ph $.
+    fmptdff.2 $e |- F/_ x A $.
+    fmptdff.3 $e |- F/_ x C $.
+    fmptdff.4 $e |- ( ( ph /\ x e. A ) -> B e. C ) $.
+    fmptdff.5 $e |- F = ( x e. A |-> B ) $.
+    $( A version of ~ fmptd using bound-variable hypothesis instead of a
+       distinct variable condition for ` ph ` .  (Contributed by Glauco
+       Siliprandi, 5-Jan-2025.) $)
+    fmptdff $p |- ( ph -> F : A --> C ) $=
+      ( wcel wral wf ralrimia fmptff sylib ) ADELZBCMCEFNARBCGJOBCEDFHIKPQ $.
+  $}
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -753519,6 +753579,19 @@ is the step (i) of the proof of Proposition 121E (d) of [Fremlin1]
       KUNDUNDJUAUBUCUGABCDULEFGHIJULUHTAUDUEKUIUJ $.
   $}
 
+  ${
+    smffmptf.x $e |- F/ x ph $.
+    smffmptf.a $e |- F/_ x A $.
+    smffmptf.s $e |- ( ph -> S e. SAlg ) $.
+    smffmptf.b $e |- ( ( ph /\ x e. A ) -> B e. V ) $.
+    smffmptf.m $e |- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) ) $.
+    $( A function measurable w.r.t. to a sigma-algebra, is actually a function.
+       (Contributed by Glauco Siliprandi, 5-Jan-2025.) $)
+    smffmptf $p |- ( ph -> ( x e. A |-> B ) : A --> RR ) $=
+      ( cr cmpt wf cdm eqid smff dmmpt1 eqcomd feq2d mpbird ) ACLBCDMZNUBOZLUBN
+      AUCEUBIKUCPQACUCLUBAUCCABCDFGHJRSTUA $.
+  $}
+
   ${
     $d A x $.
     smffmpt.x $e |- F/ x ph $.
@@ -753528,8 +753601,7 @@ is the step (i) of the proof of Proposition 121E (d) of [Fremlin1]
     $( A function measurable w.r.t. to a sigma-algebra, is actually a function.
        (Contributed by Glauco Siliprandi, 23-Oct-2021.) $)
     smffmpt $p |- ( ph -> ( x e. A |-> B ) : A --> RR ) $=
-      ( cr cmpt wf cdm eqid smff dmmptdf eqcomd feq2d mpbird ) ACKBCDLZMUANZKUA
-      MAUBEUAHJUBOPACUBKUAAUBCABUACDFGUAOIQRST $.
+      ( nfcv smffmptf ) ABCDEFGBCKHIJL $.
   $}
 
   ${
@@ -754778,6 +754850,122 @@ that every function in the sequence can have a different (partial)
       KUEUF $.
   $}
 
+  ${
+    $d C x $.
+    smfdmmblpimne.1 $e |- F/ x ph $.
+    smfdmmblpimne.2 $e |- F/_ x A $.
+    smfdmmblpimne.3 $e |- ( ph -> S e. SAlg ) $.
+    smfdmmblpimne.4 $e |- ( ph -> A e. S ) $.
+    smfdmmblpimne.5 $e |- ( ( ph /\ x e. A ) -> B e. RR ) $.
+    smfdmmblpimne.6 $e |- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) ) $.
+    smfdmmblpimne.7 $e |- ( ph -> C e. RR ) $.
+    smfdmmblpimne.8 $e |- D = { x e. A | B =/= C } $.
+    $( If a measurable function w.r.t. to a sigma-algebra has domain in the
+       sigma-algebra, the set of elements that are not mapped to a given real,
+       is in the sigma-algebra (Contributed by Glauco Siliprandi,
+       5-Jan-2025.) $)
+    smfdmmblpimne $p |- ( ph -> D e. S ) $=
+      ( clt wbr crab wcel rexrd cun wne cv wa cxr adantr pimxrneun eqtrid crest
+      co salrestss cr smfpimltxrmptf sseldd smfpimgtxrmptf saluncld eqeltrd ) A
+      FDEPQBCRZEDPQBCRZUAZGAFDEUBBCRUTOABCDEHABUCCSZUDDLTAEUESVAAENTZUFUGUHAGUR
+      USJAGCUIUJZGURAGCJKUKZABCDEGULHIJLMVBUMUNAVCGUSVDABCDGEULHIJLMVBUOUNUPUQ
+      $.
+  $}
+
+  ${
+    $d A y $.  $d B y $.  $d C y $.  $d D y $.  $d V x $.  $d ph y $.
+    $d x y $.
+    smfdivdmmbl.1 $e |- F/ x ph $.
+    smfdivdmmbl.2 $e |- F/_ x B $.
+    smfdivdmmbl.3 $e |- ( ph -> S e. SAlg ) $.
+    smfdivdmmbl.4 $e |- ( ph -> A e. S ) $.
+    smfdivdmmbl.5 $e |- ( ph -> B e. S ) $.
+    smfdivdmmbl.6 $e |- ( ( ph /\ x e. B ) -> D e. W ) $.
+    smfdivdmmbl.7 $e |- ( ph -> ( x e. B |-> D ) e. ( SMblFn ` S ) ) $.
+    smfdivdmmbl.8 $e |- E = { x e. B | D =/= 0 } $.
+    $( If a functions and a sigma-measurable function have domains in the
+       sigma-algebra, the domain of the division of the two functions is in the
+       sigma-algebra.  This is the third statement of Proposition 121H of
+       [Fremlin1] p. 39 .  Note:  While the theorem in the book assumes both
+       functions are sigma-measurable, this assumption is unnecessary for the
+       part concerning their division, for the function at the numerator (it is
+       needed only for the function at the denominator).  (Contributed by
+       Glauco Siliprandi, 5-Jan-2025.) $)
+    smfdivdmmbl $p |- ( ph -> ( A i^i E ) e. S ) $=
+      ( cc0 cr nfcv smffmptf fvmptelcdmf 0red smfdmmblpimne salincld ) AFCGKLAB
+      DEQGFIJKMABDERJBRSABDEFHIJKNOTUAOAUBPUCUD $.
+  $}
+
+  ${
+    $d A x $.
+    smfpimne.p $e |- F/ x ph $.
+    smfpimne.x $e |- F/_ x F $.
+    smfpimne.s $e |- ( ph -> S e. SAlg ) $.
+    smfpimne.f $e |- ( ph -> F e. ( SMblFn ` S ) ) $.
+    smfpimne.d $e |- D = dom F $.
+    smfpimne.a $e |- ( ph -> A e. RR* ) $.
+    $( Given a function measurable w.r.t. to a sigma-algebra, the preimage of
+       reals that are different from a value in the extended reals is in the
+       subspace of sigma-algebra induced by its domain.  (Contributed by Glauco
+       Siliprandi, 5-Jan-2025.) $)
+    smfpimne $p |- ( ph -> { x e. D | ( F ` x ) =/= A } e. ( S |`t D ) ) $=
+      ( cv cfv wne crab clt wbr cun wcel crest co wa cr ffvelcdmda rexrd adantr
+      smff cxr pimxrneun smfdmss subsaluni eqid subsalsal smfpimltxr smfpimgtxr
+      saluncld eqeltrd ) ABMZFNZCOBDPUTCQRBDPZCUTQRBDPZSEDUAUBZABDUTCGAUSDTZUCU
+      TADUDUSFADEFIJKUHUEUFACUITVDLUGUJAVCVAVBADEVCVCIADEIADEFIJKUKULVCUMUNABCD
+      EFHIJKLUOABCDEFHIJKLUPUQUR $.
+  $}
+
+  ${
+    $d A x $.
+    smfpimne2.p $e |- F/ x ph $.
+    smfpimne2.x $e |- F/_ x F $.
+    smfpimne2.s $e |- ( ph -> S e. SAlg ) $.
+    smfpimne2.f $e |- ( ph -> F e. ( SMblFn ` S ) ) $.
+    smfpimne2.d $e |- D = dom F $.
+    $( Given a function measurable w.r.t. to a sigma-algebra, the preimage of
+       reals that are different from a value is in the subspace sigma-algebra
+       induced by its domain.  Notice that ` A ` is not assumed to be an
+       extended real.  (Contributed by Glauco Siliprandi, 5-Jan-2025.) $)
+    smfpimne2 $p |- ( ph -> { x e. D | ( F ` x ) =/= A } e. ( S |`t D ) ) $=
+      ( cxr wcel cfv wa nfv nfan adantr simpr wn cv crab crest co csalg csmblfn
+      wne smfpimne wss cdm nfdm nfcxfr ssrab2f a1i ssidd wceq nne cr ffvelcdmda
+      smff rexrd eqeltrrd sylan2b adantllr simpllr condan ssrabdf eqssd smfdmss
+      subsaluni eqeltrd pm2.61dan ) ACLMZBUAZFNZCUGZBDUBZEDUCUDZMAVMOBCDEFAVMBG
+      VMBPQHAEUEMVMIRAFEUFNMVMJRKAVMSUHAVMTZOZVQDVRVTVQDVQDUIVTVPBDBDFUJKBFHUKU
+      LZUMUNVTVPBDDWAWAAVSBGVSBPQVTDUOVTVNDMZOVPVMAWBVPTZVMVSWCAWBOZVOCUPZVMVOC
+      UQWDWEOVOCLWDWESWDVOLMWEWDVOADURVNFADEFIJKUTUSVARVBVCVDAVSWBWCVEVFVGVHADV
+      RMVSADEIADEFIJKVIVJRVKVL $.
+  $}
+
+  ${
+    smfdivdmmbl2.1 $e |- F/ x ph $.
+    smfdivdmmbl2.2 $e |- F/_ x F $.
+    smfdivdmmbl2.3 $e |- F/_ x G $.
+    smfdivdmmbl2.4 $e |- ( ph -> S e. SAlg ) $.
+    smfdivdmmbl2.5 $e |- ( ph -> F : A --> V ) $.
+    smfdivdmmbl2.6 $e |- ( ph -> G e. ( SMblFn ` S ) ) $.
+    smfdivdmmbl2.7 $e |- ( ph -> A e. S ) $.
+    smfdivdmmbl2.8 $e |- ( ph -> dom G e. S ) $.
+    smfdivdmmbl2.9 $e |- D = { x e. dom G | ( G ` x ) =/= 0 } $.
+    smfdivdmmbl2.10 $e |- H = ( x e. ( dom F i^i D ) |-> ( ( F ` x ) / ( G ` x
+       ) ) ) $.
+    $( If a functions and a sigma-measurable function have domains in the
+       sigma-algebra, the domain of the division of the two functions is in the
+       sigma-algebra.  This is the third statement of Proposition 121H of
+       [Fremlin1] p. 39 .  Note:  While the theorem in the book assumes both
+       functions are sigma-measurable, this assumption is unnecessary for the
+       part concerning their division, for the function at the numerator.  It
+       is required only for the function at the denominator.  (Contributed by
+       Glauco Siliprandi, 5-Jan-2025.) $)
+    smfdivdmmbl2 $p |- ( ph -> dom H e. S ) $=
+      ( cdm cin cfv cdiv nfdm cc0 wne crab nfrab1 nfcxfr nfin ovex dmmptif fdmd
+      cv co eqeltrd crest salrestss eqid smfpimne2 eqeltrid sseldd salincld ) A
+      HTFTZDUAZEBVEBUNZFUBZVFGUBZUCUOHBVDDBFKUDBDVHUEUFZBGTZUGZRVIBVJUHUIUJVGVH
+      UCUKSULAEVDDMAVDCEACIFNUMPUPAEVJUQUOZEDAEVJMQURADVKVLRABUEVJEGJLMOVJUSUTV
+      AVBVCVA $.
+  $}
+
 $( (End of Glauco Siliprandi's mathbox.) $)
 $( End $[ set-mbox-gs.mm $] $)