fbsspw

Description: A filter base on a set is a subset of the power set. (Contributed by Stefan O'Rear, 28-Jul-2015)

		Ref	Expression
	Assertion	fbsspw	$⊢ F \in fBas (B) \to F \subseteq 𝒫 B$

Step	Hyp	Ref	Expression
1		elfvdm	$⊢ F \in fBas (B) \to B \in dom fBas$
2		isfbas	$⊢ B \in dom fBas \to (F \in fBas (B) \leftrightarrow (F \subseteq 𝒫 B \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset)))$
3	1 2	syl	$⊢ F \in fBas (B) \to (F \in fBas (B) \leftrightarrow (F \subseteq 𝒫 B \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset)))$
4	3	ibi	$⊢ F \in fBas (B) \to (F \subseteq 𝒫 B \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset))$
5	4	simpld	$⊢ F \in fBas (B) \to F \subseteq 𝒫 B$

Metamath Proof Explorer