Theorem hashuni

Description: The cardinality of a disjoint union. (Contributed by Mario Carneiro, 24-Jan-2015)

	Ref	Expression
Hypotheses	hashuni.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	hashuni.2	⊢ ( 𝜑 → 𝐴 ⊆ Fin )
	hashuni.3	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝑥 )
Assertion	hashuni	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝐴 ) = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		hashuni.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		hashuni.2	⊢ ( 𝜑 → 𝐴 ⊆ Fin )
3		hashuni.3	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝑥 )
4		uniiun	⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
5	4	fveq2i	⊢ ( ♯ ‘ ∪ 𝐴 ) = ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝑥 )
6	2	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ Fin )
7	1 6 3	hashiun	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝑥 ) = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
8	5 7	eqtrid	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝐴 ) = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )