Theorems for Godel-sets (4a) - rewrap

* theorems for ` ( M SatE U ) ` added: ~satefv, ~satef, ~sate0fv0, ~satefvfmla0 * exaples for simple wff codes added: ~sategoelfvb, ~sategoelfv, ~sategoelelxmpl, ~sategoelxmpl * theorem for ` M |= U ` added: ~prv
avekens · Nov 5, 2023 · 472ed58 · 472ed58
1 parent 385a588
commit 472ed58
Showing 1 changed file with 25 additions and 25 deletions.
diff --git a/set.mm b/set.mm
@@ -71646,7 +71646,7 @@ Axiom of Replacement (unlike ~ resfunexg ).  (Contributed by NM,
        (Contributed by AV, 6-Oct-2023.) $)
     fiunlem $p |- ( ( ( B : D --> S /\ A. y e. A ( B C_ C \/ C C_ B ) )
                     /\ u = B ) -> A. v e. { z | E. x e. A z = B }
-                                  ( u C_ v \/ v C_ u ) ) $=
+                                     ( u C_ v \/ v C_ u ) ) $=
       ( wss wo wa cv wceq wrex weq sseq12 sylan2b wf wral cab vex eqeq1 rexbidv
       wcel elab eqeq2d cbvrexv r19.29 ancoms orbi12d biimprcd expdimp rexlimivw
       wi wb imp sylan an32s adantlll ralrimiva ) IJGUAZGHLZHGLZMZBFUBZNEOZGPZNZ
@@ -71661,7 +71661,7 @@ Axiom of Replacement (unlike ~ resfunexg ).  (Contributed by NM,
        function.  Analogous to ~ fun11iun .  (Contributed by AV,
        6-Oct-2023.) $)
     fiun $p |- ( A. x e. A ( B : D --> S /\ A. y e. A ( B C_ C \/ C C_ B ) )
-                   -> U_ x e. A B : U_ x e. A D --> S ) $=
+                 -> U_ x e. A B : U_ x e. A D --> S ) $=
       ( vz vu vv wss wral wa ciun wfun cv wrex wcel wf wo wfn crn cdm wceq cuni
       cab vex weq eqeq1 rexbidv elab r19.29 nfv nfre1 nfab nfral nfan wi adantr
       ffun wb funeq adantl mpbird adantlr fiunlem jca a1i rexlimi syl ralrimiva
@@ -71706,11 +71706,11 @@ Axiom of Replacement (unlike ~ resfunexg ).  (Contributed by NM,
 
   ${
     $d F i $.  $d I i $.  $d J i $.
-    fviun.s $e |- U = U_ i e. I ( F ` i ) $.
+    fviunfun.u $e |- U = U_ i e. I ( F ` i ) $.
     $( The function value of an indexed union is the value of one of the
-       indexed functions.  (Contributed by AV, 4-Novt-2023.) $)
+       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 ) ) $=
+                     -> ( 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
@@ -506894,7 +506894,7 @@ codes is an increasing chain (with respect to inclusion).  (Contributed
   ${
     $d E x y $.  $d M x y $.  $d V x y $.  $d W x y $.
     $( The satisfaction predicate as function over wff codes in the model ` M `
-       and the binary relation ` E ` on ` M `.  (Contributed by AV,
+       and the binary relation ` E ` on ` M ` .  (Contributed by AV,
        29-Oct-2023.) $)
     satfun $p |- ( ( M e. V /\ E e. W )
              -> ( ( M Sat E ) ` _om ) : ( Fmla ` _om ) --> ~P ( M ^m _om ) ) $=
@@ -506918,14 +506918,14 @@ codes is an increasing chain (with respect to inclusion).  (Contributed
      code ` U ` for a wff using ` e. , -/\ , A. ` is a valuation
      ` S : _om --> M ` of the variables (v_0 ` = ( S `` (/) ) ` , v_1
      ` = ( S `` 1o ) ` , etc.) so that ` U ` is true under the assignment
-     ` S ` . (Contributed by AV, 29-Oct-2023.) $)
-    satfvel $p |- ( ( ( M e. V /\ E e. W ) /\ U e. ( Fmla ` _om )
+     ` S ` .  (Contributed by AV, 29-Oct-2023.) $)
+  satfvel $p |- ( ( ( M e. V /\ E e. W ) /\ U e. ( Fmla ` _om )
                     /\ S e. ( ( ( M Sat E ) ` _om ) ` U ) )
                  -> S : _om --> M ) $=
-      ( wcel wa com cfmla cfv csat co wf cmap cpw wi satfun ffvelrn syl fvex ex
-      wss elpw ssel elmapi syl6 sylbi 3imp ) DEGCFGHZBIJKZGZABIDCLMKZKZGZIDANZU
-      JUKDIOMZPZUMNZULUOUPQZQCDEFRUSULUTUSULHUNURGZUTUKURBUMSVAUNUQUCZUTUNUQBUM
-      UAUDVBUOAUQGUPUNUQAUEADIUFUGUHTUBTUI $.
+    ( wcel wa com cfmla cfv csat co wf cmap cpw wi satfun ffvelrn syl fvex elpw
+    wss ssel elmapi syl6 sylbi ex 3imp ) DEGCFGHZBIJKZGZABIDCLMKZKZGZIDANZUJUKD
+    IOMZPZUMNZULUOUPQZQCDEFRUSULUTUSULHUNURGZUTUKURBUMSVAUNUQUCZUTUNUQBUMUAUBVB
+    UOAUQGUPUNUQAUDADIUEUFUGTUHTUI $.
 
   ${
     $d E a i j x y $.  $d M a i j x y $.  $d X a i j x y $.
@@ -506963,24 +506963,24 @@ codes is an increasing chain (with respect to inclusion).  (Contributed
        model ` M ` at the code ` U ` .  (Contributed by AV, 30-Oct-2023.) $)
     satefv $p |- ( ( M e. V /\ U e. W ) -> ( M SatE U )
                        = ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` U ) ) $=
-    ( vm vu wcel wa cvv cv com cep cxp cin csat co cfv csate wceq adantr a1i id
-    cmpo df-sate sqxpeqd ineq2d oveq12d fveq1d simpr fveq12d adantl elex ovmpod
-    fvexd ) BCGZADGZHZEFBAIIFJZKEJZLUSUSMZNZOPZQZQZAKBLBBMZNZOPZQZQZRIREFIIVDUC
-    SUQFEUDUAUSBSZURASZHZVDVISUQVLURAVCVHVJVCVHSVKVJKVBVGVJUSBVAVFOVJUBZVJUTVEL
-    VJUSBVMUEUFUGUHTVJVKUIUJUKUOBIGUPBCULTUPAIGUOADULUKUQAVHUNUM $.
+      ( vm vu wcel wa cvv cv com cep cxp cin csat co cfv csate wceq adantr cmpo
+      df-sate a1i sqxpeqd ineq2d oveq12d fveq1d simpr fveq12d adantl elex fvexd
+      id ovmpod ) BCGZADGZHZEFBAIIFJZKEJZLUSUSMZNZOPZQZQZAKBLBBMZNZOPZQZQZRIREF
+      IIVDUASUQFEUBUCUSBSZURASZHZVDVISUQVLURAVCVHVJVCVHSVKVJKVBVGVJUSBVAVFOVJUM
+      ZVJUTVELVJUSBVMUDUEUFUGTVJVKUHUIUJUOBIGUPBCUKTUPAIGUOADUKUJUQAVHULUN $.
   $}
 
   $( The simplified satisfaction predicate for any wff code over an empty
      model.  (Contributed by AV, 6-Oct-2023.)  (Revised by AV, 5-Nov-2023.) $)
   sate0 $p |- ( U e. V -> ( (/) SatE U )
                           = ( ( ( (/) Sat (/) ) ` _om ) ` U ) ) $=
-      ( wcel csate com cep cxp cin csat cfv cvv wceq 0ex satefv mpan xp0 ineq2i
-      c0 co fveq1i in0 eqtri oveq2i syl6eq ) ABCZRADSZAERFRRGZHZISZJZJZAERRISZJ
-      ZJRKCUEUFUKLMARKBNOAUJUMEUIULUHRRIUHFRHRUGRFRPQFUAUBUCTTUD $.
+    ( wcel c0 csate co com cep cxp cin csat cfv cvv wceq 0ex satefv mpan ineq2i
+    xp0 fveq1i in0 eqtri oveq2i syl6eq ) ABCZDAEFZAGDHDDIZJZKFZLZLZAGDDKFZLZLDM
+    CUEUFUKNOADMBPQAUJUMGUIULUHDDKUHHDJDUGDHDSRHUAUBUCTTUD $.
 
   $( The simplified satisfaction predicate as function over wff codes over an
      empty model.  (Contributed by AV, 30-Oct-2023.) $)
-  satef $p |- ( ( M e. V /\ U e. ( Fmla ` _om ) /\  S e. ( M SatE U ) )
+  satef $p |- ( ( M e. V /\ U e. ( Fmla ` _om ) /\ S e. ( M SatE U ) )
                   -> S : _om --> M ) $=
     ( wcel com cfmla cfv csate co w3a cep cxp cin cvv wa csat adantr syl simpr
     wf satefv eleq2d simpl incom sqxpexg inex1g syl5eqel jca 3jca sylbid 3impia
@@ -507051,9 +507051,9 @@ codes is an increasing chain (with respect to inclusion).  (Contributed
       KWEVMWDTVRUQWFWG $.
 
     $( Condition of a valuation ` S ` of a simplyfied satisfaction predicate
-       for a Godel-set of membership: The sets in model ` M ` corresponding to
+       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.) $)
+       membership relation in ` M ` .  (Contributed by AV, 5-Nov-2023.) $)
     sategoelfv $p |- ( ( M e. V /\ ( A e. _om /\ B e. _om ) /\ S e. E )
                        -> ( S ` A ) e. ( S ` B ) ) $=
       ( wcel com wa cfv cmap co sategoelfvb simpr syl6bi 3impia ) EFHZAIHBIHJZC
@@ -507063,7 +507063,7 @@ codes is an increasing chain (with respect to inclusion).  (Contributed
     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
-       Godel-set of membership. (Contributed by AV, 5-Nov-2023.) $)
+       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 ) $=
       ( cwun wcel wa com wceq c0 cif ifcld adantr cvv adantl wne w3a cmap co wf
@@ -507080,7 +507080,7 @@ codes is an increasing chain (with respect to inclusion).  (Contributed
       XDWFWGWHVQBCDEFJHVRVSWB $.
 
     $( Instance of ~ sategoelfv for the example of a valuation of a simplyfied
-       satisfaction predicate for a Godel-set of membership. (Contributed by
+       satisfaction predicate for a Godel-set of membership.  (Contributed by
        AV, 5-Nov-2023.) $)
     sategoelxmpl $p |- ( ( ( M e. WUni /\ Z e. M )
                            /\ ( A e. _om /\ B e. _om /\ A =/= B ) )