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 e. ( Fil ` X ) -> E. d e. DirRel E. f ( f : dom d --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` d ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- U_ n e. F ( { n } X. n ) = U_ n e. F ( { n } X. n )
2		eqid	|- { <. x , y >. | ( ( x e. U_ n e. F ( { n } X. n ) /\ y e. U_ n e. F ( { n } X. n ) ) /\ ( 1st ` y ) C_ ( 1st ` x ) ) } = { <. x , y >. | ( ( x e. U_ n e. F ( { n } X. n ) /\ y e. U_ n e. F ( { n } X. n ) ) /\ ( 1st ` y ) C_ ( 1st ` x ) ) }
3	1 2	filnetlem4	|- ( F e. ( Fil ` X ) -> E. d e. DirRel E. f ( f : dom d --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` d ) ) ) )