Let $X$ be a set and let $\mathcal{U}\in \mathcal{P}\webleft (\mathcal{P}\webleft (X\webright )\webright )$.
Since $\mathcal{P}\webleft (X\webright )$ is posetal, it suffices to prove the condition $\webleft (\star \webright )$. So let $\mathcal{U},\mathcal{V}\in \mathcal{P}\webleft (\mathcal{P}\webleft (X\webright )\webright )$ with $\mathcal{U}\subset \mathcal{V}$. We claim that
\[ \bigcap _{V\in \mathcal{V}}V\subset \bigcap _{U\in \mathcal{U}}U. \]
Indeed, if $x\in \bigcap _{V\in \mathcal{V}}V$, then $x\in V$ for all $V\in \mathcal{V}$. But since $\mathcal{U}\subset \mathcal{V}$, it follows that $x\in U$ for all $U\in \mathcal{U}$ as well. Thus $x\in \bigcap _{U\in \mathcal{U}}U$, which gives our desired inclusion.
We have
\begin{align*} \bigcap _{A\in \mathcal{A}}\webleft(\bigcap _{U\in A}U\webright) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{for each $A\in \mathcal{A}$,}\\ & \text{we have $x\in \bigcap _{U\in A}U$} \end{aligned} \webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{for each $A\in \mathcal{A}$ and each}\\ & \text{$U\in A$, we have $x\in U$} \end{aligned} \webright\} \\ & = \webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{for each $U\in \displaystyle \bigcup _{A\in \mathcal{A}}A$,}\\ & \text{we have $x\in U$} \end{aligned} \webright\} \\ & \subset \webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{for each $U\in \displaystyle \bigcap _{A\in \mathcal{A}}A$,}\\ & \text{we have $x\in U$} \end{aligned} \webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcap _{U\in {\scriptsize \displaystyle \bigcap _{A\in \mathcal{A}}A}}U. \end{align*}
Since $\mathcal{P}\webleft (X\webright )$ is posetal, naturality is automatic (). This finishes the proof.
We have
\begin{align*} \bigcap _{V\in \webleft\{ U\webright\} }V & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{for each $V\in \webleft\{ U\webright\} $,}\\ & \text{we have $x\in U$} \end{aligned} \webright\} \\ & = \webleft\{ x\in X\ \middle |\ x\in U \webright\} \\ & = U.\end{align*}
This finishes the proof.
If $U=\text{Ø}$, then we have
\begin{align*} \bigcap _{\webleft\{ u\webright\} \in \chi _{X}\webleft (U\webright )}\webleft\{ u\webright\} & = \bigcap _{\webleft\{ u\webright\} \in \text{Ø}}\webleft\{ u\webright\} \\ & = X,\end{align*}
so $\bigcap _{\webleft\{ u\webright\} \in \chi _{X}\webleft (U\webright )}\webleft\{ u\webright\} =X\neq \text{Ø}=U$. When $U$ is nonempty, we have two cases:
-
If $U$ is a singleton, say $U=\webleft\{ u\webright\} $, we have
\begin{align*} \bigcap _{\webleft\{ u\webright\} \in \chi _{X}\webleft (U\webright )}\webleft\{ u\webright\} & = \webleft\{ u\webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}U.\end{align*}
-
If $U$ contains at least two elements, we have
\begin{align*} \bigcap _{\webleft\{ u\webright\} \in \chi _{X}\webleft (U\webright )}\webleft\{ u\webright\} & = \text{Ø}\\ & \subset U.\end{align*}
This finishes the proof.
Item 5: Interaction With Unions I
We have
\begin{align*} \bigcap _{W\in \mathcal{U}\cup \mathcal{V}}W & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{for each $W\in \mathcal{U}\cup \mathcal{V}$,}\\ & \text{we have $x\in W$} \end{aligned} \webright\} \\ & = \webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{for each $W\in \mathcal{U}$ and each}\\ & \text{$W\in \mathcal{V}$, we have $x\in W$} \end{aligned} \webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{for each $W\in \mathcal{U}$,}\\ & \text{we have $x\in W$} \end{aligned} \webright\} \\ & \phantom{={}}\mkern 4mu\cap \webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{for each $W\in \mathcal{V}$,}\\ & \text{we have $x\in W$} \end{aligned} \webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft(\bigcap _{W\in \mathcal{U}}W\webright)\cap \webleft(\bigcap _{W\in \mathcal{V}}W\webright)\\ & = \webleft(\bigcap _{U\in \mathcal{U}}U\webright)\cap \webleft(\bigcap _{V\in \mathcal{V}}V\webright). \end{align*}
This finishes the proof.
Item 6: Interaction With Unions II
Omitted.
Item 7: Interaction With Intersections I
We have
\begin{align*} \webleft(\bigcap _{U\in \mathcal{U}}U\webright)\cap \webleft(\bigcap _{V\in \mathcal{V}}V\webright) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{for each $U\in \mathcal{U}$,}\\ & \text{we have $x\in U$} \end{aligned} \webright\} \\ & \phantom{={}}\mkern 4mu\cup \webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{for each $V\in \mathcal{V}$,}\\ & \text{we have $x\in V$} \end{aligned} \webright\} \\ & = \webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{for each $W\in \mathcal{U}\cap \mathcal{V}$,}\\ & \text{we have $x\in W$} \end{aligned} \webright\} \\ & \subset \webleft\{ x\in X\ \middle |\ \begin{aligned} & \text{for each $W\in \mathcal{U}\cup \mathcal{V}$,}\\ & \text{we have $x\in W$} \end{aligned} \webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcap _{W\in \mathcal{U}\cap \mathcal{V}}W.\end{align*}
Since $\mathcal{P}\webleft (X\webright )$ is posetal, naturality is automatic (). This finishes the proof.
Item 8: Interaction With Intersections II
Omitted.
Item 9: Interaction With Differences
Let $X=\webleft\{ 0,1\webright\} $, let $\mathcal{U}=\webleft\{ \webleft\{ 0\webright\} ,\webleft\{ 0,1\webright\} \webright\} $, and let $\mathcal{V}=\webleft\{ \webleft\{ 0\webright\} \webright\} $. We have
\begin{align*} \bigcap _{W\in \mathcal{U}\setminus \mathcal{V}}U & = \bigcap _{W\in \webleft\{ \webleft\{ 0,1\webright\} \webright\} }W\\ & = \webleft\{ 0,1\webright\} , \end{align*}
whereas
\begin{align*} \webleft(\bigcap _{U\in \mathcal{U}}U\webright)\setminus \webleft(\bigcap _{V\in \mathcal{V}}V\webright) & = \webleft\{ 0\webright\} \setminus \webleft\{ 0\webright\} \\ & = \text{Ø}. \end{align*}
Thus we have
\[ \bigcap _{W\in \mathcal{U}\setminus \mathcal{V}}W=\webleft\{ 0,1\webright\} \neq \text{Ø}=\webleft(\bigcap _{U\in \mathcal{U}}U\webright)\setminus \webleft(\bigcap _{V\in \mathcal{V}}V\webright). \]
This finishes the proof.
Item 10: Interaction With Complements I
Let $X=\webleft\{ 0,1\webright\} $ and let $\mathcal{U}=\webleft\{ \webleft\{ 0\webright\} \webright\} $. We have
\begin{align*} \bigcap _{W\in \mathcal{U}^{\textsf{c}}}U & = \bigcap _{W\in \webleft\{ \text{Ø},\webleft\{ 1\webright\} ,\webleft\{ 0,1\webright\} \webright\} }W\\ & = \text{Ø}, \end{align*}
whereas
\begin{align*} \bigcap _{U\in \mathcal{U}}U^{\textsf{c}} & = \webleft\{ 0\webright\} ^{\textsf{c}}\\ & = \webleft\{ 1\webright\} . \end{align*}
Thus we have
\[ \bigcap _{W\in \mathcal{U}^{\textsf{c}}}U=\text{Ø}\neq \webleft\{ 1\webright\} =\bigcap _{U\in \mathcal{U}}U^{\textsf{c}}. \]
This finishes the proof.
Item 11: Interaction With Complements II
This is a repetition of Item 12 of Proposition 2.3.6.1.2 and is proved there.
Item 12: Interaction With Complements III
This is a repetition of Item 11 of Proposition 2.3.6.1.2 and is proved there.
Item 13: Interaction With Symmetric Differences
Let $X=\webleft\{ 0,1\webright\} $, let $\mathcal{U}=\webleft\{ \webleft\{ 0,1\webright\} \webright\} $, and let $\mathcal{V}=\webleft\{ \webleft\{ 0\webright\} ,\webleft\{ 0,1\webright\} \webright\} $. We have
\begin{align*} \bigcap _{W\in \mathcal{U}\mathbin {\triangle }\mathcal{V}}W & = \bigcap _{W\in \webleft\{ \webleft\{ 0\webright\} \webright\} }W\\ & = \webleft\{ 0\webright\} , \end{align*}
whereas
\begin{align*} \webleft(\bigcap _{U\in \mathcal{U}}U\webright)\mathbin {\triangle }\webleft(\bigcap _{V\in \mathcal{V}}V\webright) & = \webleft\{ 0,1\webright\} \mathbin {\triangle }\webleft\{ 0\webright\} \\ & = \text{Ø}, \end{align*}
Thus we have
\[ \bigcap _{W\in \mathcal{U}\mathbin {\triangle }\mathcal{V}}W=\webleft\{ 0\webright\} \neq \text{Ø}=\webleft(\bigcap _{U\in \mathcal{U}}U\webright)\mathbin {\triangle }\webleft(\bigcap _{V\in \mathcal{V}}V\webright). \]
This finishes the proof.
Item 14: Interaction With Internal Homs I
This is a repetition of Item 10 of Proposition 2.4.7.1.3 and is proved there.
Item 15: Interaction With Internal Homs II
This is a repetition of Item 11 of Proposition 2.4.7.1.3 and is proved there.
Item 16: Interaction With Internal Homs III
This is a repetition of Item 12 of Proposition 2.4.7.1.3 and is proved there.
Item 17: Interaction With Direct Images
This is a repetition of Item 4 of Proposition 2.6.1.1.4 and is proved there.
Item 18: Interaction With Inverse Images
This is a repetition of Item 4 of Proposition 2.6.2.1.3 and is proved there.
Item 19: Interaction With Direct Images With Compact Support
This is a repetition of Item 4 of Proposition 2.6.3.1.6 and is proved there.
Item 20: Interaction With Unions of Families I
This is a repetition of Item 20 of Proposition 2.3.6.1.2 and is proved there.
Item 21: Interaction With Unions of Families II
This is a repetition of Item 21 of Proposition 2.3.6.1.2 and is proved there.