Metamath Proof Explorer

Theorem flimss1

Description: A limit point of a filter is a limit point in a coarser topology. (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion flimss1 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝐾 fLim 𝐹 ) ⊆ ( 𝐽 fLim 𝐹 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
2 1 flimelbas ⊢ ( 𝑥 ∈ ( 𝐾 fLim 𝐹 ) → 𝑥 ∈ ∪ 𝐾 )
3 2 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → 𝑥 ∈ ∪ 𝐾 )
4 simpl2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
5 filunibas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
6 4 5 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → ∪ 𝐹 = 𝑋 )
7 1 flimfil ⊢ ( 𝑥 ∈ ( 𝐾 fLim 𝐹 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐾 ) )
8 7 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐾 ) )
9 filunibas ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐾 ) → ∪ 𝐹 = ∪ 𝐾 )
10 8 9 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → ∪ 𝐹 = ∪ 𝐾 )
11 6 10 eqtr3d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → 𝑋 = ∪ 𝐾 )
12 3 11 eleqtrrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → 𝑥 ∈ 𝑋 )
13 simpl1 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
14 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
15 13 14 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → 𝐽 ∈ Top )
16 flimtop ⊢ ( 𝑥 ∈ ( 𝐾 fLim 𝐹 ) → 𝐾 ∈ Top )
17 16 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → 𝐾 ∈ Top )
18 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
19 13 18 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → 𝑋 = ∪ 𝐽 )
20 19 11 eqtr3d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → ∪ 𝐽 = ∪ 𝐾 )
21 simpl3 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → 𝐽 ⊆ 𝐾 )
22 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
23 22 1 topssnei ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ ∪ 𝐽 = ∪ 𝐾 ) ∧ 𝐽 ⊆ 𝐾 ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ ( ( nei ‘ 𝐾 ) ‘ { 𝑥 } ) )
24 15 17 20 21 23 syl31anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ ( ( nei ‘ 𝐾 ) ‘ { 𝑥 } ) )
25 flimneiss ⊢ ( 𝑥 ∈ ( 𝐾 fLim 𝐹 ) → ( ( nei ‘ 𝐾 ) ‘ { 𝑥 } ) ⊆ 𝐹 )
26 25 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → ( ( nei ‘ 𝐾 ) ‘ { 𝑥 } ) ⊆ 𝐹 )
27 24 26 sstrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 )
28 elflim ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ) ) )
29 13 4 28 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → ( 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ⊆ 𝐹 ) ) )
30 12 27 29 mpbir2and ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝐹 ) ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) )
31 30 ex ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝑥 ∈ ( 𝐾 fLim 𝐹 ) → 𝑥 ∈ ( 𝐽 fLim 𝐹 ) ) )
32 31 ssrdv ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝐾 fLim 𝐹 ) ⊆ ( 𝐽 fLim 𝐹 ) )