Proof of The Number of Elements of a Disjoint Finite Union

Each result cited below is universally quantified over the data in its own statement, and is applied to the data named where it is cited.

Notation. By the laws of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §laws, the addition of $\mathbb{N}_{0}$ is associative and commutative, and $0$ is a neutral element of it, since $m+0=m$ and $0+m=m$ for $m\in\mathbb{N}_{0}$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §zero; so Sums and Products over a Finite Set and over an Interval §empty and Sums and Products over a Finite Set and over an Interval §subsets apply to it. As each $C_{i}$ is finite, $\#C_{i}\in\mathbb{N}_{0}$ is defined, and we let $c:I\to\mathbb{N}_{0}$ be the map $i\mapsto\#C_{i}$; the sum $\sum_{i\in I}\#C_{i}$ is that of $c$.

Let $J$ be a subset of $I$; it is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §subset. Writing $C$ for the family $(C_{i})_{i\in I}$, the restriction $C|_{J}$ is a function with domain $J\cap I=J$ and values $C_{j}$ at $j\in J$, by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction; so it is a family $(C_{j})_{j\in J}$ indexed by $J$. Let $U_{J}=\bigcup_{j\in J}C_{j}$ be its union, a set by The Union and Product of a Family of Sets Indexed by a Set, and the Intersection of a Family with an Inhabited Index Class, Are Sets §union and finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice §family-union; for every set $u$, $u\in U_{J}$ if and only if $u\in C_{j}$ for some $j\in J$. Let $s_{J}=\sum_{j\in J}\#C_{j}$, the sum of $c|_{J}$ as in Sums and Products over a Finite Set and over an Interval §subsets. For $J'\subseteq J$, the functions $(c|_{J})|_{J'}$ and $c|_{J'}$ both have domain $J'$ and value $\#C_{j}$ at each $j\in J'$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction, so they are equal by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality; hence the sum over $J'$ of $c|_{J}$ is $s_{J'}$. Note $U_{I}=\bigcup_{i\in I}C_{i}$ and $s_{I}=\sum_{i\in I}\#C_{i}$, since $C|_{I}=C$ and $c|_{I}=c$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality, each restriction having domain $I\cap I=I$ and the same values as the unrestricted map by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §restriction.

Step 1 (removing one index). Let $J\subseteq I$, $x\in J$ and $J'=J\setminus\{x\}$, a subset of $I$; $\{x\}$ is a set with only element $x$ by The Empty Set, the Unordered Pair and the Singleton §singleton. We show

$$\#J=\#J'+1,\qquad \#U_{J}=\#U_{J'}+\#C_{x},\qquad s_{J}=s_{J'}+\#C_{x}.$$

The first equation is Finite Sets: Removing an Element, Injective Self-Maps, Infinite Sets, Sets of Permutations, Pairs and Extended Tuples §remove-element, applied to the finite set $J$ and $x\in J$. Since $x\in J$, $J=J'\cup\{x\}$ and $J'\cap\{x\}=\emptyset$. For a set $u$: $u\in U_{J}$ if and only if $u\in C_{j}$ for some $j\in J'$ or $u\in C_{x}$, that is, if and only if $u\in U_{J'}\cup C_{x}$; so $U_{J}=U_{J'}\cup C_{x}$ by extensionality. If $u\in U_{J'}\cap C_{x}$, then $u\in C_{j}$ for some $j\in J'$, so $j\neq x$ and $u\in C_{j}\cap C_{x}=\emptyset$, which is impossible; so $U_{J'}\cap C_{x}=\emptyset$. As $U_{J'}$ and $C_{x}$ are finite, Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products §union gives $\#U_{J}=\#U_{J'}+\#C_{x}$. Finally, Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §disjoint-union, applied to the disjoint finite sets $J'$ and $\{x\}$ and to $c|_{J}:J'\cup\{x\}\to\mathbb{N}_{0}$, whose sum over $J'\cup\{x\}=J$ is the sum $s_{J}$ of $c|_{J}$, together with Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §singleton, applied to $c|_{\{x\}}$, and the remark on restrictions above, gives $s_{J}=s_{J'}+\sum_{j\in\{x\}}\#C_{j}=s_{J'}+\#C_{x}$.

Step 2 (the empty index set). If $J\subseteq I$ and $\#J=0$, then $J=\emptyset$ by Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products §empty. Then $U_{J}$ has no element, so $U_{J}=\emptyset$ and $\#U_{J}=0$ by Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products §empty; and $s_{J}=0$ by Sums and Products over a Finite Set and over an Interval §empty.

Step 3 (nonempty index sets). If $J\subseteq I$ and $\#J=n+1$ with $n\in\mathbb{N}_{0}$, then $J\neq\emptyset$: otherwise $n+1=0$ by Counting: Intervals, Empty Sets and Singletons, Injective Images, Subsets, Unions and Products §empty, so $1=0$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §zero-sum, contradicting $1\in\mathbb{N}=\mathbb{N}_{0}\setminus\{0\}$ from the setting. Hence $J$ has an element $x$, as $\emptyset$ is the only set with no element; and for $J'=J\setminus\{x\}$ Step 1 gives $\#J'+1=n+1$, so $\#J'=n$ by commutativity and Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §cancellation.

The clause disjoint-union. For $n\in\mathbb{N}_{0}$ let $P(n)$ state: for every subset $J$ of $I$ with $\#J=n$, $\#U_{J}=s_{J}$. $P(0)$ holds by Step 2, both sides being $0$. Assume $P(n)$, and let $J\subseteq I$ with $\#J=n+1$. By Step 3 there is $x\in J$ with $J'=J\setminus\{x\}$ of size $\#J'=n$, so $\#U_{J'}=s_{J'}$ by $P(n)$, and by Step 1

$$\#U_{J}=\#U_{J'}+\#C_{x}=s_{J'}+\#C_{x}=s_{J}.$$

So $P(n+1)$ holds, and by induction from $0$ on $\mathbb{N}_{0}$, from the setting, $P(n)$ holds for every $n\in\mathbb{N}_{0}$. Applying $P(\#I)$ to $J=I$ gives $\#\bigcup_{i\in I}C_{i}=\#U_{I}=s_{I}=\sum_{i\in I}\#C_{i}$.

The clause equal-blocks. Let $r\in\mathbb{N}_{0}$ with $\#C_{i}=r$ for every $i\in I$. For $n\in\mathbb{N}_{0}$ let $Q(n)$ state: for every subset $J$ of $I$ with $\#J=n$, $s_{J}=n\cdot r$. $Q(0)$ holds since $s_{J}=0$ by Step 2 and $0\cdot r=0$ by Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order §zero. Assume $Q(n)$, and let $J\subseteq I$ with $\#J=n+1$. By Step 3 there is $x\in J$ with $\#(J\setminus\{x\})=n$, so $s_{J\setminus\{x\}}=n\cdot r$ by $Q(n)$, and by Step 1

$$s_{J}=s_{J\setminus\{x\}}+\#C_{x}=n\cdot r+r=(n+1)\cdot r,$$

the last equality by Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order §successor, as $n+1$ is the successor of $n$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §plus-one. So $Q(n+1)$ holds, and by induction from $0$ on $\mathbb{N}_{0}$, $Q(n)$ holds for every $n\in\mathbb{N}_{0}$. Applying $Q(\#I)$ to $J=I$ and the clause disjoint-union shown above,

$$\#\bigcup_{i\in I}C_{i}=s_{I}=\#I\cdot r.$$