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 e. Fin -> ( # ` A ) = sum_ a e. A 1 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fsumconst1 | |- ( A e. Fin -> sum_ a e. A 1 = ( # ` A ) ) |
|
| 2 | 1 | eqcomd | |- ( A e. Fin -> ( # ` A ) = sum_ a e. A 1 ) |