Theorem iunpwss

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

	Ref	Expression
Assertion	iunpwss	$$⊢\bigcup _{x\in A}𝒫x\subseteq 𝒫\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		ssiun	$$⊢\exists x\in Ay\subseteq x\to y\subseteq \bigcup _{x\in A}x$$
2		eliun	$$⊢y\in \bigcup _{x\in A}𝒫x\leftrightarrow \exists x\in Ay\in 𝒫x$$
3		velpw	$$⊢y\in 𝒫x\leftrightarrow y\subseteq x$$
4	3	rexbii	$$⊢\exists x\in Ay\in 𝒫x\leftrightarrow \exists x\in Ay\subseteq x$$
5	2 4	bitri	$$⊢y\in \bigcup _{x\in A}𝒫x\leftrightarrow \exists x\in Ay\subseteq x$$
6		velpw	$$⊢y\in 𝒫\bigcup A\leftrightarrow y\subseteq \bigcup A$$
7		uniiun	$$⊢\bigcup A=\bigcup _{x\in A}x$$
8	7	sseq2i	$$⊢y\subseteq \bigcup A\leftrightarrow y\subseteq \bigcup _{x\in A}x$$
9	6 8	bitri	$$⊢y\in 𝒫\bigcup A\leftrightarrow y\subseteq \bigcup _{x\in A}x$$
10	1 5 9	3imtr4i	$$⊢y\in \bigcup _{x\in A}𝒫x\to y\in 𝒫\bigcup A$$
11	10	ssriv	$$⊢\bigcup _{x\in A}𝒫x\subseteq 𝒫\bigcup A$$