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 ) )