filtop

Description: The underlying set belongs to the filter. (Contributed by FL, 20-Jul-2007) (Revised by Stefan O'Rear, 28-Jul-2015)

		Ref	Expression
	Assertion	filtop	$⊢ F \in Fil (X) \to X \in F$

Step	Hyp	Ref	Expression
1		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
2		fbasne0	$⊢ F \in fBas (X) \to F \neq \emptyset$
3	1 2	syl	$⊢ F \in Fil (X) \to F \neq \emptyset$
4		n0	$⊢ F \neq \emptyset \leftrightarrow \exists x x \in F$
5		filelss	$⊢ (F \in Fil (X) \land x \in F) \to x \subseteq X$
6		ssid	$⊢ X \subseteq X$
7		filss	$⊢ (F \in Fil (X) \land (x \in F \land X \subseteq X \land x \subseteq X)) \to X \in F$
8	7	3exp2	$⊢ F \in Fil (X) \to (x \in F \to (X \subseteq X \to (x \subseteq X \to X \in F)))$
9	8	imp	$⊢ (F \in Fil (X) \land x \in F) \to (X \subseteq X \to (x \subseteq X \to X \in F))$
10	6 9	mpi	$⊢ (F \in Fil (X) \land x \in F) \to (x \subseteq X \to X \in F)$
11	5 10	mpd	$⊢ (F \in Fil (X) \land x \in F) \to X \in F$
12	11	ex	$⊢ F \in Fil (X) \to (x \in F \to X \in F)$
13	12	exlimdv	$⊢ F \in Fil (X) \to (\exists x x \in F \to X \in F)$
14	4 13	biimtrid	$⊢ F \in Fil (X) \to (F \neq \emptyset \to X \in F)$
15	3 14	mpd	$⊢ F \in Fil (X) \to X \in F$

Metamath Proof Explorer