Theorem pwpwuni

Description: Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	pwpwuni	$$⊢A\in V\to \left(A\in 𝒫𝒫B\leftrightarrow \bigcup A\in 𝒫B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elpwg	$$⊢A\in V\to \left(A\in 𝒫𝒫B\leftrightarrow A\subseteq 𝒫B\right)$$
2		sspwuni	$$⊢A\subseteq 𝒫B\leftrightarrow \bigcup A\subseteq B$$
3	2	a1i	$$⊢A\in V\to \left(A\subseteq 𝒫B\leftrightarrow \bigcup A\subseteq B\right)$$
4		uniexg	$$⊢A\in V\to \bigcup A\in \mathrm{V}$$
5		elpwg	$$⊢\bigcup A\in \mathrm{V}\to \left(\bigcup A\in 𝒫B\leftrightarrow \bigcup A\subseteq B\right)$$
6	4 5	syl	$$⊢A\in V\to \left(\bigcup A\in 𝒫B\leftrightarrow \bigcup A\subseteq B\right)$$
7	6	bicomd	$$⊢A\in V\to \left(\bigcup A\subseteq B\leftrightarrow \bigcup A\in 𝒫B\right)$$
8	1 3 7	3bitrd	$$⊢A\in V\to \left(A\in 𝒫𝒫B\leftrightarrow \bigcup A\in 𝒫B\right)$$