Theorem filunibas

Description: Recover the base set from a filter. (Contributed by Stefan O'Rear, 2-Aug-2015)

	Ref	Expression
Assertion	filunibas	$$⊢F\in \mathrm{Fil}\left(X\right)\to \bigcup F=X$$

Proof

Step	Hyp	Ref	Expression
1		filsspw	$$⊢F\in \mathrm{Fil}\left(X\right)\to F\subseteq 𝒫X$$
2		sspwuni	$$⊢F\subseteq 𝒫X\leftrightarrow \bigcup F\subseteq X$$
3	1 2	sylib	$$⊢F\in \mathrm{Fil}\left(X\right)\to \bigcup F\subseteq X$$
4		filtop	$$⊢F\in \mathrm{Fil}\left(X\right)\to X\in F$$
5		unissel	$$⊢\left(\bigcup F\subseteq X\wedge X\in F\right)\to \bigcup F=X$$
6	3 4 5	syl2anc	$$⊢F\in \mathrm{Fil}\left(X\right)\to \bigcup F=X$$