Some minor corrections

set.mm

@@ -71710,11 +71710,9 @@ Axiom of Replacement (unlike ~ resfunexg ).  (Contributed by NM,
     $( The function value of an indexed union is the value of one of the
        indexed functions.  (Contributed by AV, 4-Nov-2023.) $)
     fviunfun $p |- ( ( Fun U /\ J e. I /\ X e. dom ( F ` J ) )
-                     -> ( U_ i e. I ( F ` i ) ` X ) = ( ( F ` J ) ` X ) ) $=
-      ( wfun wcel cfv cdm w3a cv ciun wss wceq funeqi biimpi 3ad2ant1 fveq2
-      ssiun2s 3ad2ant2 simp3 funssfv syl3anc ) AHZEDIZFECJZKIZLBDBMZCJZNZHZUHUL
-      OZUIFULJFUHJPUFUGUMUIUFUMAULGQRSUGUFUNUIBDUKEUHUJECTUAUBUFUGUIUCFULUHUDUE
-      $.
+                     -> ( U ` X ) = ( ( F ` J ) ` X ) ) $=
+      ( wcel wfun cfv wss cdm wceq ciun fveq2 ssiun2s syl6sseqr funssfv syl3an2
+      cv ) EDHZAIECJZAKFUBLHFAJFUBJMUAUBBDBTZCJZNABDUDEUBUCECOPGQFAUBRS $.
   $}
 
   ${
@@ -506998,7 +506996,7 @@ codes is an increasing chain (with respect to inclusion).  (Contributed
 
   ${
     $d M a i $.  $d V a i $.  $d X a x y $.
-    $( The simplyfied satisfaction predicate for wff codes of height 0.
+    $( The simplified satisfaction predicate for wff codes of height 0.
        (Contributed by AV, 4-Nov-2023.) $)
     satefvfmla0 $p |- ( ( M e. V /\ X e. ( Fmla ` (/) ) )
                         -> ( M SatE X ) = { a e. ( M ^m _om ) |
@@ -507028,8 +507026,8 @@ codes is an increasing chain (with respect to inclusion).  (Contributed
 
   ${
     $d A a b x $.  $d B a b x $.  $d M a $.  $d S a $.  $d V a $.
-    satefv.s $e |- E = ( M SatE ( A e.g B ) ) $.
-    $( Characterization of a valuation ` S ` of a simplyfied satisfaction
+    sategoelfvb.s $e |- E = ( M SatE ( A e.g B ) ) $.
+    $( Characterization of a valuation ` S ` of a simplified satisfaction
        predicate for a Godel-set of membership.  (Contributed by AV,
        5-Nov-2023.) $)
     sategoelfvb $p |- ( ( M e. V /\ ( A e. _om /\ B e. _om ) )
@@ -507050,7 +507048,7 @@ codes is an increasing chain (with respect to inclusion).  (Contributed
       OPXSVSABVTWAZWBABKKWCVMWDTWKWTBCWKWTYOMNZBWKWQYOMYQTWKYSXSMNBYOXSMYRWBABK
       KWEVMWDTVRUQWFWG $.
 
-    $( Condition of a valuation ` S ` of a simplyfied satisfaction predicate
+    $( Condition of a valuation ` S ` of a simplified satisfaction predicate
        for a Godel-set of membership:  The sets in model ` M ` corresponding to
        the variables ` A ` and ` B ` under the assignment of ` S ` are in a
        membership relation in ` M ` .  (Contributed by AV, 5-Nov-2023.) $)
@@ -507062,7 +507060,7 @@ codes is an increasing chain (with respect to inclusion).  (Contributed
     $d M x $.  $d Z x $.
     sategoelelxmpl.s $e |- S = ( x e. _om
                           |-> if ( x = A , Z , if ( x = B , ~P Z , (/) ) ) ) $.
-    $( Example of a valuation of a simplyfied satisfaction predicate for a
+    $( Example of a valuation of a simplified satisfaction predicate for a
        Godel-set of membership.  (Contributed by AV, 5-Nov-2023.) $)
     sategoelelxmpl $p |- ( ( ( M e. WUni /\ Z e. M )
                         /\ ( A e. _om /\ B e. _om /\ A =/= B ) ) -> S e. E ) $=
@@ -507079,7 +507077,7 @@ codes is an increasing chain (with respect to inclusion).  (Contributed
       HSKWIWEXGWSOSWDWSSKWCGFVTTOSKWEVLUOQRVBXGWSOCVMVNVOVPWEWCWFWGLWKWLWOLWAWI
       XDWFWGWHVQBCDEFJHVRVSWB $.
 
-    $( Instance of ~ sategoelfv for the example of a valuation of a simplyfied
+    $( Instance of ~ sategoelfv for the example of a valuation of a simplified
        satisfaction predicate for a Godel-set of membership.  (Contributed by
        AV, 5-Nov-2023.) $)
     sategoelxmpl $p |- ( ( ( M e. WUni /\ Z e. M )