iuncom

Description: Commutation of indexed unions. (Contributed by NM, 18-Dec-2008)

		Ref	Expression
	Assertion	iuncom	$⊢ ⋃_{x \in A} ⋃_{y \in B} C = ⋃_{y \in B} ⋃_{x \in A} C$

Step	Hyp	Ref	Expression
1		rexcom	$⊢ \exists x \in A \exists y \in B z \in C \leftrightarrow \exists y \in B \exists x \in A z \in C$
2		eliun	$⊢ z \in ⋃_{y \in B} C \leftrightarrow \exists y \in B z \in C$
3	2	rexbii	$⊢ \exists x \in A z \in ⋃_{y \in B} C \leftrightarrow \exists x \in A \exists y \in B z \in C$
4		eliun	$⊢ z \in ⋃_{x \in A} C \leftrightarrow \exists x \in A z \in C$
5	4	rexbii	$⊢ \exists y \in B z \in ⋃_{x \in A} C \leftrightarrow \exists y \in B \exists x \in A z \in C$
6	1 3 5	3bitr4i	$⊢ \exists x \in A z \in ⋃_{y \in B} C \leftrightarrow \exists y \in B z \in ⋃_{x \in A} C$
7		eliun	$⊢ z \in ⋃_{x \in A} ⋃_{y \in B} C \leftrightarrow \exists x \in A z \in ⋃_{y \in B} C$
8		eliun	$⊢ z \in ⋃_{y \in B} ⋃_{x \in A} C \leftrightarrow \exists y \in B z \in ⋃_{x \in A} C$
9	6 7 8	3bitr4i	$⊢ z \in ⋃_{x \in A} ⋃_{y \in B} C \leftrightarrow z \in ⋃_{y \in B} ⋃_{x \in A} C$
10	9	eqriv	$⊢ ⋃_{x \in A} ⋃_{y \in B} C = ⋃_{y \in B} ⋃_{x \in A} C$

Metamath Proof Explorer