Metamath Proof Explorer

Theorem isfbas2

Description: The predicate " F is a filter base." (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Stefan O'Rear, 28-Jul-2015)

		Ref	Expression
	Assertion	isfbas2	$⊢ B \in A \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 \exists z \in F z \subseteq x \cap y)))$

Proof

Step	Hyp	Ref	Expression
1		isfbas	$⊢ B \in A \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)))$
2		elin	$⊢ z \in (F \cap 𝒫 (x \cap y)) \leftrightarrow (z \in F \land z \in 𝒫 (x \cap y))$
3		velpw	$⊢ z \in 𝒫 (x \cap y) \leftrightarrow z \subseteq x \cap y$
4	3	anbi2i	$⊢ (z \in F \land z \in 𝒫 (x \cap y)) \leftrightarrow (z \in F \land z \subseteq x \cap y)$
5	2 4	bitri	$⊢ z \in (F \cap 𝒫 (x \cap y)) \leftrightarrow (z \in F \land z \subseteq x \cap y)$
6	5	exbii	$⊢ \exists z z \in (F \cap 𝒫 (x \cap y)) \leftrightarrow \exists z (z \in F \land z \subseteq x \cap y)$
7		n0	$⊢ F \cap 𝒫 (x \cap y) \neq \emptyset \leftrightarrow \exists z z \in (F \cap 𝒫 (x \cap y))$
8		df-rex	$⊢ \exists z \in F z \subseteq x \cap y \leftrightarrow \exists z (z \in F \land z \subseteq x \cap y)$
9	6 7 8	3bitr4i	$⊢ F \cap 𝒫 (x \cap y) \neq \emptyset \leftrightarrow \exists z \in F z \subseteq x \cap y$
10	9	2ralbii	$⊢ \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset \leftrightarrow \forall x \in F \forall y \in F \exists z \in F z \subseteq x \cap y$
11	10	3anbi3i	$⊢ (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset) \leftrightarrow (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F \exists z \in F z \subseteq x \cap y)$
12	11	anbi2i	$⊢ (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)) \leftrightarrow (F \subseteq 𝒫 B \land (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F \exists z \in F z \subseteq x \cap y))$
13	1 12	bitrdi	$⊢ B \in A \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 \exists z \in F z \subseteq x \cap y)))$