Theorem intss2

Description: A nonempty intersection of a family of subsets of a class is included in that class. (Contributed by BJ, 7-Dec-2021)

	Ref	Expression
Assertion	intss2	$$⊢A\subseteq 𝒫X\to \left(A\ne \varnothing \to \bigcap A\subseteq X\right)$$

Proof

Step	Hyp	Ref	Expression
1		sspwuni	$$⊢A\subseteq 𝒫X\leftrightarrow \bigcup A\subseteq X$$
2	1	biimpi	$$⊢A\subseteq 𝒫X\to \bigcup A\subseteq X$$
3		intssuni	$$⊢A\ne \varnothing \to \bigcap A\subseteq \bigcup A$$
4		sstr	$$⊢\left(\bigcap A\subseteq \bigcup A\wedge \bigcup A\subseteq X\right)\to \bigcap A\subseteq X$$
5	4	expcom	$$⊢\bigcup A\subseteq X\to \left(\bigcap A\subseteq \bigcup A\to \bigcap A\subseteq X\right)$$
6	2 3 5	syl2im	$$⊢A\subseteq 𝒫X\to \left(A\ne \varnothing \to \bigcap A\subseteq X\right)$$