Metamath Proof Explorer


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 ) )