MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  conventions-label Structured version   Visualization version   GIF version

Theorem conventions-label 26413
Description:

The following explains some of the label conventions in use in the Metamath Proof Explorer ("set.mm"). For the general conventions, see conventions 26412.

Every statement has a unique identifying label, which serves the same purpose as an equation number in a book. We use various label naming conventions to provide easy-to-remember hints about their contents. Labels are not a 1-to-1 mapping, because that would create long names that would be difficult to remember and tedious to type. Instead, label names are relatively short while suggesting their purpose. Names are occasionally changed to make them more consistent or as we find better ways to name them. Here are a few of the label naming conventions:

  • Axioms, definitions, and wff syntax. As noted earlier, axioms are named "ax-NAME", proofs of proven axioms are named "axNAME", and definitions are named "df-NAME". Wff syntax declarations have labels beginning with "w" followed by short fragment suggesting its purpose.
  • Hypotheses. Hypotheses have the name of the final axiom or theorem, followed by ".", followed by a unique id (these ids are usually consecutive integers starting with 1, e.g. for rgen 2901"rgen.1 $e |- ( x e. A -> ph ) $." or letters corresponding to the (main) class variable used in the hypothesis, e.g. for mdet0 20169: "mdet0.d $e |- D = ( N maDet R ) $.").
  • Common names. If a theorem has a well-known name, that name (or a short version of it) is sometimes used directly. Examples include barbara 2546 and stirling 38782.
  • Principia Mathematica. Proofs of theorems from Principia Mathematica often use a special naming convention: "pm" followed by its identifier. For example, Theorem *2.27 of [WhiteheadRussell] p. 104 is named pm2.27 40.
  • 19.x series of theorems. Similar to the conventions for the theorems from Principia Mathematica, theorems from Section 19 of [Margaris] p. 90 often use a special naming convention: "19." resp. "r19." (for corresponding restricted quantifier versions) followed by its identifier. For example, Theorem 38 from Section 19 of [Margaris] p. 90 is labeled 19.38 1755, and the restricted quantifier version of Theorem 21 from Section 19 of [Margaris] p. 90 is labeled r19.21 2934.
  • Characters to be used for labels Although the specification of Metamath allows for dots/periods "." in any label, it is usually used only in labels for hypotheses (see above). Exceptions are the labels of theorems from Principia Mathematica and the 19.x series of theorems from Section 19 of [Margaris] p. 90 (see above) and 0.999... 14393. Furthermore, the underscore "_" should not be used.
  • Syntax label fragments. Most theorems are named using a concatenation of syntax label fragments (omitting variables) that represent the important part of the theorem's main conclusion. Almost every syntactic construct has a definition labeled "df-NAME", and normally NAME is the syntax label fragment. For example, the class difference construct (𝐴𝐵) is defined in df-dif 3538, and thus its syntax label fragment is "dif". Similarly, the subclass relation 𝐴𝐵 has syntax label fragment "ss" because it is defined in df-ss 3549. Most theorem names follow from these fragments, for example, the theorem proving (𝐴𝐵) ⊆ 𝐴 involves a class difference ("dif") of a subset ("ss"), and thus is labeled difss 3694. There are many other syntax label fragments, e.g., singleton construct {𝐴} has syntax label fragment "sn" (because it is defined in df-sn 4121), and the pair construct {𝐴, 𝐵} has fragment "pr" ( from df-pr 4123). Digits are used to represent themselves. Suffixes (e.g., with numbers) are sometimes used to distinguish multiple theorems that would otherwise produce the same label.
  • Phantom definitions. In some cases there are common label fragments for something that could be in a definition, but for technical reasons is not. The is-element-of (is member of) construct 𝐴𝐵 does not have a df-NAME definition; in this case its syntax label fragment is "el". Thus, because the theorem beginning with (𝐴 ∈ (𝐵 ∖ {𝐶}) uses is-element-of ("el") of a class difference ("dif") of a singleton ("sn"), it is labeled eldifsn 4255. An "n" is often used for negation (¬), e.g., nan 601.
  • Exceptions. Sometimes there is a definition df-NAME but the label fragment is not the NAME part. The definition should note this exception as part of its definition. In addition, the table below attempts to list all such cases and marks them in bold. For example, the label fragment "cn" represents complex numbers (even though its definition is in df-c 9794) and "re" represents real numbers ( definition df-r 9798). The empty set often uses fragment 0, even though it is defined in df-nul 3870. The syntax construct (𝐴 + 𝐵) usually uses the fragment "add" (which is consistent with df-add 9799), but "p" is used as the fragment for constant theorems. Equality (𝐴 = 𝐵) often uses "e" as the fragment. As a result, "two plus two equals four" is labeled 2p2e4 10987.
  • Other markings. In labels we sometimes use "com" for "commutative", "ass" for "associative", "rot" for "rotation", and "di" for "distributive".
  • Focus on the important part of the conclusion. Typically the conclusion is the part the user is most interested in. So, a rough guideline is that a label typically provides a hint about only the conclusion; a label rarely says anything about the hypotheses or antecedents. If there are multiple theorems with the same conclusion but different hypotheses/antecedents, then the labels will need to differ; those label differences should emphasize what is different. There is no need to always fully describe the conclusion; just identify the important part. For example, cos0 14661 is the theorem that provides the value for the cosine of 0; we would need to look at the theorem itself to see what that value is. The label "cos0" is concise and we use it instead of "cos0eq1". There is no need to add the "eq1", because there will never be a case where we have to disambiguate between different values produced by the cosine of zero, and we generally prefer shorter labels if they are unambiguous.
  • Closures and values. 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 14582) we have value cosval 14634 and closure coscl 14638.
  • Special cases. Sometimes, syntax and related markings are insufficient to distinguish different theorems. For example, there are over a hundred different implication-only theorems. They are grouped in a more ad-hoc way that attempts to make their distinctions clearer. These often use abbreviations such as "mp" for "modus ponens", "syl" for syllogism, and "id" for "identity". It is especially hard to give good names in the propositional calculus section because there are so few primitives. However, in most cases this is not a serious problem. There are a few very common theorems like ax-mp 5 and syl 17 that you will have no trouble remembering, a few theorem series like syl*anc and simp* that you can use parametrically, and a few other useful glue things for destructuring 'and's and 'or's (see natded 26414 for a list), and that is about all you need for most things. As for the rest, you can just assume that if it involves at most three connectives, then it is probably already proved in set.mm, and searching for it will give you the label.
  • Suffixes. Suffixes are used to indicate the form of a theorem (see above). Additionally, we sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as 𝑥𝜑 in 19.21 2059 via the use of disjoint variable conditions combined with nfv 1828. If two (or three) such hypotheses are eliminated, the suffix "vv" resp. "vvv" is used, e.g. exlimivv 1845. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the disjoint variable condition; e.g. euf 2461 derived from df-eu 2457. The "f" stands for "not free in" which is less restrictive than "does not occur in." The suffix "b" often means "biconditional" (, "iff" , "if and only if"), e.g. sspwb 4834. We sometimes suffix with "s" the label of an inference that manipulates an antecedent, leaving the consequent unchanged. The "s" means that the inference eliminates the need for a syllogism (syl 17) -type inference in a proof. A theorem label is suffixed with "ALT" if it provides an alternate less-preferred proof of a theorem (e.g., the proof is clearer but uses more axioms than the preferred version). The "ALT" may be further suffixed with a number if there is more than one alternate theorem. Furthermore, a theorem label is suffixed with "OLD" if there is a new version of it and the OLD version is obsolete (and will be removed within one year). Finally, it should be mentioned that suffixes can be combined, for example in cbvaldva 2263 (cbval 2253 in deduction form "d" with a not free variable replaced by a disjoint variable condition "v" with a conjunction as antecedent "a"). Here is a non-exhaustive list of common suffixes:
    • a : theorem having a conjunction as antecedent
    • b : theorem expressing a logical equivalence
    • c : contraction (e.g., sylc 62, syl2anc 690), commutes (e.g., biimpac 501)
    • d : theorem in deduction form
    • f : theorem with a hypothesis such as 𝑥𝜑
    • g : theorem in closed form having an "is a set" antecedent
    • i : theorem in inference form
    • l : theorem concerning something at the left
    • r : theorem concerning something at the right
    • r : theorem with something reversed (e.g., a biconditional)
    • s : inference that manipulates an antecedent ("s" refers to an application of syl 17 that is eliminated)
    • v : theorem with one (main) disjoint variable condition
    • vv : theorem with two (main) disjoint variable conditions
    • w : weak(er) form of a theorem
    • ALT : alternate proof of a theorem
    • ALTV : alternate version of a theorem or definition
    • OLD : old/obsolete version of a theorem/definition/proof
  • Reuse. When creating a new theorem or axiom, try to reuse abbreviations used elsewhere. A comment should explain the first use of an abbreviation.

The following table shows some commonly used abbreviations in labels, in alphabetical order. For each abbreviation we provide a mnenomic, the source theorem or the assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME. This is not a complete list of abbreviations, though we do want this to eventually be a complete list of exceptions.
AbbreviationMnenomicSource ExpressionSyntax?Example(s)
aand (suffix) No biimpa 499, rexlimiva 3005
ablAbelian group df-abl 17961 Abel Yes ablgrp 17963, zringabl 19583
absabsorption No ressabs 15708
absabsolute value (of a complex number) df-abs 13766 (abs‘𝐴) Yes absval 13768, absneg 13807, abs1 13827
adadding No adantr 479, ad2antlr 758
addadd (see "p") df-add 9799 (𝐴 + 𝐵) Yes addcl 9870, addcom 10069, addass 9875
al"for all" 𝑥𝜑 No alim 1727, alex 1741
ALTalternative/less preferred (suffix) No idALT 23
anand df-an 384 (𝜑𝜓) Yes anor 508, iman 438, imnan 436
antantecedent No adantr 479
assassociative No biass 372, orass 544, mulass 9876
asymasymmetric, antisymmetric No intasym 5413, asymref 5414, posasymb 16717
axaxiom No ax6dgen 1990, ax1cn 9822
bas, base base (set of an extensible structure) df-base 15642 (Base‘𝑆) Yes baseval 15688, ressbas 15699, cnfldbas 19513
b, bibiconditional ("iff", "if and only if") df-bi 195 (𝜑𝜓) Yes impbid 200, sspwb 4834
brbinary relation df-br 4574 𝐴𝑅𝐵 Yes brab1 4620, brun 4623
cbvchange bound variable No cbvalivw 1919, cbvrex 3139
clclosure No ifclda 4065, ovrcl 6558, zaddcl 11246
cncomplex numbers df-c 9794 Yes nnsscn 10868, nncn 10871
cnfldfield of complex numbers df-cnfld 19510 fld Yes cnfldbas 19513, cnfldinv 19538
cntzcentralizer df-cntz 17515 (Cntz‘𝑀) Yes cntzfval 17518, dprdfcntz 18179
cnvconverse df-cnv 5032 𝐴 Yes opelcnvg 5208, f1ocnv 6043
cocomposition df-co 5033 (𝐴𝐵) Yes cnvco 5214, fmptco 6284
comcommutative No orcom 400, bicomi 212, eqcomi 2614
concontradiction, contraposition No condan 830, con2d 127
csbclass substitution df-csb 3495 𝐴 / 𝑥𝐵 Yes csbid 3502, csbie2g 3525
cygcyclic group df-cyg 18045 CycGrp Yes iscyg 18046, zringcyg 19597
ddeduction form (suffix) No idd 24, impbid 200
df(alternate) definition (prefix) No dfrel2 5484, dffn2 5942
di, distrdistributive No andi 906, imdi 376, ordi 903, difindi 3835, ndmovdistr 6694
difclass difference df-dif 3538 (𝐴𝐵) Yes difss 3694, difindi 3835
divdivision df-div 10530 (𝐴 / 𝐵) Yes divcl 10536, divval 10532, divmul 10533
dmdomain df-dm 5034 dom 𝐴 Yes dmmpt 5529, iswrddm0 13126
e, eq, equequals df-cleq 2598 𝐴 = 𝐵 Yes 2p2e4 10987, uneqri 3712, equtr 1933
elelement of 𝐴𝐵 Yes eldif 3545, eldifsn 4255, elssuni 4393
eu"there exists exactly one" df-eu 2457 ∃!𝑥𝜑 Yes euex 2477, euabsn 4200
exexists (i.e. is a set) No brrelex 5066, 0ex 4709
ex"there exists (at least one)" df-ex 1695 𝑥𝜑 Yes exim 1749, alex 1741
expexport No expt 166, expcom 449
f"not free in" (suffix) No equs45f 2333, sbf 2363
ffunction df-f 5790 𝐹:𝐴𝐵 Yes fssxp 5955, opelf 5960
falfalse df-fal 1480 Yes bifal 1487, falantru 1498
fifinite intersection df-fi 8173 (fi‘𝐵) Yes fival 8174, inelfi 8180
fi, finfinite df-fin 7818 Fin Yes isfi 7838, snfi 7896, onfin 8009
fldfield (Note: there is an alternative definition Fld of a field, see df-fld 32760) df-field 18515 Field Yes isfld 18521, fldidom 19068
fnfunction with domain df-fn 5789 𝐴 Fn 𝐵 Yes ffn 5940, fndm 5886
frgpfree group df-frgp 17888 (freeGrp‘𝐼) Yes frgpval 17936, frgpadd 17941
fsuppfinitely supported function df-fsupp 8132 𝑅 finSupp 𝑍 Yes isfsupp 8135, fdmfisuppfi 8140, fsuppco 8163
funfunction df-fun 5788 Fun 𝐹 Yes funrel 5803, ffun 5943
fvfunction value df-fv 5794 (𝐹𝐴) Yes fvres 6098, swrdfv 13218
fzfinite set of sequential integers df-fz 12149 (𝑀...𝑁) Yes fzval 12150, eluzfz 12159
fz0finite set of sequential nonnegative integers (0...𝑁) Yes nn0fz0 12257, fz0tp 12260
fzohalf-open integer range df-fzo 12286 (𝑀..^𝑁) Yes elfzo 12292, elfzofz 12305
gmore general (suffix); eliminates "is a set" hypothsis No uniexg 6826
gragraph No uhgrav 25587, isumgra 25606, usgrares 25660
grpgroup df-grp 17190 Grp Yes isgrp 17193, tgpgrp 21630
gsumgroup sum df-gsum 15868 (𝐺 Σg 𝐹) Yes gsumval 17036, gsumwrev 17561
hashsize (of a set) df-hash 12931 (#‘𝐴) Yes hashgval 12933, hashfz1 12944, hashcl 12957
hbhypothesis builder (prefix) No hbxfrbi 1740, hbald 2025, hbequid 33011
hm(monoid, group, ring) homomorphism No ismhm 17102, isghm 17425, isrhm 18486
iinference (suffix) No eleq1i 2674, tcsni 8475
iimplication (suffix) No brwdomi 8329, infeq5i 8389
ididentity No biid 249
idmidempotent No anidm 673, tpidm13 4230
im, impimplication (label often omitted) df-im 13631 (𝐴𝐵) Yes iman 438, imnan 436, impbidd 198
imaimage df-ima 5037 (𝐴𝐵) Yes resima 5334, imaundi 5446
impimport No biimpa 499, impcom 444
inintersection df-in 3542 (𝐴𝐵) Yes elin 3753, incom 3762
infinfimum df-inf 8205 inf(ℝ+, ℝ*, < ) Yes fiinfcl 8263, infiso 8269
is...is (something a) ...? No isring 18316
jjoining, disjoining No jc 157, jaoi 392
lleft No olcd 406, simpl 471
mapmapping operation or set exponentiation df-map 7719 (𝐴𝑚 𝐵) Yes mapvalg 7727, elmapex 7737
matmatrix df-mat 19971 (𝑁 Mat 𝑅) Yes matval 19974, matring 20006
mdetdeterminant (of a square matrix) df-mdet 20148 (𝑁 maDet 𝑅) Yes mdetleib 20150, mdetrlin 20165
mgmmagma df-mgm 17007 Magma Yes mgmidmo 17024, mgmlrid 17031, ismgm 17008
mgpmultiplicative group df-mgp 18255 (mulGrp‘𝑅) Yes mgpress 18265, ringmgp 18318
mndmonoid df-mnd 17060 Mnd Yes mndass 17067, mndodcong 17726
mo"there exists at most one" df-mo 2458 ∃*𝑥𝜑 Yes eumo 2482, moim 2502
mpmodus ponens ax-mp 5 No mpd 15, mpi 20
mptmodus ponendo tollens No mptnan 1683, mptxor 1684
mptmaps-to notation for a function df-mpt 4635 (𝑥𝐴𝐵) Yes fconstmpt 5071, resmpt 5352
mpt2maps-to notation for an operation df-mpt2 6528 (𝑥𝐴, 𝑦𝐵𝐶) Yes mpt2mpt 6624, resmpt2 6630
mulmultiplication (see "t") df-mul 9800 (𝐴 · 𝐵) Yes mulcl 9872, divmul 10533, mulcom 9874, mulass 9876
n, notnot ¬ 𝜑 Yes nan 601, notnotr 123
nenot equaldf-ne 𝐴𝐵 Yes exmidne 2787, neeqtrd 2846
nelnot element ofdf-nel 𝐴𝐵 Yes neli 2880, nnel 2887
ne0not equal to zero (see n0) ≠ 0 No negne0d 10237, ine0 10312, gt0ne0 10338
nf "not free in" (prefix) No nfnd 1767
ngpnormed group df-ngp 22135 NrmGrp Yes isngp 22147, ngptps 22153
nmnorm (on a group or ring) df-nm 22134 (norm‘𝑊) Yes nmval 22141, subgnm 22181
nnpositive integers df-nn 10864 Yes nnsscn 10868, nncn 10871
nn0nonnegative integers df-n0 11136 0 Yes nnnn0 11142, nn0cn 11145
n0not the empty set (see ne0) ≠ ∅ No n0i 3874, vn0 3878, ssn0 3923
OLDold, obsolete (to be removed soon) No 19.43OLD 1798
opordered pair df-op 4127 𝐴, 𝐵 Yes dfopif 4327, opth 4861
oror df-or 383 (𝜑𝜓) Yes orcom 400, anor 508
otordered triple df-ot 4129 𝐴, 𝐵, 𝐶 Yes euotd 4887, fnotovb 6566
ovoperation value df-ov 6526 (𝐴𝐹𝐵) Yes fnotovb 6566, fnovrn 6680
pplus (see "add"), for all-constant theorems df-add 9799 (3 + 2) = 5 Yes 3p2e5 11003
pfxprefix df-pfx 40046 (𝑊 prefix 𝐿) Yes pfxlen 40055, ccatpfx 40073
pmPrincipia Mathematica No pm2.27 40
pmpartial mapping (operation) df-pm 7720 (𝐴pm 𝐵) Yes elpmi 7735, pmsspw 7751
prpair df-pr 4123 {𝐴, 𝐵} Yes elpr 4141, prcom 4206, prid1g 4234, prnz 4248
prm, primeprime (number) df-prm 15166 Yes 1nprm 15172, dvdsprime 15180
pssproper subset df-pss 3551 𝐴𝐵 Yes pssss 3659, sspsstri 3666
q rational numbers ("quotients") df-q 11617 Yes elq 11618
rright No orcd 405, simprl 789
rabrestricted class abstraction df-rab 2900 {𝑥𝐴𝜑} Yes rabswap 3093, df-oprab 6527
ralrestricted universal quantification df-ral 2896 𝑥𝐴𝜑 Yes ralnex 2970, ralrnmpt2 6647
rclreverse closure No ndmfvrcl 6110, nnarcl 7556
rereal numbers df-r 9798 Yes recn 9878, 0re 9892
relrelation df-rel 5031 Rel 𝐴 Yes brrelex 5066, relmpt2opab 7119
resrestriction df-res 5036 (𝐴𝐵) Yes opelres 5305, f1ores 6045
reurestricted existential uniqueness df-reu 2898 ∃!𝑥𝐴𝜑 Yes nfreud 3086, reurex 3132
rexrestricted existential quantification df-rex 2897 𝑥𝐴𝜑 Yes rexnal 2973, rexrnmpt2 6648
rmorestricted "at most one" df-rmo 2899 ∃*𝑥𝐴𝜑 Yes nfrmod 3087, nrexrmo 3135
rnrange df-rn 5035 ran 𝐴 Yes elrng 5220, rncnvcnv 5253
rng(unital) ring df-ring 18314 Ring Yes ringidval 18268, isring 18316, ringgrp 18317
rotrotation No 3anrot 1035, 3orrot 1036
seliminates need for syllogism (suffix) No ancoms 467
sb(proper) substitution (of a set) df-sb 1866 [𝑦 / 𝑥]𝜑 Yes spsbe 1869, sbimi 1871
sbc(proper) substitution of a class df-sbc 3398 [𝐴 / 𝑥]𝜑 Yes sbc2or 3406, sbcth 3412
scascalar df-sca 15726 (Scalar‘𝐻) Yes resssca 15796, mgpsca 18261
simpsimple, simplification No simpl 471, simp3r3 1163
snsingleton df-sn 4121 {𝐴} Yes eldifsn 4255
spspecialization No spsbe 1869, spei 2243
sssubset df-ss 3549 𝐴𝐵 Yes difss 3694
structstructure df-struct 15639 Struct Yes brstruct 15645, structfn 15650
subsubtract df-sub 10115 (𝐴𝐵) Yes subval 10119, subaddi 10215
supsupremum df-sup 8204 sup(𝐴, 𝐵, < ) Yes fisupcl 8231, supmo 8214
suppsupport (of a function) df-supp 7156 (𝐹 supp 𝑍) Yes ressuppfi 8157, mptsuppd 7178
swapswap (two parts within a theorem) No rabswap 3093, 2reuswap 3372
sylsyllogism syl 17 No 3syl 18
symsymmetric No df-symdif 3801, cnvsym 5412
symgsymmetric group df-symg 17563 (SymGrp‘𝐴) Yes symghash 17570, pgrpsubgsymg 17593
t times (see "mul"), for all-constant theorems df-mul 9800 (3 · 2) = 6 Yes 3t2e6 11022
ththeorem No nfth 1716, sbcth 3412, weth 9173
tptriple df-tp 4125 {𝐴, 𝐵, 𝐶} Yes eltpi 4171, tpeq1 4216
trtransitive No bitrd 266, biantr 967
trutrue df-tru 1477 Yes bitru 1486, truanfal 1497
ununion df-un 3540 (𝐴𝐵) Yes uneqri 3712, uncom 3714
unitunit (in a ring) df-unit 18407 (Unit‘𝑅) Yes isunit 18422, nzrunit 19030
vdisjoint variable conditions used when a not-free hypothesis (suffix) No spimv 2239
vv2 disjoint variables (in a not-free hypothesis) (suffix) No 19.23vv 1888
wweak (version of a theorem) (suffix) No ax11w 1992, spnfw 1913
wrdword df-word 13096 Word 𝑆 Yes iswrdb 13108, wrdfn 13116, ffz0iswrd 13129
xpcross product (Cartesian product) df-xp 5030 (𝐴 × 𝐵) Yes elxp 5041, opelxpi 5058, xpundi 5080
xreXtended reals df-xr 9930 * Yes ressxr 9935, rexr 9937, 0xr 9938
z integers (from German "Zahlen") df-z 11207 Yes elz 11208, zcn 11211
zn ring of integers mod 𝑛 df-zn 19615 (ℤ/nℤ‘𝑁) Yes znval 19643, zncrng 19653, znhash 19667
zringring of integers df-zring 19580 ring Yes zringbas 19585, zringcrng 19581
0, z slashed zero (empty set) (see n0) df-nul 3870 Yes n0i 3874, vn0 3878; snnz 4247, prnz 4248

(Contributed by DAW, 27-Dec-2016.) (New usage is discouraged.)

Hypothesis
Ref Expression
conventions-label.1 𝜑
Assertion
Ref Expression
conventions-label 𝜑

Proof of Theorem conventions-label
StepHypRef Expression
1 conventions-label.1 1 𝜑
Colors of variables: wff setvar class
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator