Metamath Proof Explorer

Theorem fgval

Description: The filter generating class gives a filter for every filter base. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	fgval	$⊢ F \in fBas (X) \to X filGen F = \{x \in 𝒫 X \| F \cap 𝒫 x \neq \emptyset\}$

Proof

Step	Hyp	Ref	Expression
1		df-fg	$⊢ filGen = (v \in V, f \in fBas (v) ⟼ \{x \in 𝒫 v \| f \cap 𝒫 x \neq \emptyset\})$
2	1	a1i	$⊢ F \in fBas (X) \to filGen = (v \in V, f \in fBas (v) ⟼ \{x \in 𝒫 v \| f \cap 𝒫 x \neq \emptyset\})$
3		pweq	$⊢ v = X \to 𝒫 v = 𝒫 X$
4	3	adantr	$⊢ (v = X \land f = F) \to 𝒫 v = 𝒫 X$
5		ineq1	$⊢ f = F \to f \cap 𝒫 x = F \cap 𝒫 x$
6	5	neeq1d	$⊢ f = F \to (f \cap 𝒫 x \neq \emptyset \leftrightarrow F \cap 𝒫 x \neq \emptyset)$
7	6	adantl	$⊢ (v = X \land f = F) \to (f \cap 𝒫 x \neq \emptyset \leftrightarrow F \cap 𝒫 x \neq \emptyset)$
8	4 7	rabeqbidv	$⊢ (v = X \land f = F) \to \{x \in 𝒫 v \| f \cap 𝒫 x \neq \emptyset\} = \{x \in 𝒫 X \| F \cap 𝒫 x \neq \emptyset\}$
9	8	adantl	$⊢ (F \in fBas (X) \land (v = X \land f = F)) \to \{x \in 𝒫 v \| f \cap 𝒫 x \neq \emptyset\} = \{x \in 𝒫 X \| F \cap 𝒫 x \neq \emptyset\}$
10		fveq2	$⊢ v = X \to fBas (v) = fBas (X)$
11	10	adantl	$⊢ (F \in fBas (X) \land v = X) \to fBas (v) = fBas (X)$
12		elfvex	$⊢ F \in fBas (X) \to X \in V$
13		id	$⊢ F \in fBas (X) \to F \in fBas (X)$
14		elfvdm	$⊢ F \in fBas (X) \to X \in dom fBas$
15		pwexg	$⊢ X \in dom fBas \to 𝒫 X \in V$
16		rabexg	$⊢ 𝒫 X \in V \to \{x \in 𝒫 X \| F \cap 𝒫 x \neq \emptyset\} \in V$
17	14 15 16	3syl	$⊢ F \in fBas (X) \to \{x \in 𝒫 X \| F \cap 𝒫 x \neq \emptyset\} \in V$
18	2 9 11 12 13 17	ovmpodx	$⊢ F \in fBas (X) \to X filGen F = \{x \in 𝒫 X \| F \cap 𝒫 x \neq \emptyset\}$