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 ( 𝜑𝐴 ∈ 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 ( 𝜑 → ( ♯ ‘ 𝑥𝐴 𝑦𝐵 𝐶 ) = Σ 𝑥𝐴 Σ 𝑦𝐵 ( ♯ ‘ 𝐶 ) )