df-fg

Description: Define the filter generating function. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 11-Jul-2015)

		Ref	Expression
	Assertion	df-fg	$⊢ filGen = (w \in V, x \in fBas (w) ⟼ \{y \in 𝒫 w \| x \cap 𝒫 y \neq \emptyset\})$

Step	Hyp	Ref	Expression
0		cfg	$class filGen$
1		vw	$setvar w$
2		cvv	$class V$
3		vx	$setvar x$
4		cfbas	$class fBas$
5	1	cv	$setvar w$
6	5 4	cfv	$class fBas (w)$
7		vy	$setvar y$
8	5	cpw	$class 𝒫 w$
9	3	cv	$setvar x$
10	7	cv	$setvar y$
11	10	cpw	$class 𝒫 y$
12	9 11	cin	$class (x \cap 𝒫 y)$
13		c0	$class \emptyset$
14	12 13	wne	$wff x \cap 𝒫 y \neq \emptyset$
15	14 7 8	crab	$class \{y \in 𝒫 w \| x \cap 𝒫 y \neq \emptyset\}$
16	1 3 2 6 15	cmpo	$class (w \in V, x \in fBas (w) ⟼ \{y \in 𝒫 w \| x \cap 𝒫 y \neq \emptyset\})$
17	0 16	wceq	$wff filGen = (w \in V, x \in fBas (w) ⟼ \{y \in 𝒫 w \| x \cap 𝒫 y \neq \emptyset\})$

Metamath Proof Explorer