Review remarks

* ~satfv1lemlem1 and ~satfv1lemlem2 removed (replaced by ~fvsnun1 and ~fvsnun2 in the proof of ~satfv1lem) * comments of ~df-prv and ~prv0 enhanced.
avekens · Nov 26, 2023 · d91b350 · d91b350
1 parent cd79b65
commit d91b350
Showing 1 changed file with 40 additions and 53 deletions.
diff --git a/set.mm b/set.mm
@@ -505457,8 +505457,14 @@ required as (atomic) formulas, can be introduced as a defined notion in
     $d m u $.
     $( Define the "proves" relation on a set.  A wff is true in a model ` M `
        if for every valuation ` s e. ( M ^m _om ) ` , the interpretation of the
-       wff using the membership relation on ` M ` is true.  (Contributed by
-       Mario Carneiro, 14-Jul-2013.) $)
+       wff using the membership relation on ` M ` is true.  Since ` |= ` is
+       defined in terms of the interpretations making the given formula true,
+       it is not defined on the empty "model" ` M = (/) ` , since there are no
+       interpretations.  In particular, the empty set on the LHS of ` |= `
+       should not be interpreted as the empty model.  Statement ~ prv0 shows
+       that our definition yields ` (/) |= U ` for all formulas, though of
+       course the formula ` E. x x = x ` is not satisfied on the empty model.
+       (Contributed by Mario Carneiro, 14-Jul-2013.) $)
     df-prv $a |- |= = { <. m , u >. | ( m SatE u ) = ( m ^m _om ) } $.
   $}
 
@@ -505743,29 +505749,6 @@ required as (atomic) formulas, can be introduced as a defined notion in
       $.
   $}
 
-  $( Lemma 1 for ~ satfv1lem .  (Contributed by AV, 17-Nov-2023.) $)
-  satfv1lemlem1 $p |- ( ( N e. V /\ F e. ( M ^m V ) /\ Z e. M )
-              -> ( ( { <. N , Z >. } u. ( F |` ( V \ { N } ) ) ) ` N ) = Z ) $=
-    ( wcel cmap co w3a cop csn cdif cres cun cfv wfn cin c0 wceq 3adant2 difssd
-    fnsng 3ad2ant2 fnssresd wn neldifsnd incom eqeq1i disjsn bitri sylibr snidg
-    elmapfn 3ad2ant1 fvun1 syl112anc fvsng eqtrd ) CDFZABDGHFZEBFZIZCCEJKZADCKZ
-    LZMZNOZCVCOZEVBVCVDPZVFVEPVDVEQZRSZCVDFZVGVHSUSVAVIUTCEDBUBTVBDVEAUTUSADPVA
-    ABDUMUCVBDVDUAUDVBCVEFUEZVKVBCDUFVKVEVDQZRSVMVJVNRVDVEUGUHVECUIUJUKUSUTVLVA
-    CDULUNVDVEVCVFCUOUPUSVAVHESUTCEDBUQTUR $.
-
-  $( Lemma 2 for ~ satfv1lem .  (Contributed by AV, 17-Nov-2023.) $)
-  satfv1lemlem2 $p |- ( ( ( N e. V /\ J e. V /\ -. J = N )
-                          /\ F e. ( M ^m V ) /\ Z e. M )
-      -> ( ( { <. N , Z >. } u. ( F |` ( V \ { N } ) ) ) ` J ) = ( F ` J ) ) $=
-    ( wcel wceq wn w3a cmap co cop csn cfv wfn cin c0 wa sylibr cdif cres simp1
-    cun anim1i 3adant2 fnsng syl elmapfn 3ad2ant2 difssd neldifsnd incom eqeq1i
-    fnssresd disjsn bitri neqne anim2i 3adant1 3ad2ant1 eldifsn fvun2 syl112anc
-    wne fvresd eqtrd ) DEGZBEGZBDHIZJZACEKLGZFCGZJZBDFMNZAEDNZUAZUBZUDOZBVROZBA
-    OVNVOVPPZVRVQPVPVQQZRHZBVQGZVSVTHVNVHVMSZWAVKVMWEVLVKVHVMVHVIVJUCUEUFDFECUG
-    UHVNEVQAVLVKAEPVMACEUIUJVNEVPUKUOVNDVQGIZWCVNDEULWCVQVPQZRHWFWBWGRVPVQUMUNV
-    QDUPUQTVNVIBDVEZSZWDVKVLWIVMVIVJWIVHVJWHVIBDURUSUTVABEDVBTZVPVQVOVRBVCVDVNB
-    VQAWJVFVG $.
-
   ${
     $d E b $.  $d I a b z $.  $d J a b z $.  $d M b z $.  $d N a b z $.
     $( Lemma for ~ satfv1 .  (Contributed by AV, 9-Nov-2023.) $)
@@ -505780,32 +505763,32 @@ required as (atomic) formulas, can be introduced as a defined notion in
       csn cun co crab wral wif fveq1 breq12d elrab a1i cin wf 3ad2ant1 ad2antrr
       elex fsnd elmapex simpld snex elmapd adantll mpbird elmapi difssd fssresd
       simpr omex difexi res0 eqtr4i disjdif reseq2i 3eqtr4i elmapresaun syl3anc
-      c0 uncom difsnid syl5req oveq2d eleqtrrd ibar bicomd simpl1 satfv1lemlem1
-      simplr fveq2 breq2d ifptru bibi12d wn simpll3 simpl simprlr satfv1lemlem2
-      syl311anc ifpfal bitrd pm2.61ian breq1d simpll2 adantrl ralbidva rabbidva
-      mpdan ) FIJZCIJZDIJZUAZFAUBZUCUEZGUBZIFUEZUDZKZUFZCHUBZLZDYALZBMZHEINUGZU
-      HJZAEUICFOZDFOZXNXNBMZXNDXPLZBMZUJZYHCXPLZXNBMZYMYJBMZUJZUJZAEUIGYEXMXPYE
-      JZPZYFYQAEYSXNEJZPZYFXTYEJZCXTLZDXTLZBMZPZYQYFUUFQUUAYDUUEHXTYEYAXTOYBUUC
-      YCUUDBCYAXTUKDYAXTUKULUMUNUUAUUBUUFYQQUUAXTEXQXRUFZNUGZYEUUAXOEXQNUGJZXSE
-      XRNUGJZXOXQXRUOZKZXSUUKKZOZXTUUHJUUAUUIXQEXOUPZUUAFXNREXMFRJZYRYTXJXKUUPX
-      LFIUSUQURYSYTVJZUTYRYTUUIUUOQXMYRYTPZEXQXORRYRERJZYTYRUUSIRJXPEIVAVBZSXQR
-      JUURFVCUNVDVEVFYSUUJYTYRUUJXMYRUUJXREXSUPYRIEXRXPXPEIVGYRIXQVHVIYREXRXSRR
-      UUTXRRJYRIXQVKVLUNVDVFTSUUNUUAXOVTKZXSVTKZUULUUMUVAVTUVBXOVMXSVMVNUUKVTXO
-      XQIVOZVPUUKVTXSUVCVPVQUNXQXREXOXSVRVSUUAIUUGENXMIUUGOZYRYTXJXKUVDXLXJUUGX
-      RXQUFIXQXRWAIFWBWCUQURWDWEUUAUUBPZUUFUUEYQUVEUUEUUFUUBUUEUUFQUUAUUBUUEWFT
-      WGYGUVEUUEYQQZYGUVEPUVFFXTLZUUDBMZYLQZUVEUVIYGYHUVEUVIYHUVEPUVIUVGUVGBMZY
-      IQZUVEUVKYHUVEUVGXNUVGXNBUUAUVGXNOZUUBUUAXJYRYTUVLYSXJYTXJXKXLYRWHZSXMYRY
-      TWJZUUQXPEFIXNWIVSSZUVOULTYHUVIUVKQUVEYHUVHUVJYLYIYHUUDUVGUVGBDFXTWKZWLYH
-      YIYKWMWNSVFYHWOZUVEPZUVHYKYLUVRUVGXNUUDYJBUVEUVLUVQUVOTUVRXJXLUVQYRYTUUDY
-      JOZUVEXJUVQYSXJYTUUBUVMURZTUVEXLUVQUUAXLUUBXJXKXLYRYTWPSTUVQUVEWQUVEYRUVQ
-      UUAYRUUBUVNSZTUVQYSYTUUBWRXPDEFIXNWSWTZULUVQYKYLQUVEUVQYLYKYHYIYKXAWGSXBX
-      CTYGUVFUVIQUVEYGUUEUVHYQYLYGUUCUVGUUDBCFXTWKXDYGYLYPWMWNSVFYGWOZUVEPZUUEY
-      PYQYHUWDUUEYPQZYHUWDPUWEUUCUVGBMZYNQZUWDUWGYHUWDUUCYMUVGXNBUWDXJXKUWCYRYT
-      UUCYMOZUVEXJUWCUVTTUVEXKUWCUUAXKUUBXJXKXLYRYTXESTUWCUVEWQUVEYRUWCUWATUWCY
-      SYTUUBWRXPCEFIXNWSWTZUVEUVLUWCUVOTULTYHUWEUWGQUWDYHUUEUWFYPYNYHUUDUVGUUCB
-      UVPWLYHYNYOWMWNSVFUVQUWDPZUUEYOYPUWJUUCYMUUDYJBUWDUWHUVQUWITUVQUVEUVSUWCU
-      WBXFULUVQYOYPQUWDUVQYPYOYHYNYOXAWGSXBXCUWCYPYQQUVEUWCYQYPYGYLYPXAWGSXBXCX
-      BXIXBXGXH $.
+      c0 uncom difsnid syl5req oveq2d eleqtrrd ibar bicomd simpll1 eqid fvsnun1
+      fveq2 breq2d ifptru bibi12d wn wne neqne simpll3 anim12ci eldifsn fvsnun2
+      sylibr ifpfal bitrd pm2.61ian breq1d simpll2 adantrl ralbidva rabbidva
+      mpdan ) FIJZCIJZDIJZUAZFAUBZUCUEZGUBZIFUEZUDZKZUFZCHUBZLZDYCLZBMZHEINUGZU
+      HJZAEUICFOZDFOZXPXPBMZXPDXRLZBMZUJZYJCXRLZXPBMZYOYLBMZUJZUJZAEUIGYGXOXRYG
+      JZPZYHYSAEUUAXPEJZPZYHYBYGJZCYBLZDYBLZBMZPZYSYHUUHQUUCYFUUGHYBYGYCYBOYDUU
+      EYEUUFBCYCYBUKDYCYBUKULUMUNUUCUUDUUHYSQUUCYBEXSXTUFZNUGZYGUUCXQEXSNUGJZYA
+      EXTNUGJZXQXSXTUOZKZYAUUMKZOZYBUUJJUUCUUKXSEXQUPZUUCFXPREXOFRJZYTUUBXLXMUU
+      RXNFIUSUQURUUAUUBVJZUTYTUUBUUKUUQQXOYTUUBPZEXSXQRRYTERJZUUBYTUVAIRJXREIVA
+      VBZSXSRJUUTFVCUNVDVEVFUUAUULUUBYTUULXOYTUULXTEYAUPYTIEXTXRXREIVGYTIXSVHVI
+      YTEXTYARRUVBXTRJYTIXSVKVLUNVDVFTSUUPUUCXQVTKZYAVTKZUUNUUOUVCVTUVDXQVMYAVM
+      VNUUMVTXQXSIVOZVPUUMVTYAUVEVPVQUNXSXTEXQYAVRVSUUCIUUIENXOIUUIOZYTUUBXLXMU
+      VFXNXLUUIXTXSUFIXSXTWAIFWBWCUQURWDWEUUCUUDPZUUHUUGYSUVGUUGUUHUUDUUGUUHQUU
+      CUUDUUGWFTWGYIUVGUUGYSQZYIUVGPUVHFYBLZUUFBMZYNQZUVGUVKYIYJUVGUVKYJUVGPUVK
+      UVIUVIBMZYKQZUVGUVMYJUVGUVIXPUVIXPBUUCUVIXPOZUUDUUCFXPIXRYBIEXLXMXNYTUUBW
+      HZUUSYBWIZWJSZUVQULTYJUVKUVMQUVGYJUVJUVLYNYKYJUUFUVIUVIBDFYBWKZWLYJYKYMWM
+      WNSVFYJWOZUVGPZUVJYMYNUVTUVIXPUUFYLBUVGUVNUVSUVQTUVTFXPIDXRYBIEUVGXLUVSUU
+      CXLUUDUVOSZTUVGUUBUVSUUCUUBUUDUUSSZTUVPUVTXNDFWPZPDXTJUVSUWCUVGXNDFWQUUCX
+      NUUDXLXMXNYTUUBWRSWSDIFWTXBXAZULUVSYMYNQUVGUVSYNYMYJYKYMXCWGSXDXETYIUVHUV
+      KQUVGYIUUGUVJYSYNYIUUEUVIUUFBCFYBWKXFYIYNYRWMWNSVFYIWOZUVGPZUUGYRYSYJUWFU
+      UGYRQZYJUWFPUWGUUEUVIBMZYPQZUWFUWIYJUWFUUEYOUVIXPBUWFFXPICXRYBIEUVGXLUWEU
+      WATUVGUUBUWEUWBTUVPUWFXMCFWPZPCXTJUWEUWJUVGXMCFWQUUCXMUUDXLXMXNYTUUBXGSWS
+      CIFWTXBXAZUVGUVNUWEUVQTULTYJUWGUWIQUWFYJUUGUWHYRYPYJUUFUVIUUEBUVRWLYJYPYQ
+      WMWNSVFUVSUWFPZUUGYQYRUWLUUEYOUUFYLBUWFUUEYOOUVSUWKTUVSUVGUUFYLOUWEUWDXHU
+      LUVSYQYRQUWFUVSYRYQYJYPYQXCWGSXDXEUWEYRYSQUVGUWEYSYRYIYNYRXCWGSXDXEXDXKXD
+      XIXJ $.
   $}
 
   ${
@@ -507727,8 +507710,12 @@ proper pair (of ordinal numbers) as model for a Godel-set of membership
 
   ${
     $d U x $.
-    $( Every wff encoded as ` U ` is true in an empty model.  (Contributed by
-       AV, 19-Nov-2023.) $)
+    $( Every wff encoded as ` U ` is true in an "empty model" ( ` M = (/) ` ).
+       Since ` |= ` is defined in terms of the interpretations making the given
+       formula true, it is not defined on the "empty model", since there are no
+       interpretations.  In particular, the empty set on the LHS of ` |= `
+       should not be interpreted as the empty model, because ` E. x x = x ` is
+       not satisfied on the empty model.  (Contributed by AV, 19-Nov-2023.) $)
     prv0 $p |- ( U e. ( Fmla ` _om ) -> (/) |= U ) $=
       ( vx com cfmla cfv wcel c0 cprv wbr csate co wceq csat sate0 cv wn peano1
       wa cvv 0ex wal wf n0ii intnan a1i f00 sylnibr pm3.2i satfvel mp3an1 mtand