Theorem 1enumkard

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 is not limited to numerable sets, but it also does not depend on AC. See 1enumen for a version that uses equinumerosity , 1enumcard for a version that uses the card function, and 1enum for a version that uses an explicit sum of complex number 1s.

(Contributed by BTernaryTau, 4-Jul-2026)

	Ref	Expression
Assertion	1enumkard	|- ( A e. _V -> ( kard ` A ) = ( kard ` U_ x e. A ( { x } X. 1o ) ) )

Proof

Step	Hyp	Ref	Expression
1		1enumen	|- ( A e. _V -> A ~~ U_ x e. A ( { x } X. 1o ) )
2		kardenir	|- ( A ~~ U_ x e. A ( { x } X. 1o ) -> ( kard ` A ) = ( kard ` U_ x e. A ( { x } X. 1o ) ) )
3	1 2	syl	|- ( A e. _V -> ( kard ` A ) = ( kard ` U_ x e. A ( { x } X. 1o ) ) )