Metamath Proof Explorer

Theorem hash2iun

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

Ref Expression
Hypotheses hash2iun.a ⊢ φ → A ∈ Fin
hash2iun.b ⊢ φ ∧ x ∈ A → B ∈ Fin
hash2iun.c ⊢ φ ∧ x ∈ A ∧ y ∈ B → C ∈ Fin
hash2iun.da ⊢ φ → Disj x ∈ A ⋃ y ∈ B C
hash2iun.db ⊢ φ ∧ x ∈ A → Disj y ∈ B C
Assertion hash2iun ⊢ φ → ⋃ x ∈ A ⋃ y ∈ B C = ∑ x ∈ A ∑ y ∈ B C

Proof

Step Hyp Ref Expression
1 hash2iun.a ⊢ φ → A ∈ Fin
2 hash2iun.b ⊢ φ ∧ x ∈ A → B ∈ Fin
3 hash2iun.c ⊢ φ ∧ x ∈ A ∧ y ∈ B → C ∈ Fin
4 hash2iun.da ⊢ φ → Disj x ∈ A ⋃ y ∈ B C
5 hash2iun.db ⊢ φ ∧ x ∈ A → Disj y ∈ B C
6 3 3expa ⊢ φ ∧ x ∈ A ∧ y ∈ B → C ∈ Fin
7 6 ralrimiva ⊢ φ ∧ x ∈ A → ∀ y ∈ B C ∈ Fin
8 iunfi ⊢ B ∈ Fin ∧ ∀ y ∈ B C ∈ Fin → ⋃ y ∈ B C ∈ Fin
9 2 7 8 syl2anc ⊢ φ ∧ x ∈ A → ⋃ y ∈ B C ∈ Fin
10 1 9 4 hashiun ⊢ φ → ⋃ x ∈ A ⋃ y ∈ B C = ∑ x ∈ A ⋃ y ∈ B C
11 2 6 5 hashiun ⊢ φ ∧ x ∈ A → ⋃ y ∈ B C = ∑ y ∈ B C
12 11 sumeq2dv ⊢ φ → ∑ x ∈ A ⋃ y ∈ B C = ∑ x ∈ A ∑ y ∈ B C
13 10 12 eqtrd ⊢ φ → ⋃ x ∈ A ⋃ y ∈ B C = ∑ x ∈ A ∑ y ∈ B C