Metamath Proof Explorer

Theorem iunxiun

Description: Separate an indexed union in the index of an indexed union. (Contributed by Mario Carneiro, 5-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		eliun	$⊢ x \in ⋃_{y \in A} B \leftrightarrow \exists y \in A x \in B$
2	1	anbi1i	$⊢ (x \in ⋃_{y \in A} B \land z \in C) \leftrightarrow (\exists y \in A x \in B \land z \in C)$
3		r19.41v	$⊢ \exists y \in A (x \in B \land z \in C) \leftrightarrow (\exists y \in A x \in B \land z \in C)$
4	2 3	bitr4i	$⊢ (x \in ⋃_{y \in A} B \land z \in C) \leftrightarrow \exists y \in A (x \in B \land z \in C)$
5	4	exbii	$⊢ \exists x (x \in ⋃_{y \in A} B \land z \in C) \leftrightarrow \exists x \exists y \in A (x \in B \land z \in C)$
6		rexcom4	$⊢ \exists y \in A \exists x (x \in B \land z \in C) \leftrightarrow \exists x \exists y \in A (x \in B \land z \in C)$
7	5 6	bitr4i	$⊢ \exists x (x \in ⋃_{y \in A} B \land z \in C) \leftrightarrow \exists y \in A \exists x (x \in B \land z \in C)$
8		df-rex	$⊢ \exists x \in ⋃_{y \in A} B z \in C \leftrightarrow \exists x (x \in ⋃_{y \in A} B \land z \in C)$
9		eliun	$⊢ z \in ⋃_{x \in B} C \leftrightarrow \exists x \in B z \in C$
10		df-rex	$⊢ \exists x \in B z \in C \leftrightarrow \exists x (x \in B \land z \in C)$
11	9 10	bitri	$⊢ z \in ⋃_{x \in B} C \leftrightarrow \exists x (x \in B \land z \in C)$
12	11	rexbii	$⊢ \exists y \in A z \in ⋃_{x \in B} C \leftrightarrow \exists y \in A \exists x (x \in B \land z \in C)$
13	7 8 12	3bitr4i	$⊢ \exists x \in ⋃_{y \in A} B z \in C \leftrightarrow \exists y \in A z \in ⋃_{x \in B} C$
14		eliun	$⊢ z \in ⋃_{x \in ⋃_{y \in A} B} C \leftrightarrow \exists x \in ⋃_{y \in A} B z \in C$
15		eliun	$⊢ z \in ⋃_{y \in A} ⋃_{x \in B} C \leftrightarrow \exists y \in A z \in ⋃_{x \in B} C$
16	13 14 15	3bitr4i	$⊢ z \in ⋃_{x \in ⋃_{y \in A} B} C \leftrightarrow z \in ⋃_{y \in A} ⋃_{x \in B} C$
17	16	eqriv	$⊢ ⋃_{x \in ⋃_{y \in A} B} C = ⋃_{y \in A} ⋃_{x \in B} C$