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

Metamath Proof Explorer

Theorem flimcls

Description: Closure in terms of filter convergence. (Contributed by Jeff Hankins, 28-Nov-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Assertion flimcls ⊢ J ∈ TopOn ⁡ X ∧ S ⊆ X → A ∈ cls ⁡ J ⁡ S ↔ ∃ f ∈ Fil ⁡ X S ∈ f ∧ A ∈ J fLim f

Proof

Step Hyp Ref Expression
1 eqid ⊢ X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S = X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S
2 1 flimclslem ⊢ J ∈ TopOn ⁡ X ∧ S ⊆ X ∧ A ∈ cls ⁡ J ⁡ S → X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S ∈ Fil ⁡ X ∧ S ∈ X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S ∧ A ∈ J fLim X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S
3 3anass ⊢ X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S ∈ Fil ⁡ X ∧ S ∈ X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S ∧ A ∈ J fLim X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S ↔ X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S ∈ Fil ⁡ X ∧ S ∈ X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S ∧ A ∈ J fLim X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S
4 2 3 sylib ⊢ J ∈ TopOn ⁡ X ∧ S ⊆ X ∧ A ∈ cls ⁡ J ⁡ S → X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S ∈ Fil ⁡ X ∧ S ∈ X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S ∧ A ∈ J fLim X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S
5 eleq2 ⊢ f = X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S → S ∈ f ↔ S ∈ X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S
6 oveq2 ⊢ f = X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S → J fLim f = J fLim X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S
7 6 eleq2d ⊢ f = X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S → A ∈ J fLim f ↔ A ∈ J fLim X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S
8 5 7 anbi12d ⊢ f = X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S → S ∈ f ∧ A ∈ J fLim f ↔ S ∈ X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S ∧ A ∈ J fLim X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S
9 8 rspcev ⊢ X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S ∈ Fil ⁡ X ∧ S ∈ X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S ∧ A ∈ J fLim X filGen fi ⁡ nei ⁡ J ⁡ A ∪ S → ∃ f ∈ Fil ⁡ X S ∈ f ∧ A ∈ J fLim f
10 4 9 syl ⊢ J ∈ TopOn ⁡ X ∧ S ⊆ X ∧ A ∈ cls ⁡ J ⁡ S → ∃ f ∈ Fil ⁡ X S ∈ f ∧ A ∈ J fLim f
11 10 3expia ⊢ J ∈ TopOn ⁡ X ∧ S ⊆ X → A ∈ cls ⁡ J ⁡ S → ∃ f ∈ Fil ⁡ X S ∈ f ∧ A ∈ J fLim f
12 flimclsi ⊢ S ∈ f → J fLim f ⊆ cls ⁡ J ⁡ S
13 12 sselda ⊢ S ∈ f ∧ A ∈ J fLim f → A ∈ cls ⁡ J ⁡ S
14 13 rexlimivw ⊢ ∃ f ∈ Fil ⁡ X S ∈ f ∧ A ∈ J fLim f → A ∈ cls ⁡ J ⁡ S
15 11 14 impbid1 ⊢ J ∈ TopOn ⁡ X ∧ S ⊆ X → A ∈ cls ⁡ J ⁡ S ↔ ∃ f ∈ Fil ⁡ X S ∈ f ∧ A ∈ J fLim f