Theorem iunpw

Description: An indexed union of a power class in terms of the power class of the union of its index. Part of Exercise 24(b) of Enderton p. 33. (Contributed by NM, 29-Nov-2003)

	Ref	Expression
Hypothesis	iunpw.1	$$⊢A\in \mathrm{V}$$
Assertion	iunpw	$$⊢\exists x\in Ax=\bigcup A\leftrightarrow 𝒫\bigcup A=\bigcup _{x\in A}𝒫x$$

Proof

Step	Hyp	Ref	Expression
1		iunpw.1	$$⊢A\in \mathrm{V}$$
2		sseq2	$$⊢x=\bigcup A\to \left(y\subseteq x\leftrightarrow y\subseteq \bigcup A\right)$$
3	2	biimprcd	$$⊢y\subseteq \bigcup A\to \left(x=\bigcup A\to y\subseteq x\right)$$
4	3	reximdv	$$⊢y\subseteq \bigcup A\to \left(\exists x\in Ax=\bigcup A\to \exists x\in Ay\subseteq x\right)$$
5	4	com12	$$⊢\exists x\in Ax=\bigcup A\to \left(y\subseteq \bigcup A\to \exists x\in Ay\subseteq x\right)$$
6		ssiun	$$⊢\exists x\in Ay\subseteq x\to y\subseteq \bigcup _{x\in A}x$$
7		uniiun	$$⊢\bigcup A=\bigcup _{x\in A}x$$
8	6 7	sseqtrrdi	$$⊢\exists x\in Ay\subseteq x\to y\subseteq \bigcup A$$
9	5 8	impbid1	$$⊢\exists x\in Ax=\bigcup A\to \left(y\subseteq \bigcup A\leftrightarrow \exists x\in Ay\subseteq x\right)$$
10		velpw	$$⊢y\in 𝒫\bigcup A\leftrightarrow y\subseteq \bigcup A$$
11		eliun	$$⊢y\in \bigcup _{x\in A}𝒫x\leftrightarrow \exists x\in Ay\in 𝒫x$$
12		velpw	$$⊢y\in 𝒫x\leftrightarrow y\subseteq x$$
13	12	rexbii	$$⊢\exists x\in Ay\in 𝒫x\leftrightarrow \exists x\in Ay\subseteq x$$
14	11 13	bitri	$$⊢y\in \bigcup _{x\in A}𝒫x\leftrightarrow \exists x\in Ay\subseteq x$$
15	9 10 14	3bitr4g	$$⊢\exists x\in Ax=\bigcup A\to \left(y\in 𝒫\bigcup A\leftrightarrow y\in \bigcup _{x\in A}𝒫x\right)$$
16	15	eqrdv	$$⊢\exists x\in Ax=\bigcup A\to 𝒫\bigcup A=\bigcup _{x\in A}𝒫x$$
17		ssid	$$⊢\bigcup A\subseteq \bigcup A$$
18	1	uniex	$$⊢\bigcup A\in \mathrm{V}$$
19	18	elpw	$$⊢\bigcup A\in 𝒫\bigcup A\leftrightarrow \bigcup A\subseteq \bigcup A$$
20		eleq2	$$⊢𝒫\bigcup A=\bigcup _{x\in A}𝒫x\to \left(\bigcup A\in 𝒫\bigcup A\leftrightarrow \bigcup A\in \bigcup _{x\in A}𝒫x\right)$$
21	19 20	bitr3id	$$⊢𝒫\bigcup A=\bigcup _{x\in A}𝒫x\to \left(\bigcup A\subseteq \bigcup A\leftrightarrow \bigcup A\in \bigcup _{x\in A}𝒫x\right)$$
22	17 21	mpbii	$$⊢𝒫\bigcup A=\bigcup _{x\in A}𝒫x\to \bigcup A\in \bigcup _{x\in A}𝒫x$$
23		eliun	$$⊢\bigcup A\in \bigcup _{x\in A}𝒫x\leftrightarrow \exists x\in A\bigcup A\in 𝒫x$$
24	22 23	sylib	$$⊢𝒫\bigcup A=\bigcup _{x\in A}𝒫x\to \exists x\in A\bigcup A\in 𝒫x$$
25		elssuni	$$⊢x\in A\to x\subseteq \bigcup A$$
26		elpwi	$$⊢\bigcup A\in 𝒫x\to \bigcup A\subseteq x$$
27	25 26	anim12i	$$⊢\left(x\in A\wedge \bigcup A\in 𝒫x\right)\to \left(x\subseteq \bigcup A\wedge \bigcup A\subseteq x\right)$$
28		eqss	$$⊢x=\bigcup A\leftrightarrow \left(x\subseteq \bigcup A\wedge \bigcup A\subseteq x\right)$$
29	27 28	sylibr	$$⊢\left(x\in A\wedge \bigcup A\in 𝒫x\right)\to x=\bigcup A$$
30	29	ex	$$⊢x\in A\to \left(\bigcup A\in 𝒫x\to x=\bigcup A\right)$$
31	30	reximia	$$⊢\exists x\in A\bigcup A\in 𝒫x\to \exists x\in Ax=\bigcup A$$
32	24 31	syl	$$⊢𝒫\bigcup A=\bigcup _{x\in A}𝒫x\to \exists x\in Ax=\bigcup A$$
33	16 32	impbii	$$⊢\exists x\in Ax=\bigcup A\leftrightarrow 𝒫\bigcup A=\bigcup _{x\in A}𝒫x$$