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 fi (A) \subseteq 𝒫 X$

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

Metamath Proof Explorer