Theorems for Godel-sets (3) (#3596)

* Theorems for Godel-sets (3)

The proof that ( ( M Sat E ) ` N ) is a function, as indicated in the definition ~df-sat, which was missing in PR #3572, is available now (see ~satffun).

Changes in main set.mm:
* ~bj-2ex moved as ~2oex from BJ's mathbox
* ~ralrexbid, ~elneeldif, ~rexdifi added
* ~dmopabelb, ~dmopab2rex added
* ~releldmdifi, ~funfv1st2nd, ~funelss, ~funeldmdif added
* ~omsucne, ~1one2o added

Changes in MC's mathbox:
* theorems for "Godel-set for the Sheffer stroke NAND" added (~gonafv, ~gonanegoal)
* ~satfvsucsuc added
* theorems for Godel-formulas added (~fmlasssuc, ~fmlan0, ~gonan0, ~goaln0, ~gonar, ~goalr)
* theorems for disjoint sets of Godel-formulas added (~fmla0disjsuc, ~fmlasucdisj)
* main theorem ~satffun added (together with some lemmata)
*

* typos corrected, theorem satff added

* theorem ~satff added and mentioned in the comment of ~df-sat

* formatting

* correction of copy&paste error

detected by Gérard Lang.

---------

Co-authored-by: tirix <[email protected]>

Author: avekens

changes-set.txt

@@ -102,6 +102,7 @@ make a github issue.)
 DONE:
 Date      Old       New         Notes
 31-Oct-23 spimv1    spimfv      labeling consistent with speimfv
+28-Oct-23 bj-2ex    2oex        moved from BJ's mathbox to main set.mm
 23-Oct-23 bj-alequexv alequexv  moved from BJ's mathbox to main set.mm
 23-Oct-23 axext2    axexte      existential form of ax-ext
 23-Oct-23 axext3    axextg      more general form of ax-ext