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	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑑 ∈ DirRel ∃ 𝑓 ( 𝑓 : dom 𝑑 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝑑 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) = ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 )
2		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ∧ 𝑦 ∈ ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ) ∧ ( 1st ‘ 𝑦 ) ⊆ ( 1st ‘ 𝑥 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ∧ 𝑦 ∈ ∪ 𝑛 ∈ 𝐹 ( { 𝑛 } × 𝑛 ) ) ∧ ( 1st ‘ 𝑦 ) ⊆ ( 1st ‘ 𝑥 ) ) }
3	1 2	filnetlem4	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∃ 𝑑 ∈ DirRel ∃ 𝑓 ( 𝑓 : dom 𝑑 ⟶ 𝑋 ∧ 𝐹 = ( ( 𝑋 FilMap 𝑓 ) ‘ ran ( tail ‘ 𝑑 ) ) ) )