hash2iun

Description: The cardinality of a nested disjoint indexed union. (Contributed by AV, 9-Jan-2022)

	Ref	Expression
Hypotheses	hash2iun.a	$⊢ φ \to A \in Fin$
	hash2iun.b	$⊢ (φ \land x \in A) \to B \in Fin$
	hash2iun.c	$⊢ (φ \land x \in A \land y \in B) \to C \in Fin$
	hash2iun.da	$⊢ φ \to \underset{x \in A}{Disj} ⋃_{y \in B} C$
	hash2iun.db	$⊢ (φ \land x \in A) \to \underset{y \in B}{Disj} C$
Assertion	hash2iun	$⊢ φ \to \|⋃_{x \in A} ⋃_{y \in B} C\| = \sum_{x \in A} \sum_{y \in B} \|C\|$

Step	Hyp	Ref	Expression
1		hash2iun.a	$⊢ φ \to A \in Fin$
2		hash2iun.b	$⊢ (φ \land x \in A) \to B \in Fin$
3		hash2iun.c	$⊢ (φ \land x \in A \land y \in B) \to C \in Fin$
4		hash2iun.da	$⊢ φ \to \underset{x \in A}{Disj} ⋃_{y \in B} C$
5		hash2iun.db	$⊢ (φ \land x \in A) \to \underset{y \in B}{Disj} C$
6	3	3expa	$⊢ ((φ \land x \in A) \land y \in B) \to C \in Fin$
7	6	ralrimiva	$⊢ (φ \land x \in A) \to \forall y \in B C \in Fin$
8		iunfi	$⊢ (B \in Fin \land \forall y \in B C \in Fin) \to ⋃_{y \in B} C \in Fin$
9	2 7 8	syl2anc	$⊢ (φ \land x \in A) \to ⋃_{y \in B} C \in Fin$
10	1 9 4	hashiun	$⊢ φ \to \|⋃_{x \in A} ⋃_{y \in B} C\| = \sum_{x \in A} \|⋃_{y \in B} C\|$
11	2 6 5	hashiun	$⊢ (φ \land x \in A) \to \|⋃_{y \in B} C\| = \sum_{y \in B} \|C\|$
12	11	sumeq2dv	$⊢ φ \to \sum_{x \in A} \|⋃_{y \in B} C\| = \sum_{x \in A} \sum_{y \in B} \|C\|$
13	10 12	eqtrd	$⊢ φ \to \|⋃_{x \in A} ⋃_{y \in B} C\| = \sum_{x \in A} \sum_{y \in B} \|C\|$

Metamath Proof Explorer