Theorem hashuni

Description: The cardinality of a disjoint union. (Contributed by Mario Carneiro, 24-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		hashuni.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		hashuni.2	$$⊢\phi \to A\subseteq \mathrm{Fin}$$
3		hashuni.3	$$⊢\phi \to \underset{x\in A}{Disj}x$$
4		uniiun	$$⊢\bigcup A=\bigcup _{x\in A}x$$
5	4	fveq2i	$$⊢\left|\bigcup A\right|=\left|\bigcup _{x\in A}x\right|$$
6	2	sselda	$$⊢\left(\phi \wedge x\in A\right)\to x\in \mathrm{Fin}$$
7	1 6 3	hashiun	$$⊢\phi \to \left|\bigcup _{x\in A}x\right|=\sum _{x\in A}\left|x\right|$$
8	5 7	syl5eq	$$⊢\phi \to \left|\bigcup A\right|=\sum _{x\in A}\left|x\right|$$