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 ⊢ φ → ∼ ˙ Er A
qshash.2 ⊢ φ → A ∈ Fin
Assertion qshash ⊢ φ → A = ∑ x ∈ A / ∼ ˙ x

Proof

Step Hyp Ref Expression
1 qshash.1 ⊢ φ → ∼ ˙ Er A
2 qshash.2 ⊢ φ → A ∈ Fin
3 erex ⊢ ∼ ˙ Er A → A ∈ Fin → ∼ ˙ ∈ V
4 1 2 3 sylc ⊢ φ → ∼ ˙ ∈ V
5 1 4 uniqs2 ⊢ φ → ⋃ A / ∼ ˙ = A
6 5 fveq2d ⊢ φ → ⋃ A / ∼ ˙ = A
7 pwfi ⊢ A ∈ Fin ↔ 𝒫 A ∈ Fin
8 2 7 sylib ⊢ φ → 𝒫 A ∈ Fin
9 1 qsss ⊢ φ → A / ∼ ˙ ⊆ 𝒫 A
10 8 9 ssfid ⊢ φ → A / ∼ ˙ ∈ Fin
11 elpwi ⊢ x ∈ 𝒫 A → x ⊆ A
12 ssfi ⊢ A ∈ Fin ∧ x ⊆ A → x ∈ Fin
13 12 ex ⊢ A ∈ Fin → x ⊆ A → x ∈ Fin
14 2 11 13 syl2im ⊢ φ → x ∈ 𝒫 A → x ∈ Fin
15 14 ssrdv ⊢ φ → 𝒫 A ⊆ Fin
16 9 15 sstrd ⊢ φ → A / ∼ ˙ ⊆ Fin
17 qsdisj2 ⊢ ∼ ˙ Er A → Disj x ∈ A / ∼ ˙ x
18 1 17 syl ⊢ φ → Disj x ∈ A / ∼ ˙ x
19 10 16 18 hashuni ⊢ φ → ⋃ A / ∼ ˙ = ∑ x ∈ A / ∼ ˙ x
20 6 19 eqtr3d ⊢ φ → A = ∑ x ∈ A / ∼ ˙ x