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		pwexg	$⊢ B \in A \to 𝒫 B \in V$
2		elpw2g	$⊢ 𝒫 B \in V \to (F \in 𝒫 𝒫 B \leftrightarrow F \subseteq 𝒫 B)$
3	1 2	syl	$⊢ B \in A \to (F \in 𝒫 𝒫 B \leftrightarrow F \subseteq 𝒫 B)$
4	3	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)))$
5		elex	$⊢ B \in A \to B \in V$
6	5	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))))$
7	4 6	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))))$
8		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)\})$
9		neeq1	$⊢ w = F \to (w \neq \emptyset \leftrightarrow F \neq \emptyset)$
10		neleq2	$⊢ w = F \to (\emptyset \notin w \leftrightarrow \emptyset \notin F)$
11		ineq1	$⊢ w = F \to w \cap 𝒫 (x \cap y) = F \cap 𝒫 (x \cap y)$
12	11	neeq1d	$⊢ w = F \to (w \cap 𝒫 (x \cap y) \neq \emptyset \leftrightarrow F \cap 𝒫 (x \cap y) \neq \emptyset)$
13	12	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)$
14	13	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)$
15	9 10 14	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))$
16	15	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))$
17		pweq	$⊢ z = B \to 𝒫 z = 𝒫 B$
18	17	pweqd	$⊢ z = B \to 𝒫 𝒫 z = 𝒫 𝒫 B$
19		vpwex	$⊢ 𝒫 z \in V$
20	19	pwex	$⊢ 𝒫 𝒫 z \in V$
21	20	a1i	$⊢ z \in V \to 𝒫 𝒫 z \in V$
22	8 16 18 21	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))$
23		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)))$
24	22 23	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)))$
25	7 24	syl6rbbr	$⊢ 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