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:

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 , rexlimiva
ablAbelian group df-abl Abel Yes ablgrp , zringabl
absabsorption No ressabs
absabsolute value (of a complex number) df-abs ( absA ) Yes absval , absneg , abs1
adadding No adantr , ad2antlr
addadd (see "p") df-add ( A + B ) Yes addcl , addcom , addass
al"for all" A. x ph No alim , alex
ALTalternative/less preferred (suffix) No idALT
anand df-an ( ph /\ ps ) Yes anor , iman , imnan
antantecedent No adantr
assassociative No biass , orass , mulass
asymasymmetric, antisymmetric No intasym , asymref , posasymb
axaxiom No ax6dgen , ax1cn
bas, base base (set of an extensible structure) df-base ( BaseS ) Yes baseval , ressbas , cnfldbas
b, bibiconditional ("iff", "if and only if") df-bi ( ph <-> ps ) Yes impbid , sspwb
brbinary relation df-br A R B Yes brab1 , brun
cbvchange bound variable No cbvalivw , cbvrex
clclosure No ifclda , ovrcl , zaddcl
cncomplex numbers df-c CC Yes nnsscn , nncn
cnfldfield of complex numbers df-cnfld CCfld Yes cnfldbas , cnfldinv
cntzcentralizer df-cntz ( CntzM ) Yes cntzfval , dprdfcntz
cnvconverse df-cnv ` ``' A Yes opelcnvg , f1ocnv
cocomposition df-co ( A o. B ) Yes cnvco , fmptco
comcommutative No orcom , bicomi , eqcomi
concontradiction, contraposition No condan , con2d
csbclass substitution df-csb [_ A / x ]_ B Yes csbid , csbie2g
cygcyclic group df-cyg CycGrp Yes iscyg , zringcyg
ddeduction form (suffix) No idd , impbid
df(alternate) definition (prefix) No dfrel2 , dffn2
di, distrdistributive No andi , imdi , ordi , difindi , ndmovdistr
difclass difference df-dif ( A \ B ) Yes difss , difindi
divdivision df-div ( A / B ) Yes divcl , divval , divmul
dmdomain df-dm dom A Yes dmmpt , iswrddm0
e, eq, equequals (equ for setvars, eq for classes) df-cleq A = B Yes 2p2e4 , uneqri , equtr
edgedge df-edg ( Edg `G ) Yes edgopval , usgredgppr
elelement of A e. B Yes eldif , eldifsn , elssuni
enequinumerous df-en A ~B Yes domen , enfi
eu"there exists exactly one" eu6 E! x ph Yes euex , euabsn
exexists (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
expexport No expt , expcom
f"not free in" (suffix) No equs45f , sbf
ffunction df-f F : A --> B Yes fssxp , opelf
falfalse df-fal F. Yes bifal , falantru
fifinite intersection df-fi ( fiB ) Yes fival , inelfi
fi, finfinite df-fin Fin Yes isfi , snfi , onfin
fldfield (Note: there is an alternative definition Fld of a field, see df-fld ) df-field Field Yes isfld , fldidom
fnfunction with domain df-fn A Fn B Yes ffn , fndm
frgpfree group df-frgp ( freeGrpI ) Yes frgpval , frgpadd
fsuppfinitely supported function df-fsupp R finSupp Z Yes isfsupp , fdmfisuppfi , fsuppco
funfunction df-fun Fun F Yes funrel , ffun
fvfunction value df-fv ( FA ) Yes fvres , swrdfv
fzfinite set of sequential integers df-fz ( M ... N ) Yes fzval , eluzfz
fz0finite set of sequential nonnegative integers ( 0 ... N ) Yes nn0fz0 , fz0tp
fzohalf-open integer range df-fzo ( M ..^ N ) Yes elfzo , elfzofz
gmore general (suffix); eliminates "is a set" hypotheses No uniexg
grgraph No uhgrf , isumgr , usgrres1
grpgroup df-grp Grp Yes isgrp , tgpgrp
gsumgroup sum df-gsum ( G gsum F ) Yes gsumval , gsumwrev
hashsize (of a set) df-hash ( #A ) Yes hashgval , hashfz1 , hashcl
hbhypothesis builder (prefix) No hbxfrbi , hbald , hbequid
hm(monoid, group, ring) homomorphism No ismhm , isghm , isrhm
iinference (suffix) No eleq1i , tcsni
iimplication (suffix) No brwdomi , infeq5i
ididentity No biid
iedgindexed edge df-iedg ( iEdgG ) Yes iedgval0 , edgiedgb
idmidempotent No anidm , tpidm13
im, impimplication (label often omitted) df-im ( A -> B ) Yes iman , imnan , impbidd
imaimage df-ima ( A " B ) Yes resima , imaundi
impimport No biimpa , impcom
inintersection df-in ( A i^i B ) Yes elin , incom
infinfimum df-inf inf ( RR+ , RR* , < ) Yes fiinfcl , infiso
is...is (something a) ...? No isring
jjoining, disjoining No jc , jaoi
lleft No olcd , simpl
mapmapping operation or set exponentiation df-map ( A ^m B ) Yes mapvalg , elmapex
matmatrix df-mat ( N Mat R ) Yes matval , matring
mdetdeterminant (of a square matrix) df-mdet ( N maDet R ) Yes mdetleib , mdetrlin
mgmmagma df-mgm Magma Yes mgmidmo , mgmlrid , ismgm
mgpmultiplicative group df-mgp ( mulGrpR ) Yes mgpress , ringmgp
mndmonoid df-mnd Mnd Yes mndass , mndodcong
mo"there exists at most one" df-mo E* x ph Yes eumo , moim
mpmodus ponens ax-mp No mpd , mpi
mpomaps-to notation for an operation df-mpo ( x e. A , y e. B |-> C ) Yes mpompt , resmpo
mptmodus ponendo tollens No mptnan , mptxor
mptmaps-to notation for a function df-mpt ( x e. A |-> B ) Yes fconstmpt , resmpt
mpt2maps-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
mulmultiplication (see "t") df-mul ( A x. B ) Yes mulcl , divmul , mulcom , mulass
n, notnot -. ph Yes nan , notnotr
nenot equaldf-ne A =/= B Yes exmidne , neeqtrd
nelnot element ofdf-nel A e/ B Yes neli , nnel
ne0not equal to zero (see n0) =/= 0 No negne0d , ine0 , gt0ne0
nf "not free in" (prefix) No nfnd
ngpnormed group df-ngp NrmGrp Yes isngp , ngptps
nmnorm (on a group or ring) df-nm ( normW ) Yes nmval , subgnm
nnpositive integers df-nn NN Yes nnsscn , nncn
nn0nonnegative integers df-n0 NN0 Yes nnnn0 , nn0cn
n0not the empty set (see ne0) =/= (/) No n0i , vn0 , ssn0
OLDold, obsolete (to be removed soon) No 19.43OLD
onordinal number df-on A e. On Yes elon , 1on onelon
opordered pair df-op <. A , B >. Yes dfopif , opth
oror df-or ( ph \/ ps ) Yes orcom , anor
otordered triple df-ot <. A , B , C >. Yes euotd , fnotovb
ovoperation value df-ov ( A F B ) Yes fnotovb , fnovrn
pplus (see "add"), for all-constant theorems df-add ( 3 + 2 ) = 5 Yes 3p2e5
pfxprefix df-pfx ( W prefix L ) Yes pfxlen , ccatpfx
pmPrincipia Mathematica No pm2.27
pmpartial mapping (operation) df-pm ( A ^pm B ) Yes elpmi , pmsspw
prpair df-pr { A , B } Yes elpr , prcom , prid1g , prnz
prm, primeprime (number) df-prm Prime Yes 1nprm , dvdsprime
pssproper subset df-pss A C. B Yes pssss , sspsstri
q rational numbers ("quotients") df-q QQ Yes elq
rright No orcd , simprl
rabrestricted class abstraction df-rab { x e. A | ph } Yes rabswap , df-oprab
ralrestricted universal quantification df-ral A. x e. A ph Yes ralnex , ralrnmpo
rclreverse closure No ndmfvrcl , nnarcl
rereal numbers df-r RR Yes recn , 0re
relrelation df-rel Rel A Yes brrelex1 , relmpoopab
resrestriction df-res ` ( A |`B ) Yes opelres , f1ores
reurestricted existential uniqueness df-reu E! x e. A ph Yes nfreud , reurex
rexrestricted existential quantification df-rex E. x e. A ph Yes rexnal , rexrnmpo
rmorestricted "at most one" df-rmo E* x e. A ph Yes nfrmod , nrexrmo
rnrange df-rn ran A Yes elrng , rncnvcnv
rng(unital) ring df-ring Ring Yes ringidval , isring , ringgrp
rotrotation No 3anrot , 3orrot
seliminates 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
scascalar df-sca ( ScalarH ) Yes resssca , mgpsca
simpsimple, simplification No simpl , simp3r3
snsingleton df-sn { A } Yes eldifsn
spspecialization No spsbe , spei
sssubset df-ss A C B Yes difss
structstructure df-struct Struct Yes brstruct , structfn
subsubtract df-sub ( A - B ) Yes subval , subaddi
supsupremum df-sup sup ( A , B , < ) Yes fisupcl , supmo
suppsupport (of a function) df-supp ( F supp Z ) Yes ressuppfi , mptsuppd
swapswap (two parts within a theorem) No rabswap , 2reuswap
sylsyllogism syl No 3syl
symsymmetric No df-symdif , cnvsym
symgsymmetric 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
tptriple df-tp { A , B , C } Yes eltpi , tpeq1
trtransitive No bitrd , biantr
tru, t true, truth df-tru T. Yes bitru , truanfal , biimt
ununion df-un ( A u. B ) Yes uneqri , uncom
unitunit (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
wweak (version of a theorem) (suffix) No ax11w , spnfw
wrdword df-word Word S Yes iswrdb , wrdfn , ffz0iswrd
xpcross product (Cartesian product) df-xp ( A X. B ) Yes elxp , opelxpi , xpundi
xreXtended 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
zringring 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
|- ph
Assertion conventions-labels
|- ph

Proof

Step Hyp Ref Expression
1 conventions-labels.1
 |-  ph