Theorem hashunif

Description: The cardinality of a disjoint finite union of finite sets. Cf. hashuni . (Contributed by Thierry Arnoux, 17-Feb-2017)

	Ref	Expression
Hypotheses	hashiunf.1	$$⊢Ⅎx\phi$$
	hashiunf.3	$$⊢\phi \to A\in \mathrm{Fin}$$
	hashunif.4	$$⊢\phi \to A\subseteq \mathrm{Fin}$$
	hashunif.5	$$⊢\phi \to \underset{x\in A}{Disj}x$$
Assertion	hashunif	$$⊢\phi \to \left|\bigcup A\right|=\sum _{x\in A}\left|x\right|$$

Proof

Step	Hyp	Ref	Expression
1		hashiunf.1	$$⊢Ⅎx\phi$$
2		hashiunf.3	$$⊢\phi \to A\in \mathrm{Fin}$$
3		hashunif.4	$$⊢\phi \to A\subseteq \mathrm{Fin}$$
4		hashunif.5	$$⊢\phi \to \underset{x\in A}{Disj}x$$
5		uniiun	$$⊢\bigcup A=\bigcup _{x\in A}x$$
6	5	fveq2i	$$⊢\left|\bigcup A\right|=\left|\bigcup _{x\in A}x\right|$$
7	3	sselda	$$⊢\left(\phi \wedge y\in A\right)\to y\in \mathrm{Fin}$$
8		id	$$⊢x=y\to x=y$$
9	8	cbvdisjv	$$⊢\underset{x\in A}{Disj}x\leftrightarrow \underset{y\in A}{Disj}y$$
10	4 9	sylib	$$⊢\phi \to \underset{y\in A}{Disj}y$$
11	2 7 10	hashiun	$$⊢\phi \to \left|\bigcup _{y\in A}y\right|=\sum _{y\in A}\left|y\right|$$
12	8	cbviunv	$$⊢\bigcup _{x\in A}x=\bigcup _{y\in A}y$$
13	12	a1i	$$⊢\phi \to \bigcup _{x\in A}x=\bigcup _{y\in A}y$$
14	13	fveq2d	$$⊢\phi \to \left|\bigcup _{x\in A}x\right|=\left|\bigcup _{y\in A}y\right|$$
15		fveq2	$$⊢x=y\to \left|x\right|=\left|y\right|$$
16	15	cbvsumv	$$⊢\sum _{x\in A}\left|x\right|=\sum _{y\in A}\left|y\right|$$
17	16	a1i	$$⊢\phi \to \sum _{x\in A}\left|x\right|=\sum _{y\in A}\left|y\right|$$
18	11 14 17	3eqtr4d	$$⊢\phi \to \left|\bigcup _{x\in A}x\right|=\sum _{x\in A}\left|x\right|$$
19	6 18	eqtrid	$$⊢\phi \to \left|\bigcup A\right|=\sum _{x\in A}\left|x\right|$$