Theorem hash2iun

Description: The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022)

	Ref	Expression
Hypotheses	hash2iun.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	hash2iun.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ Fin )
	hash2iun.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ Fin )
	hash2iun.da	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 )
	hash2iun.db	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Disj 𝑦 ∈ 𝐵 𝐶 )
Assertion	hash2iun	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 ) = Σ 𝑥 ∈ 𝐴 Σ 𝑦 ∈ 𝐵 ( ♯ ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		hash2iun.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		hash2iun.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ Fin )
3		hash2iun.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ Fin )
4		hash2iun.da	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 )
5		hash2iun.db	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → Disj 𝑦 ∈ 𝐵 𝐶 )
6	3	3expa	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ Fin )
7	6	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐵 𝐶 ∈ Fin )
8		iunfi	⊢ ( ( 𝐵 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐵 𝐶 ∈ Fin ) → ∪ 𝑦 ∈ 𝐵 𝐶 ∈ Fin )
9	2 7 8	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∪ 𝑦 ∈ 𝐵 𝐶 ∈ Fin )
10	1 9 4	hashiun	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 ) = Σ 𝑥 ∈ 𝐴 ( ♯ ‘ ∪ 𝑦 ∈ 𝐵 𝐶 ) )
11	2 6 5	hashiun	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ♯ ‘ ∪ 𝑦 ∈ 𝐵 𝐶 ) = Σ 𝑦 ∈ 𝐵 ( ♯ ‘ 𝐶 ) )
12	11	sumeq2dv	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 ( ♯ ‘ ∪ 𝑦 ∈ 𝐵 𝐶 ) = Σ 𝑥 ∈ 𝐴 Σ 𝑦 ∈ 𝐵 ( ♯ ‘ 𝐶 ) )
13	10 12	eqtrd	⊢ ( 𝜑 → ( ♯ ‘ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 ) = Σ 𝑥 ∈ 𝐴 Σ 𝑦 ∈ 𝐵 ( ♯ ‘ 𝐶 ) )