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 𝐴 )
	qshash.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
Assertion	qshash	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = Σ 𝑥 ∈ ( 𝐴 / ∼ ) ( ♯ ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		qshash.1	⊢ ( 𝜑 → ∼ Er 𝐴 )
2		qshash.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		erex	⊢ ( ∼ Er 𝐴 → ( 𝐴 ∈ Fin → ∼ ∈ V ) )
4	1 2 3	sylc	⊢ ( 𝜑 → ∼ ∈ V )
5	1 4	uniqs2	⊢ ( 𝜑 → ∪ ( 𝐴 / ∼ ) = 𝐴 )
6	5	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ ∪ ( 𝐴 / ∼ ) ) = ( ♯ ‘ 𝐴 ) )
7		pwfi	⊢ ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin )
8	2 7	sylib	⊢ ( 𝜑 → 𝒫 𝐴 ∈ Fin )
9	1	qsss	⊢ ( 𝜑 → ( 𝐴 / ∼ ) ⊆ 𝒫 𝐴 )
10	8 9	ssfid	⊢ ( 𝜑 → ( 𝐴 / ∼ ) ∈ Fin )
11		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
12		ssfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑥 ⊆ 𝐴 ) → 𝑥 ∈ Fin )
13	12	ex	⊢ ( 𝐴 ∈ Fin → ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ Fin ) )
14	2 11 13	syl2im	⊢ ( 𝜑 → ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ Fin ) )
15	14	ssrdv	⊢ ( 𝜑 → 𝒫 𝐴 ⊆ Fin )
16	9 15	sstrd	⊢ ( 𝜑 → ( 𝐴 / ∼ ) ⊆ Fin )
17		qsdisj2	⊢ ( ∼ Er 𝐴 → Disj 𝑥 ∈ ( 𝐴 / ∼ ) 𝑥 )
18	1 17	syl	⊢ ( 𝜑 → Disj 𝑥 ∈ ( 𝐴 / ∼ ) 𝑥 )
19	10 16 18	hashuni	⊢ ( 𝜑 → ( ♯ ‘ ∪ ( 𝐴 / ∼ ) ) = Σ 𝑥 ∈ ( 𝐴 / ∼ ) ( ♯ ‘ 𝑥 ) )
20	6 19	eqtr3d	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = Σ 𝑥 ∈ ( 𝐴 / ∼ ) ( ♯ ‘ 𝑥 ) )