Theorem hashunif

Description: The cardinality of a disjoint finite union of finite sets. Cf. hashuni . (Contributed by Thierry Arnoux, 17-Feb-2017)

	Ref	Expression
Hypotheses	hashiunf.1	⊢ Ⅎ 𝑥 𝜑
	hashiunf.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	hashunif.4	⊢ ( 𝜑 → 𝐴 ⊆ Fin )
	hashunif.5	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝑥 )
Assertion	hashunif	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝐴 ) = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		hashiunf.1	⊢ Ⅎ 𝑥 𝜑
2		hashiunf.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		hashunif.4	⊢ ( 𝜑 → 𝐴 ⊆ Fin )
4		hashunif.5	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝑥 )
5		uniiun	⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
6	5	fveq2i	⊢ ( ♯ ‘ ∪ 𝐴 ) = ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝑥 )
7	3	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ Fin )
8		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
9	8	cbvdisjv	⊢ ( Disj 𝑥 ∈ 𝐴 𝑥 ↔ Disj 𝑦 ∈ 𝐴 𝑦 )
10	4 9	sylib	⊢ ( 𝜑 → Disj 𝑦 ∈ 𝐴 𝑦 )
11	2 7 10	hashiun	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑦 ∈ 𝐴 𝑦 ) = Σ 𝑦 ∈ 𝐴 ( ♯ ‘ 𝑦 ) )
12	8	cbviunv	⊢ ∪ 𝑥 ∈ 𝐴 𝑥 = ∪ 𝑦 ∈ 𝐴 𝑦
13	12	a1i	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝑥 = ∪ 𝑦 ∈ 𝐴 𝑦 )
14	13	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝑥 ) = ( ♯ ‘ ∪ 𝑦 ∈ 𝐴 𝑦 ) )
15		fveq2	⊢ ( 𝑥 = 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
16	15	cbvsumv	⊢ Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = Σ 𝑦 ∈ 𝐴 ( ♯ ‘ 𝑦 )
17	16	a1i	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) = Σ 𝑦 ∈ 𝐴 ( ♯ ‘ 𝑦 ) )
18	11 14 17	3eqtr4d	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 𝑥 ) = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )
19	6 18	eqtrid	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝐴 ) = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ 𝑥 ) )