This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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