Theorem 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 \mathrm{Fil}\left(X\right)\to X\in F$$

Proof

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