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	|- ( ph -> .~ Er A )
	qshash.2	|- ( ph -> A e. Fin )
Assertion	qshash	|- ( ph -> ( # ` A ) = sum_ x e. ( A /. .~ ) ( # ` x ) )

Proof

Step	Hyp	Ref	Expression
1		qshash.1	|- ( ph -> .~ Er A )
2		qshash.2	|- ( ph -> A e. Fin )
3		erex	|- ( .~ Er A -> ( A e. Fin -> .~ e. _V ) )
4	1 2 3	sylc	|- ( ph -> .~ e. _V )
5	1 4	uniqs2	|- ( ph -> U. ( A /. .~ ) = A )
6	5	fveq2d	|- ( ph -> ( # ` U. ( A /. .~ ) ) = ( # ` A ) )
7		pwfi	|- ( A e. Fin <-> ~P A e. Fin )
8	2 7	sylib	|- ( ph -> ~P A e. Fin )
9	1	qsss	|- ( ph -> ( A /. .~ ) C_ ~P A )
10	8 9	ssfid	|- ( ph -> ( A /. .~ ) e. Fin )
11		elpwi	|- ( x e. ~P A -> x C_ A )
12		ssfi	|- ( ( A e. Fin /\ x C_ A ) -> x e. Fin )
13	12	ex	|- ( A e. Fin -> ( x C_ A -> x e. Fin ) )
14	2 11 13	syl2im	|- ( ph -> ( x e. ~P A -> x e. Fin ) )
15	14	ssrdv	|- ( ph -> ~P A C_ Fin )
16	9 15	sstrd	|- ( ph -> ( A /. .~ ) C_ Fin )
17		qsdisj2	|- ( .~ Er A -> Disj_ x e. ( A /. .~ ) x )
18	1 17	syl	|- ( ph -> Disj_ x e. ( A /. .~ ) x )
19	10 16 18	hashuni	|- ( ph -> ( # ` U. ( A /. .~ ) ) = sum_ x e. ( A /. .~ ) ( # ` x ) )
20	6 19	eqtr3d	|- ( ph -> ( # ` A ) = sum_ x e. ( A /. .~ ) ( # ` x ) )