This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem filunibas

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

		Ref	Expression
	Assertion	filunibas	$⊢ F \in Fil (X) \to ⋃ F = X$

Step	Hyp	Ref	Expression
1		filsspw	$⊢ F \in Fil (X) \to F \subseteq 𝒫 X$
2		sspwuni	$⊢ F \subseteq 𝒫 X \leftrightarrow ⋃ F \subseteq X$
3	1 2	sylib	$⊢ F \in Fil (X) \to ⋃ F \subseteq X$
4		filtop	$⊢ F \in Fil (X) \to X \in F$
5		unissel	$⊢ (⋃ F \subseteq X \land X \in F) \to ⋃ F = X$
6	3 4 5	syl2anc	$⊢ F \in Fil (X) \to ⋃ F = X$