Metamath Proof Explorer

Theorem conventions-labels

Description:

The following gives conventions used in the Metamath Proof Explorer (MPE, set.mm) regarding labels. For other conventions, see conventions and links therein.

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 "rgen.1 $e |- ( x e. A -> ph ) $." or letters corresponding to the (main) class variable used in the hypothesis, e.g. for mdet0 : "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 and stirling .

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 .

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 , and the restricted quantifier version of Theorem 21 from Section 19 of Margaris p. 90 is labeled r19.21 .

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... . Furthermore, the underscore "_" should not be used. Finally, only lower case characters should be used (except the special suffixes OLD, ALT, and ALTV mentioned in bullet point "Suffixes"), at least in main set.mm (exceptions are tolerated in mathboxes).

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 ( A \ B ) is defined in df-dif , and thus its syntax label fragment is "dif". Similarly, the subclass relation A C_ B has syntax label fragment "ss" because it is defined in df-ss . Most theorem names follow from these fragments, for example, the theorem proving ( A \ B ) C_ A involves a class difference ("dif") of a subset ("ss"), and thus is labeled difss . There are many other syntax label fragments, e.g., singleton construct { A } has syntax label fragment "sn" (because it is defined in df-sn ), and the pair construct { A , B } has fragment "pr" ( from df-pr ). 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 A e. B does not have a df-NAME definition; in this case its syntax label fragment is "el". Thus, because the theorem beginning with ( A e. ( B \ { C } ) uses is-element-of ("el") of a class difference ("dif") of a singleton ("sn"), it is labeled eldifsn . An "n" is often used for negation ( -. ), e.g., nan .

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 CC (even though its definition is in df-c ) and "re" represents real numbers RR ( definition df-r ). The empty set (/) often uses fragment 0, even though it is defined in df-nul . The syntax construct ( A + B ) usually uses the fragment "add" (which is consistent with df-add ), but "p" is used as the fragment for constant theorems. Equality ( A = B ) often uses "e" as the fragment. As a result, "two plus two equals four" is labeled 2p2e4 .

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 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 ) we have value cosval and closure coscl .

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 and syl 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 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 (inference, deduction, or closed form, see above). Additionally, we sometimes suffix with "v" the label of a theorem adding a disjoint variable condition, as in 19.21v versus 19.21 . This often permits to prove the result using fewer axioms, and/or to eliminate a nonfreeness hypothesis (such as F/ x ph in 19.21 ). If no constraint is put on axiom use, then the v-version can be proved from the original theorem using nfv . If two (resp. three) such disjoint variable conditions are added, then the suffix "vv" (resp. "vvv") is used, e.g., exlimivv . 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 derived from eu6 . 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 . 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 ) -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 ( cbval in deduction form "d" with a not free variable replaced by a disjoint variable condition "v" with a conjunction as antecedent "a"). As a general rule, the suffixes for the theorem forms ("i", "d" or "g") should be the first of multiple suffixes, as for example in vtocldf .

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 , syl2anc ), commutes (e.g., biimpac )
- d : theorem in deduction form
- f : theorem with a hypothesis such as F/ x ph
- 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 that is eliminated)
- t : theorem in closed form (not having an "is a set" antecedent)
- 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 (mathbox only)
- OLD : old/obsolete version of a theorem (or proof) or definition

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.

Abbreviation	Mnenomic	Source	Expression	Syntax?	Example(s)
a	and (suffix)			No	biimpa , rexlimiva
abl	Abelian group	df-abl	Abel	Yes	ablgrp , zringabl
abs	absorption			No	ressabs
abs	absolute value (of a complex number)	df-abs	( absA )	Yes	absval , absneg , abs1
ad	adding			No	adantr , ad2antlr
add	add (see "p")	df-add	( A + B )	Yes	addcl , addcom , addass
al	"for all"		A. x ph	No	alim , alex
ALT	alternative/less preferred (suffix)			No	idALT
an	and	df-an	( ph /\ ps )	Yes	anor , iman , imnan
ant	antecedent			No	adantr
ass	associative			No	biass , orass , mulass
asym	asymmetric, antisymmetric			No	intasym , asymref , posasymb
ax	axiom			No	ax6dgen , ax1cn
bas, base	base (set of an extensible structure)	df-base	( BaseS )	Yes	baseval , ressbas , cnfldbas
b, bi	biconditional ("iff", "if and only if")	df-bi	( ph <-> ps )	Yes	impbid , sspwb
br	binary relation	df-br	A R B	Yes	brab1 , brun
cbv	change bound variable			No	cbvalivw , cbvrex
cl	closure			No	ifclda , ovrcl , zaddcl
cn	complex numbers	df-c	CC	Yes	nnsscn , nncn
cnfld	field of complex numbers	df-cnfld	CCfld	Yes	cnfldbas , cnfldinv
cntz	centralizer	df-cntz	( CntzM )	Yes	cntzfval , dprdfcntz
cnv	converse	df-cnv	` ``' A	Yes	opelcnvg , f1ocnv
co	composition	df-co	( A o. B )	Yes	cnvco , fmptco
com	commutative			No	orcom , bicomi , eqcomi
con	contradiction, contraposition			No	condan , con2d
csb	class substitution	df-csb	[_ A / x ]_ B	Yes	csbid , csbie2g
cyg	cyclic group	df-cyg	CycGrp	Yes	iscyg , zringcyg
d	deduction form (suffix)			No	idd , impbid
df	(alternate) definition (prefix)			No	dfrel2 , dffn2
di, distr	distributive			No	andi , imdi , ordi , difindi , ndmovdistr
dif	class difference	df-dif	( A \ B )	Yes	difss , difindi
div	division	df-div	( A / B )	Yes	divcl , divval , divmul
dm	domain	df-dm	dom A	Yes	dmmpt , iswrddm0
e, eq, equ	equals (equ for setvars, eq for classes)	df-cleq	A = B	Yes	2p2e4 , uneqri , equtr
edg	edge	df-edg	( Edg `G )	Yes	edgopval , usgredgppr
el	element of		A e. B	Yes	eldif , eldifsn , elssuni
en	equinumerous	df-en	A ~B	Yes	domen , enfi
eu	"there exists exactly one"	eu6	E! x ph	Yes	euex , euabsn
ex	exists (i.e. is a set)		e.V	No	brrelex1 , 0ex
ex, e	"there exists (at least one)"	df-ex	E. x ph	Yes	exim , alex
exp	export			No	expt , expcom
f	"not free in" (suffix)			No	equs45f , sbf
f	function	df-f	F : A --> B	Yes	fssxp , opelf
fal	false	df-fal	F.	Yes	bifal , falantru
fi	finite intersection	df-fi	( fiB )	Yes	fival , inelfi
fi, fin	finite	df-fin	Fin	Yes	isfi , snfi , onfin
fld	field (Note: there is an alternative definition Fld of a field, see df-fld )	df-field	Field	Yes	isfld , fldidom
fn	function with domain	df-fn	A Fn B	Yes	ffn , fndm
frgp	free group	df-frgp	( freeGrpI )	Yes	frgpval , frgpadd
fsupp	finitely supported function	df-fsupp	R finSupp Z	Yes	isfsupp , fdmfisuppfi , fsuppco
fun	function	df-fun	Fun F	Yes	funrel , ffun
fv	function value	df-fv	( FA )	Yes	fvres , swrdfv
fz	finite set of sequential integers	df-fz	( M ... N )	Yes	fzval , eluzfz
fz0	finite set of sequential nonnegative integers		( 0 ... N )	Yes	nn0fz0 , fz0tp
fzo	half-open integer range	df-fzo	( M ..^ N )	Yes	elfzo , elfzofz
g	more general (suffix); eliminates "is a set" hypotheses			No	uniexg
gr	graph			No	uhgrf , isumgr , usgrres1
grp	group	df-grp	Grp	Yes	isgrp , tgpgrp
gsum	group sum	df-gsum	( G gsum F )	Yes	gsumval , gsumwrev
hash	size (of a set)	df-hash	( #A )	Yes	hashgval , hashfz1 , hashcl
hb	hypothesis builder (prefix)			No	hbxfrbi , hbald , hbequid
hm	(monoid, group, ring) homomorphism			No	ismhm , isghm , isrhm
i	inference (suffix)			No	eleq1i , tcsni
i	implication (suffix)			No	brwdomi , infeq5i
id	identity			No	biid
iedg	indexed edge	df-iedg	( iEdgG )	Yes	iedgval0 , edgiedgb
idm	idempotent			No	anidm , tpidm13
im, imp	implication (label often omitted)	df-im	( A -> B )	Yes	iman , imnan , impbidd
ima	image	df-ima	( A " B )	Yes	resima , imaundi
imp	import			No	biimpa , impcom
in	intersection	df-in	( A i^i B )	Yes	elin , incom
inf	infimum	df-inf	inf ( RR+ , RR* , < )	Yes	fiinfcl , infiso
is...	is (something a) ...?			No	isring
j	joining, disjoining			No	jc , jaoi
l	left			No	olcd , simpl
map	mapping operation or set exponentiation	df-map	( A ^m B )	Yes	mapvalg , elmapex
mat	matrix	df-mat	( N Mat R )	Yes	matval , matring
mdet	determinant (of a square matrix)	df-mdet	( N maDet R )	Yes	mdetleib , mdetrlin
mgm	magma	df-mgm	Magma	Yes	mgmidmo , mgmlrid , ismgm
mgp	multiplicative group	df-mgp	( mulGrpR )	Yes	mgpress , ringmgp
mnd	monoid	df-mnd	Mnd	Yes	mndass , mndodcong
mo	"there exists at most one"	df-mo	E* x ph	Yes	eumo , moim
mp	modus ponens	ax-mp		No	mpd , mpi
mpo	maps-to notation for an operation	df-mpo	( x e. A , y e. B \|-> C )	Yes	mpompt , resmpo
mpt	modus ponendo tollens			No	mptnan , mptxor
mpt	maps-to notation for a function	df-mpt	( x e. A \|-> B )	Yes	fconstmpt , resmpt
mpt2	maps-to notation for an operation (deprecated). We are in the process of replacing mpt2 with mpo in labels.	df-mpo	( x e. A , y e. B \|-> C )	Yes	mpompt , resmpo
mul	multiplication (see "t")	df-mul	( A x. B )	Yes	mulcl , divmul , mulcom , mulass
n, not	not		-. ph	Yes	nan , notnotr
ne	not equal	df-ne	A =/= B	Yes	exmidne , neeqtrd
nel	not element of	df-nel	A e/ B	Yes	neli , nnel
ne0	not equal to zero (see n0)		=/= 0	No	negne0d , ine0 , gt0ne0
nf	"not free in" (prefix)			No	nfnd
ngp	normed group	df-ngp	NrmGrp	Yes	isngp , ngptps
nm	norm (on a group or ring)	df-nm	( normW )	Yes	nmval , subgnm
nn	positive integers	df-nn	NN	Yes	nnsscn , nncn
nn0	nonnegative integers	df-n0	NN0	Yes	nnnn0 , nn0cn
n0	not the empty set (see ne0)		=/= (/)	No	n0i , vn0 , ssn0
OLD	old, obsolete (to be removed soon)			No	19.43OLD
on	ordinal number	df-on	A e. On	Yes	elon , 1on onelon
op	ordered pair	df-op	<. A , B >.	Yes	dfopif , opth
or	or	df-or	( ph \/ ps )	Yes	orcom , anor
ot	ordered triple	df-ot	<. A , B , C >.	Yes	euotd , fnotovb
ov	operation value	df-ov	( A F B )	Yes	fnotovb , fnovrn
p	plus (see "add"), for all-constant theorems	df-add	( 3 + 2 ) = 5	Yes	3p2e5
pfx	prefix	df-pfx	( W prefix L )	Yes	pfxlen , ccatpfx
pm	Principia Mathematica			No	pm2.27
pm	partial mapping (operation)	df-pm	( A ^pm B )	Yes	elpmi , pmsspw
pr	pair	df-pr	{ A , B }	Yes	elpr , prcom , prid1g , prnz
prm, prime	prime (number)	df-prm	Prime	Yes	1nprm , dvdsprime
pss	proper subset	df-pss	A C. B	Yes	pssss , sspsstri
q	rational numbers ("quotients")	df-q	QQ	Yes	elq
r	right			No	orcd , simprl
rab	restricted class abstraction	df-rab	{ x e. A \| ph }	Yes	rabswap , df-oprab
ral	restricted universal quantification	df-ral	A. x e. A ph	Yes	ralnex , ralrnmpo
rcl	reverse closure			No	ndmfvrcl , nnarcl
re	real numbers	df-r	RR	Yes	recn , 0re
rel	relation	df-rel	Rel A	Yes	brrelex1 , relmpoopab
res	restriction	df-res	` ( A \|`B )	Yes	opelres , f1ores
reu	restricted existential uniqueness	df-reu	E! x e. A ph	Yes	nfreud , reurex
rex	restricted existential quantification	df-rex	E. x e. A ph	Yes	rexnal , rexrnmpo
rmo	restricted "at most one"	df-rmo	E* x e. A ph	Yes	nfrmod , nrexrmo
rn	range	df-rn	ran A	Yes	elrng , rncnvcnv
rng	(unital) ring	df-ring	Ring	Yes	ringidval , isring , ringgrp
rot	rotation			No	3anrot , 3orrot
s	eliminates need for syllogism (suffix)			No	ancoms
sb	(proper) substitution (of a set)	df-sb	[ y / x ] ph	Yes	spsbe , sbimi
sbc	(proper) substitution of a class	df-sbc	[. A / x ]. ph	Yes	sbc2or , sbcth
sca	scalar	df-sca	( ScalarH )	Yes	resssca , mgpsca
simp	simple, simplification			No	simpl , simp3r3
sn	singleton	df-sn	{ A }	Yes	eldifsn
sp	specialization			No	spsbe , spei
ss	subset	df-ss	A C B	Yes	difss
struct	structure	df-struct	Struct	Yes	brstruct , structfn
sub	subtract	df-sub	( A - B )	Yes	subval , subaddi
sup	supremum	df-sup	sup ( A , B , < )	Yes	fisupcl , supmo
supp	support (of a function)	df-supp	( F supp Z )	Yes	ressuppfi , mptsuppd
swap	swap (two parts within a theorem)			No	rabswap , 2reuswap
syl	syllogism	syl		No	3syl
sym	symmetric			No	df-symdif , cnvsym
symg	symmetric group	df-symg	( SymGrpA )	Yes	symghash , pgrpsubgsymg
t	times (see "mul"), for all-constant theorems	df-mul	( 3 x. 2 ) = 6	Yes	3t2e6
th, t	theorem			No	nfth , sbcth , weth , ancomst
tp	triple	df-tp	{ A , B , C }	Yes	eltpi , tpeq1
tr	transitive			No	bitrd , biantr
tru, t	true, truth	df-tru	T.	Yes	bitru , truanfal , biimt
un	union	df-un	( A u. B )	Yes	uneqri , uncom
unit	unit (in a ring)	df-unit	( UnitR )	Yes	isunit , nzrunit
v	setvar (especially for specializations of theorems when a class is replaced by a setvar variable)		x	Yes	cv , vex , velpw , vtoclf
v	disjoint variable condition used in place of nonfreeness hypothesis (suffix)			No	spimv
vtx	vertex	df-vtx	( VtxG )	Yes	vtxval0 , opvtxov
vv	two disjoint variable conditions used in place of nonfreeness hypotheses (suffix)			No	19.23vv
w	weak (version of a theorem) (suffix)			No	ax11w , spnfw
wrd	word	df-word	Word S	Yes	iswrdb , wrdfn , ffz0iswrd
xp	cross product (Cartesian product)	df-xp	( A X. B )	Yes	elxp , opelxpi , xpundi
xr	eXtended reals	df-xr	RR*	Yes	ressxr , rexr , 0xr
z	integers (from German "Zahlen")	df-z	ZZ	Yes	elz , zcn
zn	ring of integers mod N	df-zn	( Z/nZN )	Yes	znval , zncrng , znhash
zring	ring of integers	df-zring	ZZring	Yes	zringbas , zringcrng
0, z	slashed zero (empty set)	df-nul	(/)	Yes	n0i , vn0 ; snnz , prnz

(Contributed by the Metamath team, 27-Dec-2016) Date of last revision. (Revised by the Metamath team, 22-Sep-2022) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	conventions-labels.1	$⊢ φ$
	Assertion	conventions-labels	$⊢ φ$

Proof

Step	Hyp	Ref	Expression
1		conventions-labels.1	$⊢ φ$