Metamath Proof Explorer

Theorem filnet

Description: A filter has the same convergence and clustering properties as some net. (Contributed by Jeff Hankins, 12-Dec-2009) (Revised by Mario Carneiro, 8-Aug-2015)

		Ref	Expression
	Assertion	filnet	$⊢ F \in Fil (X) \to \exists d \in DirRel \exists f (f : dom d ⟶ X \land F = (X FilMap f) (ran tail (d)))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃_{n \in F} (\{n\} \times n) = ⋃_{n \in F} (\{n\} \times n)$
2		eqid	$⊢ \{⟨x, y⟩ \| ((x \in ⋃_{n \in F} (\{n\} \times n) \land y \in ⋃_{n \in F} (\{n\} \times n)) \land 1^{st} (y) \subseteq 1^{st} (x))\} = \{⟨x, y⟩ \| ((x \in ⋃_{n \in F} (\{n\} \times n) \land y \in ⋃_{n \in F} (\{n\} \times n)) \land 1^{st} (y) \subseteq 1^{st} (x))\}$
3	1 2	filnetlem4	$⊢ F \in Fil (X) \to \exists d \in DirRel \exists f (f : dom d ⟶ X \land F = (X FilMap f) (ran tail (d)))$