From ff36d62388d2685e799b94224c89c6233521f076 Mon Sep 17 00:00:00 2001
From: Benoit Jubin <benoit.jubin@gmail.com>
Date: Sat, 5 Oct 2024 22:22:43 +0200
Subject: [PATCH] Shorten dfnul2; mathbox propcalc.

---
 discouraged |  1 +
 set.mm      | 35 ++++++++++++++++++++++++++++++-----
 2 files changed, 31 insertions(+), 5 deletions(-)

diff --git a/discouraged b/discouraged
index 5e37c609b7..b914fe0323 100644
--- a/discouraged
+++ b/discouraged
@@ -19113,6 +19113,7 @@ Proof modification of "bj-exlimmpbi" is discouraged (11 steps).
 Proof modification of "bj-exlimmpbir" is discouraged (11 steps).
 Proof modification of "bj-exlimmpi" is discouraged (11 steps).
 Proof modification of "bj-exlimvmpi" is discouraged (10 steps).
+Proof modification of "bj-fal" is discouraged (5 steps).
 Proof modification of "bj-falor" is discouraged (4 steps).
 Proof modification of "bj-falor2" is discouraged (13 steps).
 Proof modification of "bj-fununsn1" is discouraged (37 steps).
diff --git a/set.mm b/set.mm
index 9b3f402196..6f4f8ecfd9 100644
--- a/set.mm
+++ b/set.mm
@@ -39611,8 +39611,8 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets,
      ~ ax-11 , and ~ ax-12 .  (Revised by Steven Nguyen, 3-May-2023.)  (Proof
      shortened by BJ, 23-Sep-2024.) $)
   dfnul2 $p |- (/) = { x | -. x = x } $=
-    ( c0 wfal cab weq wn dfnul4 fal equid notnoti 2false abbii eqtri ) BCADAAEZ
-    FZADAGCOACOHNAIJKLM $.
+    ( c0 wfal cab weq wn dfnul4 equid notnoti bifal abbii eqtr4i ) BCADAAEZFZAD
+    AGNCANMAHIJKL $.
 
   $( Alternate definition of the empty set.  (Contributed by NM, 25-Mar-2004.)
      (Proof shortened by BJ, 23-Sep-2024.) $)
@@ -430011,9 +430011,9 @@ involves a class difference ("dif") of a subset ("ss"), and thus is
 
        <li><b>Closures and values.</b>
        As noted above, if a function df-NAME is defined, there is typically a
-       proof of its value labeled "NAMEval" and of its closure labeld "NAMEcl".
-       E.g., for cosine ( ~ df-cos ) we have value ~ cosval and closure
-       ~ coscl .
+       proof of its value labeled "NAMEval" and of its closure labeled
+       "NAMEcl".  E.g., for cosine ( ~ df-cos ) we have value ~ cosval and
+       closure ~ coscl .
        </li>
 
        <li><b>Special cases.</b>
@@ -545131,6 +545131,31 @@ proof is intuitionistic (use of ~ ax-3 comes from the unusual definition
       ( wi bj-looinvi ax-mp ) BAEADABCFG $.
   $}
 
+  ${
+    bj-mt2bi.min $e |- ph $.
+    bj-mt2bi.maj $e |- ( ps <-> -. ph ) $.
+    $( Version of ~ mt2 where the major premise is a biconditional.  Another
+       proof is also possible via ~ con2bii and ~ mpbi .  The current ~ mt2bi
+       should be relabeled, maybe to imfal.  (Contributed by BJ,
+       5-Oct-2024.) $)
+    bj-mt2bi $p |- -. ps $=
+      ( wn biimpi mt2 ) BACBAEDFG $.
+  $}
+
+  ${
+    bj-ntrufal.1 $e |- ph $.
+    $( The negation of a theorem is equivalent to false.  This can shorten
+       ~ dfnul2 .  (Contributed by BJ, 5-Oct-2024.) $)
+    bj-ntrufal $p |- ( -. ph <-> F. ) $=
+      ( wn notnoti bifal ) ACABDE $.
+  $}
+
+  $( Shortening of ~ fal using ~ bj-mt2bi .  (Contributed by Anthony Hart,
+     22-Oct-2010.)  (Proof shortened by Mel L. O'Cat, 11-Mar-2012.)
+     (Proof modification is discouraged.) $)
+  bj-fal $p |- -. F. $=
+    ( wtru wfal tru df-fal bj-mt2bi ) ABCDE $.
+
 
 $(
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-