isfbas

Description: The predicate " F is a filter base." Note that some authors require filter bases to be closed under pairwise intersections, but that is not necessary under our definition. One advantage of this definition is that tails in a directed set form a filter base under our meaning. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Mario Carneiro, 28-Jul-2015)

		Ref	Expression
	Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		df-fbas	$⊢ fBas = (z \in V ⟼ \{w \in 𝒫 𝒫 z \| (w \neq \emptyset \land \emptyset \notin w \land \forall x \in w \forall y \in w w \cap 𝒫 (x \cap y) \neq \emptyset)\})$
2		neeq1	$⊢ w = F \to (w \neq \emptyset \leftrightarrow F \neq \emptyset)$
3		neleq2	$⊢ w = F \to (\emptyset \notin w \leftrightarrow \emptyset \notin F)$
4		ineq1	$⊢ w = F \to w \cap 𝒫 (x \cap y) = F \cap 𝒫 (x \cap y)$
5	4	neeq1d	$⊢ w = F \to (w \cap 𝒫 (x \cap y) \neq \emptyset \leftrightarrow F \cap 𝒫 (x \cap y) \neq \emptyset)$
6	5	raleqbi1dv	$⊢ w = F \to (\forall y \in w w \cap 𝒫 (x \cap y) \neq \emptyset \leftrightarrow \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset)$
7	6	raleqbi1dv	$⊢ w = F \to (\forall x \in w \forall y \in w w \cap 𝒫 (x \cap y) \neq \emptyset \leftrightarrow \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset)$
8	2 3 7	3anbi123d	$⊢ w = F \to ((w \neq \emptyset \land \emptyset \notin w \land \forall x \in w \forall y \in w w \cap 𝒫 (x \cap y) \neq \emptyset) \leftrightarrow (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset))$
9	8	adantl	$⊢ (z = B \land w = F) \to ((w \neq \emptyset \land \emptyset \notin w \land \forall x \in w \forall y \in w w \cap 𝒫 (x \cap y) \neq \emptyset) \leftrightarrow (F \neq \emptyset \land \emptyset \notin F \land \forall x \in F \forall y \in F F \cap 𝒫 (x \cap y) \neq \emptyset))$
10		pweq	$⊢ z = B \to 𝒫 z = 𝒫 B$
11	10	pweqd	$⊢ z = B \to 𝒫 𝒫 z = 𝒫 𝒫 B$
12		vpwex	$⊢ 𝒫 z \in V$
13	12	pwex	$⊢ 𝒫 𝒫 z \in V$
14	13	a1i	$⊢ z \in V \to 𝒫 𝒫 z \in V$
15	1 9 11 14	elmptrab	$⊢ F \in fBas (B) \leftrightarrow (B \in V \land F \in 𝒫 𝒫 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))$
16		3anass	$⊢ (B \in V \land F \in 𝒫 𝒫 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 (B \in V \land (F \in 𝒫 𝒫 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)))$
17	15 16	bitri	$⊢ F \in fBas (B) \leftrightarrow (B \in V \land (F \in 𝒫 𝒫 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)))$
18		pwexg	$⊢ B \in A \to 𝒫 B \in V$
19		elpw2g	$⊢ 𝒫 B \in V \to (F \in 𝒫 𝒫 B \leftrightarrow F \subseteq 𝒫 B)$
20	18 19	syl	$⊢ B \in A \to (F \in 𝒫 𝒫 B \leftrightarrow F \subseteq 𝒫 B)$
21	20	anbi1d	$⊢ B \in A \to ((F \in 𝒫 𝒫 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 F \cap 𝒫 (x \cap y) \neq \emptyset)))$
22		elex	$⊢ B \in A \to B \in V$
23	22	biantrurd	$⊢ B \in A \to ((F \in 𝒫 𝒫 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 (B \in V \land (F \in 𝒫 𝒫 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))))$
24	21 23	bitr3d	$⊢ B \in A \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)) \leftrightarrow (B \in V \land (F \in 𝒫 𝒫 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))))$
25	17 24	bitr4id	$⊢ 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)))$

Metamath Proof Explorer

Theorem isfbas

Proof