Theorem 1enumcard

Description: The Fundamental Theorem of Enumeration (see https://sites.math.rutgers.edu/~zeilberg/mamarim/mamarimPDF/enu.pdf ), extended to all sets.

The expression U_ x e. A ( { x } X. B ) can be thought of as expressing an indexed disjoint union |_| x e. A B where each B has its elements tagged with the set x that generated it. See the comment directly before undjudom for context on disjoint union as a representation of cardinal addition.

This theorem does not depend on AC, but it is only meaningful for numerable sets. See 1enumen for a version that is meaningful for non-numerable sets, and see 1enum for a version that uses an explicit sum of complex number 1s.

(Contributed by BTernaryTau, 26-Jun-2026)

	Ref	Expression
Assertion	1enumcard	$$⊢A\in \mathrm{V}\to \mathrm{card}\left(A\right)=\mathrm{card}\left(\bigcup _{x\in A}\left(\left\{x\right\}\times 1_{𝑜}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		1enumen	$$⊢A\in \mathrm{V}\to A\approx \bigcup _{x\in A}\left(\left\{x\right\}\times 1_{𝑜}\right)$$
2		carden2b	$$⊢A\approx \bigcup _{x\in A}\left(\left\{x\right\}\times 1_{𝑜}\right)\to \mathrm{card}\left(A\right)=\mathrm{card}\left(\bigcup _{x\in A}\left(\left\{x\right\}\times 1_{𝑜}\right)\right)$$
3	1 2	syl	$$⊢A\in \mathrm{V}\to \mathrm{card}\left(A\right)=\mathrm{card}\left(\bigcup _{x\in A}\left(\left\{x\right\}\times 1_{𝑜}\right)\right)$$