Theorem 1enumen

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 1enumcard for a version that uses the cardinality function, and see 1enum for a version that uses an explicit sum of complex number 1s.

(Contributed by BTernaryTau, 26-Jun-2026)

	Ref	Expression
Assertion	1enumen	⊢ ( 𝐴 ∈ V → 𝐴 ≈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 1o ) )

Proof

Step	Hyp	Ref	Expression
1		xp1en	⊢ ( 𝐴 ∈ V → ( 𝐴 × 1o ) ≈ 𝐴 )
2	1	ensymd	⊢ ( 𝐴 ∈ V → 𝐴 ≈ ( 𝐴 × 1o ) )
3		iunid	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴
4	3	xpeq1i	⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑥 } × 1o ) = ( 𝐴 × 1o )
5		xpiundir	⊢ ( ∪ 𝑥 ∈ 𝐴 { 𝑥 } × 1o ) = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 1o )
6	4 5	eqtr3i	⊢ ( 𝐴 × 1o ) = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 1o )
7	2 6	breqtrdi	⊢ ( 𝐴 ∈ V → 𝐴 ≈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 1o ) )