Theorem fipwss

Description: If a set is a family of subsets of some base set, then so is its finite intersection. (Contributed by Stefan O'Rear, 2-Aug-2015)

	Ref	Expression
Assertion	fipwss	$$⊢A\subseteq 𝒫X\to \mathrm{fi}\left(A\right)\subseteq 𝒫X$$

Proof

Step	Hyp	Ref	Expression
1		fiuni	$$⊢A\in \mathrm{V}\to \bigcup A=\bigcup \mathrm{fi}\left(A\right)$$
2	1	sseq1d	$$⊢A\in \mathrm{V}\to \left(\bigcup A\subseteq X\leftrightarrow \bigcup \mathrm{fi}\left(A\right)\subseteq X\right)$$
3		sspwuni	$$⊢A\subseteq 𝒫X\leftrightarrow \bigcup A\subseteq X$$
4		sspwuni	$$⊢\mathrm{fi}\left(A\right)\subseteq 𝒫X\leftrightarrow \bigcup \mathrm{fi}\left(A\right)\subseteq X$$
5	2 3 4	3bitr4g	$$⊢A\in \mathrm{V}\to \left(A\subseteq 𝒫X\leftrightarrow \mathrm{fi}\left(A\right)\subseteq 𝒫X\right)$$
6	5	biimpa	$$⊢\left(A\in \mathrm{V}\wedge A\subseteq 𝒫X\right)\to \mathrm{fi}\left(A\right)\subseteq 𝒫X$$
7		fvprc	$$⊢\neg A\in \mathrm{V}\to \mathrm{fi}\left(A\right)=\varnothing$$
8		0ss	$$⊢\varnothing \subseteq 𝒫X$$
9	7 8	eqsstrdi	$$⊢\neg A\in \mathrm{V}\to \mathrm{fi}\left(A\right)\subseteq 𝒫X$$
10	9	adantr	$$⊢\left(\neg A\in \mathrm{V}\wedge A\subseteq 𝒫X\right)\to \mathrm{fi}\left(A\right)\subseteq 𝒫X$$
11	6 10	pm2.61ian	$$⊢A\subseteq 𝒫X\to \mathrm{fi}\left(A\right)\subseteq 𝒫X$$