This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpiundir

Description: Distributive law for Cartesian product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014)

		Ref	Expression
	Assertion	xpiundir	$⊢ ⋃_{x \in A} B \times C = ⋃_{x \in A} (B \times C)$

Proof

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