Theorem iinpw

Description: The power class of an intersection in terms of indexed intersection. Exercise 24(a) of Enderton p. 33. (Contributed by NM, 29-Nov-2003)

	Ref	Expression
Assertion	iinpw	$$⊢𝒫\bigcap A=\bigcap _{x\in A}𝒫x$$

Proof

Step	Hyp	Ref	Expression
1		ssint	$$⊢y\subseteq \bigcap A\leftrightarrow \forall x\in Ay\subseteq x$$
2		velpw	$$⊢y\in 𝒫x\leftrightarrow y\subseteq x$$
3	2	ralbii	$$⊢\forall x\in Ay\in 𝒫x\leftrightarrow \forall x\in Ay\subseteq x$$
4	1 3	bitr4i	$$⊢y\subseteq \bigcap A\leftrightarrow \forall x\in Ay\in 𝒫x$$
5		velpw	$$⊢y\in 𝒫\bigcap A\leftrightarrow y\subseteq \bigcap A$$
6		eliin	$$⊢y\in \mathrm{V}\to \left(y\in \bigcap _{x\in A}𝒫x\leftrightarrow \forall x\in Ay\in 𝒫x\right)$$
7	6	elv	$$⊢y\in \bigcap _{x\in A}𝒫x\leftrightarrow \forall x\in Ay\in 𝒫x$$
8	4 5 7	3bitr4i	$$⊢y\in 𝒫\bigcap A\leftrightarrow y\in \bigcap _{x\in A}𝒫x$$
9	8	eqriv	$$⊢𝒫\bigcap A=\bigcap _{x\in A}𝒫x$$