isfil

Description: The predicate "is a filter." (Contributed by FL, 20-Jul-2007) (Revised by Mario Carneiro, 28-Jul-2015)

		Ref	Expression
	Assertion	isfil	$⊢ F \in Fil (X) \leftrightarrow (F \in fBas (X) \land \forall x \in 𝒫 X (F \cap 𝒫 x \neq \emptyset \to x \in F))$

Step	Hyp	Ref	Expression
1		df-fil	$⊢ Fil = (z \in V ⟼ \{f \in fBas (z) \| \forall x \in 𝒫 z (f \cap 𝒫 x \neq \emptyset \to x \in f)\})$
2		pweq	$⊢ z = X \to 𝒫 z = 𝒫 X$
3	2	adantr	$⊢ (z = X \land f = F) \to 𝒫 z = 𝒫 X$
4		ineq1	$⊢ f = F \to f \cap 𝒫 x = F \cap 𝒫 x$
5	4	neeq1d	$⊢ f = F \to (f \cap 𝒫 x \neq \emptyset \leftrightarrow F \cap 𝒫 x \neq \emptyset)$
6		eleq2	$⊢ f = F \to (x \in f \leftrightarrow x \in F)$
7	5 6	imbi12d	$⊢ f = F \to ((f \cap 𝒫 x \neq \emptyset \to x \in f) \leftrightarrow (F \cap 𝒫 x \neq \emptyset \to x \in F))$
8	7	adantl	$⊢ (z = X \land f = F) \to ((f \cap 𝒫 x \neq \emptyset \to x \in f) \leftrightarrow (F \cap 𝒫 x \neq \emptyset \to x \in F))$
9	3 8	raleqbidv	$⊢ (z = X \land f = F) \to (\forall x \in 𝒫 z (f \cap 𝒫 x \neq \emptyset \to x \in f) \leftrightarrow \forall x \in 𝒫 X (F \cap 𝒫 x \neq \emptyset \to x \in F))$
10		fveq2	$⊢ z = X \to fBas (z) = fBas (X)$
11		fvex	$⊢ fBas (z) \in V$
12		elfvdm	$⊢ F \in fBas (X) \to X \in dom fBas$
13	1 9 10 11 12	elmptrab2	$⊢ F \in Fil (X) \leftrightarrow (F \in fBas (X) \land \forall x \in 𝒫 X (F \cap 𝒫 x \neq \emptyset \to x \in F))$

Metamath Proof Explorer