elfg

Description: A condition for elements of a generated filter. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

		Ref	Expression
	Assertion	elfg	$⊢ F \in fBas (X) \to (A \in (X filGen F) \leftrightarrow (A \subseteq X \land \exists x \in F x \subseteq A))$

Proof

Step	Hyp	Ref	Expression
1		fgval	$⊢ F \in fBas (X) \to X filGen F = \{y \in 𝒫 X \| F \cap 𝒫 y \neq \emptyset\}$
2	1	eleq2d	$⊢ F \in fBas (X) \to (A \in (X filGen F) \leftrightarrow A \in \{y \in 𝒫 X \| F \cap 𝒫 y \neq \emptyset\})$
3		pweq	$⊢ y = A \to 𝒫 y = 𝒫 A$
4	3	ineq2d	$⊢ y = A \to F \cap 𝒫 y = F \cap 𝒫 A$
5	4	neeq1d	$⊢ y = A \to (F \cap 𝒫 y \neq \emptyset \leftrightarrow F \cap 𝒫 A \neq \emptyset)$
6	5	elrab	$⊢ A \in \{y \in 𝒫 X \| F \cap 𝒫 y \neq \emptyset\} \leftrightarrow (A \in 𝒫 X \land F \cap 𝒫 A \neq \emptyset)$
7		elfvdm	$⊢ F \in fBas (X) \to X \in dom fBas$
8		elpw2g	$⊢ X \in dom fBas \to (A \in 𝒫 X \leftrightarrow A \subseteq X)$
9	7 8	syl	$⊢ F \in fBas (X) \to (A \in 𝒫 X \leftrightarrow A \subseteq X)$
10		elin	$⊢ x \in (F \cap 𝒫 A) \leftrightarrow (x \in F \land x \in 𝒫 A)$
11		velpw	$⊢ x \in 𝒫 A \leftrightarrow x \subseteq A$
12	11	anbi2i	$⊢ (x \in F \land x \in 𝒫 A) \leftrightarrow (x \in F \land x \subseteq A)$
13	10 12	bitri	$⊢ x \in (F \cap 𝒫 A) \leftrightarrow (x \in F \land x \subseteq A)$
14	13	exbii	$⊢ \exists x x \in (F \cap 𝒫 A) \leftrightarrow \exists x (x \in F \land x \subseteq A)$
15		n0	$⊢ F \cap 𝒫 A \neq \emptyset \leftrightarrow \exists x x \in (F \cap 𝒫 A)$
16		df-rex	$⊢ \exists x \in F x \subseteq A \leftrightarrow \exists x (x \in F \land x \subseteq A)$
17	14 15 16	3bitr4i	$⊢ F \cap 𝒫 A \neq \emptyset \leftrightarrow \exists x \in F x \subseteq A$
18	17	a1i	$⊢ F \in fBas (X) \to (F \cap 𝒫 A \neq \emptyset \leftrightarrow \exists x \in F x \subseteq A)$
19	9 18	anbi12d	$⊢ F \in fBas (X) \to ((A \in 𝒫 X \land F \cap 𝒫 A \neq \emptyset) \leftrightarrow (A \subseteq X \land \exists x \in F x \subseteq A))$
20	6 19	bitrid	$⊢ F \in fBas (X) \to (A \in \{y \in 𝒫 X \| F \cap 𝒫 y \neq \emptyset\} \leftrightarrow (A \subseteq X \land \exists x \in F x \subseteq A))$
21	2 20	bitrd	$⊢ F \in fBas (X) \to (A \in (X filGen F) \leftrightarrow (A \subseteq X \land \exists x \in F x \subseteq A))$

Metamath Proof Explorer

Theorem elfg

Proof