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