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 
|- ( ph -> A e. Fin )
hash2iun.b 
|- ( ( ph /\ x e. A ) -> B e. Fin )
hash2iun.c 
|- ( ( ph /\ x e. A /\ y e. B ) -> C e. Fin )
hash2iun.da 
|- ( ph -> Disj_ x e. A U_ y e. B C )
hash2iun.db 
|- ( ( ph /\ x e. A ) -> Disj_ y e. B C )
Assertion hash2iun 
|- ( ph -> ( # ` U_ x e. A U_ y e. B C ) = sum_ x e. A sum_ y e. B ( # ` C ) )

Proof

Step Hyp Ref Expression
1 hash2iun.a 
 |-  ( ph -> A e. Fin )
2 hash2iun.b 
 |-  ( ( ph /\ x e. A ) -> B e. Fin )
3 hash2iun.c 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> C e. Fin )
4 hash2iun.da 
 |-  ( ph -> Disj_ x e. A U_ y e. B C )
5 hash2iun.db 
 |-  ( ( ph /\ x e. A ) -> Disj_ y e. B C )
6 3 3expa 
 |-  ( ( ( ph /\ x e. A ) /\ y e. B ) -> C e. Fin )
7 6 ralrimiva 
 |-  ( ( ph /\ x e. A ) -> A. y e. B C e. Fin )
8 iunfi 
 |-  ( ( B e. Fin /\ A. y e. B C e. Fin ) -> U_ y e. B C e. Fin )
9 2 7 8 syl2anc 
 |-  ( ( ph /\ x e. A ) -> U_ y e. B C e. Fin )
10 1 9 4 hashiun 
 |-  ( ph -> ( # ` U_ x e. A U_ y e. B C ) = sum_ x e. A ( # ` U_ y e. B C ) )
11 2 6 5 hashiun 
 |-  ( ( ph /\ x e. A ) -> ( # ` U_ y e. B C ) = sum_ y e. B ( # ` C ) )
12 11 sumeq2dv 
 |-  ( ph -> sum_ x e. A ( # ` U_ y e. B C ) = sum_ x e. A sum_ y e. B ( # ` C ) )
13 10 12 eqtrd 
 |-  ( ph -> ( # ` U_ x e. A U_ y e. B C ) = sum_ x e. A sum_ y e. B ( # ` C ) )