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

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 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐽 fLim 𝐺 ) ⊆ ( 𝐽 fLim 𝐹 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 1 flimelbas ⊢ ( 𝑥 ∈ ( 𝐽 fLim 𝐺 ) → 𝑥 ∈ ∪ 𝐽 )
3 2 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → 𝑥 ∈ ∪ 𝐽 )
4 simpl1 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
6 4 5 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → 𝑋 = ∪ 𝐽 )
7 3 6 eleqtrrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → 𝑥 ∈ 𝑋 )
8 flimneiss ⊢ ( 𝑥 ∈ ( 𝐽 fLim 𝐺 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐺 )
9 8 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐺 )
10 simpl3 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → 𝐺 ⊆ 𝐹 )
11 9 10 sstrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 )
12 simpl2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
13 elflim ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ) ) )
14 4 12 13 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ) ) )
15 7 11 14 mpbir2and ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) ∧ 𝑥 ∈ ( 𝐽 fLim 𝐺 ) ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) )
16 15 ex ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐺 ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) )
17 16 ssrdv ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐽 fLim 𝐺 ) ⊆ ( 𝐽 fLim 𝐹 ) )