--- David A. Wheeler
--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.
...and I thought I was answering fast! ;-)
My method ultimately leads to a proof longer than Mario's:
10::df-pr |- { C , D } = ( { C } u. { D } )
20::difundi |- ( B \ ( { C } u. { D } ) ) = ( ( B \ { C } )
i^i ( B \ { D } ) )
25:10:difeq2i |- ( B \ { C , D } ) = ( B \ ( { C } u. { D } )
)
26:25,20:eqtri |- ( B \ { C , D } ) = ( ( B \ { C } ) i^i ( B
\ { D } ) )
29:26:eleq2i |- ( A e. ( B \ { C , D } ) <-> A e. ( (
B \ { C } ) i^i ( B \ { D } ) ) )
30::elin |- ( A e. ( ( B \ { C } ) i^i ( B \ { D } ) )
<-> ( A e. ( B \ { C } ) /\ A e. ( B \ { D } ) ) )
40::eldifsn |- ( A e. ( B \ { C } ) <-> ( A e. B /\ A
=/= C ) )
50::eldifsn |- ( A e. ( B \ { D } ) <-> ( A e. B /\ A
=/= D ) )
60:40,50:anbi12i |- ( ( A e. ( B \ { C } ) /\ A e. ( B \ { D } )
) <-> ( ( A e. B /\ A =/= C ) /\ ( A e. B /\ A =/= D ) ) )
70::anandi |- ( ( A e. B /\ ( A =/= C /\ A =/= D ) )
<-> ( ( A e. B /\ A =/= C ) /\ ( A e. B /\ A =/= D ) ) )
80::3anass |- ( ( A e. B /\ A =/= C /\ A =/= D ) <->
( A e. B /\ ( A =/= C /\ A =/= D ) ) )
90:29,30,60:3bitri |- ( A e. ( B \ { C , D } ) <-> ( ( A e.
B /\ A =/= C ) /\ ( A e. B /\ A =/= D ) ) )
qed:70,80,90:3bitr4ri |- ( A e. ( B \ { C , D } ) <-> ( A e.
B /\ A =/= C /\ A =/= D ) )
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
--- David A. Wheeler
On Tue, 18 Jul 2017 19:49:53 +0100, Mario Carneiro <di....@gmail.com> wrote:
> That would be eldifpr and eldiftp. [in addition to eldifsn]
Okay. Given that "eldifsn" is:
> ( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )
I'm trying to decipher the naming convention used here.
I'm guessing the initial "el" is "element member of" (e.),
"dif" is "difference", and the last 2 letters
are sn->singleton, pr->pair, tp->triple.
Is that right? Or is "d" used for difference, followed by "if"?
If so, that seems odd; "if" is often used for inference "->", but this is a
biconditional.
I'd like to document in comments where some of the
names "come from", to help make the naming conventions more obvious.
Something like this:
The name of this theorem ("eldifsn") is derived from
"el" (element member of) + "dif" (difference) + "sn" (singleton).
> On Tue, Jul 18, 2017 at 10:19 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:
> > I'd like to document in comments where some of the
> > names "come from", to help make the naming conventions more obvious.
> > Something like this:
> > The name of this theorem ("eldifsn") is derived from
> > "el" (element member of) + "dif" (difference) + "sn" (singleton).
On Tue, 18 Jul 2017 22:45:52 +0100, Mario Carneiro <di....@gmail.com> wrote:
> I'm not opposed to this, but I don't know how best to present and store the
> information.
I think putting a list in "conventions" of some more-common abbrevations used in
names would be a good start. It should show both the longer name (to help
remember it) and its symbol(s) where relevant.
I'd also add examples, to put them in context, and
sort them alphabetically so a mysterious name might be decodable.
In short, add this to "conventions":
Common abbreviations used in theorem names are:
* "dif": difference ( ` \ ` ). Example: ~ eldifsn
* "el": element member of ( ` e. ` ). Example: ~ eldifsn
* "mp": modus ponens
* "sn": singleton ( ` { A } ` ). Example: ~ eldifsn
* "syl": syllogism
On Tue, 18 Jul 2017 19:49:53 +0100, Mario Carneiro wrote:
> That would be eldifpr and eldiftp. [in addition to eldifsn]
Okay. Given that "eldifsn" is:
> ( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )
I'm trying to decipher the naming convention used here.
I'm guessing the initial "el" is "element member of" (e.),
"dif" is "difference", and the last 2 letters
are sn->singleton, pr->pair, tp->triple.
Is that right? Or is "d" used for difference, followed by "if"?
If so, that seems odd; "if" is often used for inference "->", but this is a
biconditional.
I'd like to document in comments where some of the
names "come from", to help make the naming conventions more obvious.
Something like this:
The name of this theorem ("eldifsn") is derived from
"el" (element member of) + "dif" (difference) + "sn" (singleton).
...
(As a semi-related aside, I want to change "*a4*", which means "related to ax-4", to become "sp", standing for "specialization", because tying the abbreviation to ax-4 would make a later change of axiom names confusing. There aren't any conflicts with "sp" in the pred. calc. section, only later on where it means "span" and a few other things, but we tolerate such conflicts outside of context.)
Most people will be unaffected by this change because it is not common for the axioms to be referenced directly in proofs.
I'm okay with all this, although separating ax-9, ax-11 and especially ax-17 from these numbers will take some re-learning. (I've also referred to them by these names in various papers, which will now be obsolete. Not sure how much of a concern this is.)
Most people will be unaffected by this change because it is not common for the axioms to be referenced directly in proofs.It's good, then, that we introduced nfv as an alternative to ax-17. Pretty sure none of the others have more than a handful of direct uses.Mario