This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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