df-fbas

Description: Define the class of all filter bases. Note that a filter base on one set is also a filter base for any superset, so there is not a unique base set that can be recovered. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Stefan O'Rear, 11-Jul-2015)

		Ref	Expression
	Assertion	df-fbas	$⊢ fBas = (w \in V ⟼ \{x \in 𝒫 𝒫 w \| (x \neq \emptyset \land \emptyset \notin x \land \forall y \in x \forall z \in x x \cap 𝒫 (y \cap z) \neq \emptyset)\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfbas	$class fBas$
1		vw	$setvar w$
2		cvv	$class V$
3		vx	$setvar x$
4	1	cv	$setvar w$
5	4	cpw	$class 𝒫 w$
6	5	cpw	$class 𝒫 𝒫 w$
7	3	cv	$setvar x$
8		c0	$class \emptyset$
9	7 8	wne	$wff x \neq \emptyset$
10	8 7	wnel	$wff \emptyset \notin x$
11		vy	$setvar y$
12		vz	$setvar z$
13	11	cv	$setvar y$
14	12	cv	$setvar z$
15	13 14	cin	$class (y \cap z)$
16	15	cpw	$class 𝒫 (y \cap z)$
17	7 16	cin	$class (x \cap 𝒫 (y \cap z))$
18	17 8	wne	$wff x \cap 𝒫 (y \cap z) \neq \emptyset$
19	18 12 7	wral	$wff \forall z \in x x \cap 𝒫 (y \cap z) \neq \emptyset$
20	19 11 7	wral	$wff \forall y \in x \forall z \in x x \cap 𝒫 (y \cap z) \neq \emptyset$
21	9 10 20	w3a	$wff (x \neq \emptyset \land \emptyset \notin x \land \forall y \in x \forall z \in x x \cap 𝒫 (y \cap z) \neq \emptyset)$
22	21 3 6	crab	$class \{x \in 𝒫 𝒫 w \| (x \neq \emptyset \land \emptyset \notin x \land \forall y \in x \forall z \in x x \cap 𝒫 (y \cap z) \neq \emptyset)\}$
23	1 2 22	cmpt	$class (w \in V ⟼ \{x \in 𝒫 𝒫 w \| (x \neq \emptyset \land \emptyset \notin x \land \forall y \in x \forall z \in x x \cap 𝒫 (y \cap z) \neq \emptyset)\})$
24	0 23	wceq	$wff fBas = (w \in V ⟼ \{x \in 𝒫 𝒫 w \| (x \neq \emptyset \land \emptyset \notin x \land \forall y \in x \forall z \in x x \cap 𝒫 (y \cap z) \neq \emptyset)\})$

Metamath Proof Explorer

Definition df-fbas

Detailed syntax breakdown