Theorem qshash

Description: The cardinality of a set with an equivalence relation is the sum of the cardinalities of its equivalence classes. (Contributed by Mario Carneiro, 16-Jan-2015)

	Ref	Expression
Hypotheses	qshash.1	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}A$$
	qshash.2	$$⊢\phi \to A\in \mathrm{Fin}$$
Assertion	qshash	$$⊢\phi \to \left|A\right|=\sum _{x\in A/\underset{\dot{}}{\sim }}\left|x\right|$$

Proof

Step	Hyp	Ref	Expression
1		qshash.1	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}A$$
2		qshash.2	$$⊢\phi \to A\in \mathrm{Fin}$$
3		erex	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}A\to \left(A\in \mathrm{Fin}\to \underset{\dot{}}{\sim }\in \mathrm{V}\right)$$
4	1 2 3	sylc	$$⊢\phi \to \underset{\dot{}}{\sim }\in \mathrm{V}$$
5	1 4	uniqs2	$$⊢\phi \to \bigcup \left(A/\underset{\dot{}}{\sim }\right)=A$$
6	5	fveq2d	$$⊢\phi \to \left|\bigcup \left(A/\underset{\dot{}}{\sim }\right)\right|=\left|A\right|$$
7		pwfi	$$⊢A\in \mathrm{Fin}\leftrightarrow 𝒫A\in \mathrm{Fin}$$
8	2 7	sylib	$$⊢\phi \to 𝒫A\in \mathrm{Fin}$$
9	1	qsss	$$⊢\phi \to A/\underset{\dot{}}{\sim }\subseteq 𝒫A$$
10	8 9	ssfid	$$⊢\phi \to A/\underset{\dot{}}{\sim }\in \mathrm{Fin}$$
11		elpwi	$$⊢x\in 𝒫A\to x\subseteq A$$
12		ssfi	$$⊢\left(A\in \mathrm{Fin}\wedge x\subseteq A\right)\to x\in \mathrm{Fin}$$
13	12	ex	$$⊢A\in \mathrm{Fin}\to \left(x\subseteq A\to x\in \mathrm{Fin}\right)$$
14	2 11 13	syl2im	$$⊢\phi \to \left(x\in 𝒫A\to x\in \mathrm{Fin}\right)$$
15	14	ssrdv	$$⊢\phi \to 𝒫A\subseteq \mathrm{Fin}$$
16	9 15	sstrd	$$⊢\phi \to A/\underset{\dot{}}{\sim }\subseteq \mathrm{Fin}$$
17		qsdisj2	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}A\to \underset{x\in A/\underset{\dot{}}{\sim }}{Disj}x$$
18	1 17	syl	$$⊢\phi \to \underset{x\in A/\underset{\dot{}}{\sim }}{Disj}x$$
19	10 16 18	hashuni	$$⊢\phi \to \left|\bigcup \left(A/\underset{\dot{}}{\sim }\right)\right|=\sum _{x\in A/\underset{\dot{}}{\sim }}\left|x\right|$$
20	6 19	eqtr3d	$$⊢\phi \to \left|A\right|=\sum _{x\in A/\underset{\dot{}}{\sim }}\left|x\right|$$