coiun1

Description: Composition with an indexed union. Proof analogous to that of coiun . (Contributed by RP, 20-Jun-2020)

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

Proof

Step	Hyp	Ref	Expression
1		relco	$⊢ Rel (⋃_{x \in C} A \circ B)$
2		reliun	$⊢ Rel ⋃_{x \in C} (A \circ B) \leftrightarrow \forall x \in C Rel (A \circ B)$
3		relco	$⊢ Rel (A \circ B)$
4	3	a1i	$⊢ x \in C \to Rel (A \circ B)$
5	2 4	mprgbir	$⊢ Rel ⋃_{x \in C} (A \circ B)$
6		eliun	$⊢ ⟨w, z⟩ \in ⋃_{x \in C} A \leftrightarrow \exists x \in C ⟨w, z⟩ \in A$
7		df-br	$⊢ w ⋃_{x \in C} A z \leftrightarrow ⟨w, z⟩ \in ⋃_{x \in C} A$
8		df-br	$⊢ w A z \leftrightarrow ⟨w, z⟩ \in A$
9	8	rexbii	$⊢ \exists x \in C w A z \leftrightarrow \exists x \in C ⟨w, z⟩ \in A$
10	6 7 9	3bitr4i	$⊢ w ⋃_{x \in C} A z \leftrightarrow \exists x \in C w A z$
11	10	anbi2i	$⊢ (y B w \land w ⋃_{x \in C} A z) \leftrightarrow (y B w \land \exists x \in C w A z)$
12		r19.42v	$⊢ \exists x \in C (y B w \land w A z) \leftrightarrow (y B w \land \exists x \in C w A z)$
13	11 12	bitr4i	$⊢ (y B w \land w ⋃_{x \in C} A z) \leftrightarrow \exists x \in C (y B w \land w A z)$
14	13	exbii	$⊢ \exists w (y B w \land w ⋃_{x \in C} A z) \leftrightarrow \exists w \exists x \in C (y B w \land w A z)$
15		rexcom4	$⊢ \exists x \in C \exists w (y B w \land w A z) \leftrightarrow \exists w \exists x \in C (y B w \land w A z)$
16	14 15	bitr4i	$⊢ \exists w (y B w \land w ⋃_{x \in C} A z) \leftrightarrow \exists x \in C \exists w (y B w \land w A z)$
17		vex	$⊢ y \in V$
18		vex	$⊢ z \in V$
19	17 18	opelco	$⊢ ⟨y, z⟩ \in (⋃_{x \in C} A \circ B) \leftrightarrow \exists w (y B w \land w ⋃_{x \in C} A z)$
20		eliun	$⊢ ⟨y, z⟩ \in ⋃_{x \in C} (A \circ B) \leftrightarrow \exists x \in C ⟨y, z⟩ \in (A \circ B)$
21	17 18	opelco	$⊢ ⟨y, z⟩ \in (A \circ B) \leftrightarrow \exists w (y B w \land w A z)$
22	21	rexbii	$⊢ \exists x \in C ⟨y, z⟩ \in (A \circ B) \leftrightarrow \exists x \in C \exists w (y B w \land w A z)$
23	20 22	bitri	$⊢ ⟨y, z⟩ \in ⋃_{x \in C} (A \circ B) \leftrightarrow \exists x \in C \exists w (y B w \land w A z)$
24	16 19 23	3bitr4i	$⊢ ⟨y, z⟩ \in (⋃_{x \in C} A \circ B) \leftrightarrow ⟨y, z⟩ \in ⋃_{x \in C} (A \circ B)$
25	1 5 24	eqrelriiv	$⊢ ⋃_{x \in C} A \circ B = ⋃_{x \in C} (A \circ B)$

Metamath Proof Explorer

Theorem coiun1

Proof