Metamath Proof Explorer

Theorem flimss2

Description: A limit point of a filter is a limit point of a finer filter. (Contributed by Jeff Hankins, 5-Sep-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion flimss2 ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ G ⊆ F → J fLim G ⊆ J fLim F

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 1 flimelbas ⊢ x ∈ J fLim G → x ∈ ⋃ J
3 2 adantl ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ G ⊆ F ∧ x ∈ J fLim G → x ∈ ⋃ J
4 simpl1 ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ G ⊆ F ∧ x ∈ J fLim G → J ∈ TopOn ⁡ X
5 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
6 4 5 syl ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ G ⊆ F ∧ x ∈ J fLim G → X = ⋃ J
7 3 6 eleqtrrd ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ G ⊆ F ∧ x ∈ J fLim G → x ∈ X
8 flimneiss ⊢ x ∈ J fLim G → nei ⁡ J ⁡ x ⊆ G
9 8 adantl ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ G ⊆ F ∧ x ∈ J fLim G → nei ⁡ J ⁡ x ⊆ G
10 simpl3 ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ G ⊆ F ∧ x ∈ J fLim G → G ⊆ F
11 9 10 sstrd ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ G ⊆ F ∧ x ∈ J fLim G → nei ⁡ J ⁡ x ⊆ F
12 simpl2 ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ G ⊆ F ∧ x ∈ J fLim G → F ∈ Fil ⁡ X
13 elflim ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X → x ∈ J fLim F ↔ x ∈ X ∧ nei ⁡ J ⁡ x ⊆ F
14 4 12 13 syl2anc ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ G ⊆ F ∧ x ∈ J fLim G → x ∈ J fLim F ↔ x ∈ X ∧ nei ⁡ J ⁡ x ⊆ F
15 7 11 14 mpbir2and ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ G ⊆ F ∧ x ∈ J fLim G → x ∈ J fLim F
16 15 ex ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ G ⊆ F → x ∈ J fLim G → x ∈ J fLim F
17 16 ssrdv ⊢ J ∈ TopOn ⁡ X ∧ F ∈ Fil ⁡ X ∧ G ⊆ F → J fLim G ⊆ J fLim F