Theorem 1enum

Description: The Fundamental Theorem of Enumeration. According to Doron Zeilberger (in https://sites.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/enu.pdf ), this theorem was independently discovered by several anonymous cave-dwellers.

Zeilberger also states that "While this formula is still useful after all these years, enumerating specific finite sets is no longer considered mathematics. A genuine mathematical fact has to incorporate infinitely many facts". Fortunately, theorems in Metamath are actually theorem schemes that correspond to an infinite number of object-language theorems, so this concern does not apply to us.

See 1enumen for a version that applies to all sets, and see 1enumcard for a version that uses the cardinality function.

(Contributed by BTernaryTau, 26-Jun-2026)

	Ref	Expression
Assertion	1enum	$$⊢A\in \mathrm{Fin}\to \left|A\right|=\sum _{a\in A}1$$

Proof

Step	Hyp	Ref	Expression
1		fsumconst1	$$⊢A\in \mathrm{Fin}\to \sum _{a\in A}1=\left|A\right|$$
2	1	eqcomd	$$⊢A\in \mathrm{Fin}\to \left|A\right|=\sum _{a\in A}1$$