uniuni

Description: Expression for double union that moves union into a class abstraction. (Contributed by FL, 28-May-2007)

		Ref	Expression
	Assertion	uniuni	$⊢ ⋃ ⋃ A = ⋃ \{x \| \exists y (x = ⋃ y \land y \in A)\}$

Proof

Step	Hyp	Ref	Expression
1		eluni	$⊢ u \in ⋃ A \leftrightarrow \exists y (u \in y \land y \in A)$
2	1	anbi2i	$⊢ (z \in u \land u \in ⋃ A) \leftrightarrow (z \in u \land \exists y (u \in y \land y \in A))$
3	2	exbii	$⊢ \exists u (z \in u \land u \in ⋃ A) \leftrightarrow \exists u (z \in u \land \exists y (u \in y \land y \in A))$
4		19.42v	$⊢ \exists y (z \in u \land (u \in y \land y \in A)) \leftrightarrow (z \in u \land \exists y (u \in y \land y \in A))$
5	4	bicomi	$⊢ (z \in u \land \exists y (u \in y \land y \in A)) \leftrightarrow \exists y (z \in u \land (u \in y \land y \in A))$
6	5	exbii	$⊢ \exists u (z \in u \land \exists y (u \in y \land y \in A)) \leftrightarrow \exists u \exists y (z \in u \land (u \in y \land y \in A))$
7		excom	$⊢ \exists u \exists y (z \in u \land (u \in y \land y \in A)) \leftrightarrow \exists y \exists u (z \in u \land (u \in y \land y \in A))$
8		anass	$⊢ ((z \in u \land u \in y) \land y \in A) \leftrightarrow (z \in u \land (u \in y \land y \in A))$
9		ancom	$⊢ ((z \in u \land u \in y) \land y \in A) \leftrightarrow (y \in A \land (z \in u \land u \in y))$
10	8 9	bitr3i	$⊢ (z \in u \land (u \in y \land y \in A)) \leftrightarrow (y \in A \land (z \in u \land u \in y))$
11	10	2exbii	$⊢ \exists y \exists u (z \in u \land (u \in y \land y \in A)) \leftrightarrow \exists y \exists u (y \in A \land (z \in u \land u \in y))$
12		exdistr	$⊢ \exists y \exists u (y \in A \land (z \in u \land u \in y)) \leftrightarrow \exists y (y \in A \land \exists u (z \in u \land u \in y))$
13	7 11 12	3bitri	$⊢ \exists u \exists y (z \in u \land (u \in y \land y \in A)) \leftrightarrow \exists y (y \in A \land \exists u (z \in u \land u \in y))$
14		eluni	$⊢ z \in ⋃ y \leftrightarrow \exists u (z \in u \land u \in y)$
15	14	bicomi	$⊢ \exists u (z \in u \land u \in y) \leftrightarrow z \in ⋃ y$
16	15	anbi2i	$⊢ (y \in A \land \exists u (z \in u \land u \in y)) \leftrightarrow (y \in A \land z \in ⋃ y)$
17	16	exbii	$⊢ \exists y (y \in A \land \exists u (z \in u \land u \in y)) \leftrightarrow \exists y (y \in A \land z \in ⋃ y)$
18	6 13 17	3bitri	$⊢ \exists u (z \in u \land \exists y (u \in y \land y \in A)) \leftrightarrow \exists y (y \in A \land z \in ⋃ y)$
19		vuniex	$⊢ ⋃ y \in V$
20		eleq2	$⊢ v = ⋃ y \to (z \in v \leftrightarrow z \in ⋃ y)$
21	19 20	ceqsexv	$⊢ \exists v (v = ⋃ y \land z \in v) \leftrightarrow z \in ⋃ y$
22		exancom	$⊢ \exists v (v = ⋃ y \land z \in v) \leftrightarrow \exists v (z \in v \land v = ⋃ y)$
23	21 22	bitr3i	$⊢ z \in ⋃ y \leftrightarrow \exists v (z \in v \land v = ⋃ y)$
24	23	anbi2i	$⊢ (y \in A \land z \in ⋃ y) \leftrightarrow (y \in A \land \exists v (z \in v \land v = ⋃ y))$
25		19.42v	$⊢ \exists v (y \in A \land (z \in v \land v = ⋃ y)) \leftrightarrow (y \in A \land \exists v (z \in v \land v = ⋃ y))$
26		ancom	$⊢ (y \in A \land (z \in v \land v = ⋃ y)) \leftrightarrow ((z \in v \land v = ⋃ y) \land y \in A)$
27		anass	$⊢ ((z \in v \land v = ⋃ y) \land y \in A) \leftrightarrow (z \in v \land (v = ⋃ y \land y \in A))$
28	26 27	bitri	$⊢ (y \in A \land (z \in v \land v = ⋃ y)) \leftrightarrow (z \in v \land (v = ⋃ y \land y \in A))$
29	28	exbii	$⊢ \exists v (y \in A \land (z \in v \land v = ⋃ y)) \leftrightarrow \exists v (z \in v \land (v = ⋃ y \land y \in A))$
30	24 25 29	3bitr2i	$⊢ (y \in A \land z \in ⋃ y) \leftrightarrow \exists v (z \in v \land (v = ⋃ y \land y \in A))$
31	30	exbii	$⊢ \exists y (y \in A \land z \in ⋃ y) \leftrightarrow \exists y \exists v (z \in v \land (v = ⋃ y \land y \in A))$
32		excom	$⊢ \exists y \exists v (z \in v \land (v = ⋃ y \land y \in A)) \leftrightarrow \exists v \exists y (z \in v \land (v = ⋃ y \land y \in A))$
33		exdistr	$⊢ \exists v \exists y (z \in v \land (v = ⋃ y \land y \in A)) \leftrightarrow \exists v (z \in v \land \exists y (v = ⋃ y \land y \in A))$
34		vex	$⊢ v \in V$
35		eqeq1	$⊢ x = v \to (x = ⋃ y \leftrightarrow v = ⋃ y)$
36	35	anbi1d	$⊢ x = v \to ((x = ⋃ y \land y \in A) \leftrightarrow (v = ⋃ y \land y \in A))$
37	36	exbidv	$⊢ x = v \to (\exists y (x = ⋃ y \land y \in A) \leftrightarrow \exists y (v = ⋃ y \land y \in A))$
38	34 37	elab	$⊢ v \in \{x \| \exists y (x = ⋃ y \land y \in A)\} \leftrightarrow \exists y (v = ⋃ y \land y \in A)$
39	38	bicomi	$⊢ \exists y (v = ⋃ y \land y \in A) \leftrightarrow v \in \{x \| \exists y (x = ⋃ y \land y \in A)\}$
40	39	anbi2i	$⊢ (z \in v \land \exists y (v = ⋃ y \land y \in A)) \leftrightarrow (z \in v \land v \in \{x \| \exists y (x = ⋃ y \land y \in A)\})$
41	40	exbii	$⊢ \exists v (z \in v \land \exists y (v = ⋃ y \land y \in A)) \leftrightarrow \exists v (z \in v \land v \in \{x \| \exists y (x = ⋃ y \land y \in A)\})$
42	33 41	bitri	$⊢ \exists v \exists y (z \in v \land (v = ⋃ y \land y \in A)) \leftrightarrow \exists v (z \in v \land v \in \{x \| \exists y (x = ⋃ y \land y \in A)\})$
43	31 32 42	3bitri	$⊢ \exists y (y \in A \land z \in ⋃ y) \leftrightarrow \exists v (z \in v \land v \in \{x \| \exists y (x = ⋃ y \land y \in A)\})$
44	3 18 43	3bitri	$⊢ \exists u (z \in u \land u \in ⋃ A) \leftrightarrow \exists v (z \in v \land v \in \{x \| \exists y (x = ⋃ y \land y \in A)\})$
45	44	abbii	$⊢ \{z \| \exists u (z \in u \land u \in ⋃ A)\} = \{z \| \exists v (z \in v \land v \in \{x \| \exists y (x = ⋃ y \land y \in A)\})\}$
46		df-uni	$⊢ ⋃ ⋃ A = \{z \| \exists u (z \in u \land u \in ⋃ A)\}$
47		df-uni	$⊢ ⋃ \{x \| \exists y (x = ⋃ y \land y \in A)\} = \{z \| \exists v (z \in v \land v \in \{x \| \exists y (x = ⋃ y \land y \in A)\})\}$
48	45 46 47	3eqtr4i	$⊢ ⋃ ⋃ A = ⋃ \{x \| \exists y (x = ⋃ y \land y \in A)\}$

Metamath Proof Explorer

Theorem uniuni

Proof