Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Shorten dfnul2; mathbox propcalc. #4267

Merged
merged 1 commit into from
Oct 6, 2024
Merged

Shorten dfnul2; mathbox propcalc. #4267

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions discouraged
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down
35 changes: 30 additions & 5 deletions set.mm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.) $)
Expand Down Expand Up @@ -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>
Expand Down Expand Up @@ -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 $.


$(
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
Expand Down
Loading