Metamath Proof Explorer


Theorem flimcf

Description: Fineness is properly characterized by the property that every limit point of a filter in the finer topology is a limit point in the coarser topology. (Contributed by Jeff Hankins, 28-Sep-2009) (Revised by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion flimcf ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐽𝐾 ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) )

Proof

Step Hyp Ref Expression
1 simplll ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽𝐾 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝑓 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 simprl ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽𝐾 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝑓 ) ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) )
3 simplr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽𝐾 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝑓 ) ) ) → 𝐽𝐾 )
4 flimss1 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽𝐾 ) → ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) )
5 1 2 3 4 syl3anc ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽𝐾 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝑓 ) ) ) → ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) )
6 simprr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽𝐾 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝑓 ) ) ) → 𝑥 ∈ ( 𝐾 fLim 𝑓 ) )
7 5 6 sseldd ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽𝐾 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝑓 ) ) ) → 𝑥 ∈ ( 𝐽 fLim 𝑓 ) )
8 7 expr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽𝐾 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑥 ∈ ( 𝐾 fLim 𝑓 ) → 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) )
9 8 ssrdv ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽𝐾 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) )
10 9 ralrimiva ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽𝐾 ) → ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) )
11 oveq2 ( 𝑓 = ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) → ( 𝐾 fLim 𝑓 ) = ( 𝐾 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) )
12 oveq2 ( 𝑓 = ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) → ( 𝐽 fLim 𝑓 ) = ( 𝐽 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) )
13 11 12 sseq12d ( 𝑓 = ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) → ( ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ↔ ( 𝐾 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ⊆ ( 𝐽 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ) )
14 simplr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) )
15 simpllr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
16 simplll ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
17 simprl ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → 𝑥𝐽 )
18 toponss ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥𝐽 ) → 𝑥𝑋 )
19 16 17 18 syl2anc ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → 𝑥𝑋 )
20 simprr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → 𝑦𝑥 )
21 19 20 sseldd ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → 𝑦𝑋 )
22 21 snssd ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → { 𝑦 } ⊆ 𝑋 )
23 20 snn0d ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → { 𝑦 } ≠ ∅ )
24 neifil ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ { 𝑦 } ⊆ 𝑋 ∧ { 𝑦 } ≠ ∅ ) → ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ∈ ( Fil ‘ 𝑋 ) )
25 15 22 23 24 syl3anc ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ∈ ( Fil ‘ 𝑋 ) )
26 13 14 25 rspcdva ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → ( 𝐾 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ⊆ ( 𝐽 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) )
27 neiflim ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦𝑋 ) → 𝑦 ∈ ( 𝐾 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) )
28 15 21 27 syl2anc ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → 𝑦 ∈ ( 𝐾 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) )
29 26 28 sseldd ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → 𝑦 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) )
30 flimneiss ( 𝑦 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ⊆ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) )
31 29 30 syl ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ⊆ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) )
32 topontop ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
33 16 32 syl ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → 𝐽 ∈ Top )
34 opnneip ( ( 𝐽 ∈ Top ∧ 𝑥𝐽𝑦𝑥 ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
35 33 17 20 34 syl3anc ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
36 31 35 sseldd ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥𝐽𝑦𝑥 ) ) → 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) )
37 36 anassrs ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥𝐽 ) ∧ 𝑦𝑥 ) → 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) )
38 37 ralrimiva ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥𝐽 ) → ∀ 𝑦𝑥 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) )
39 simpllr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥𝐽 ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
40 topontop ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) → 𝐾 ∈ Top )
41 opnnei ( 𝐾 ∈ Top → ( 𝑥𝐾 ↔ ∀ 𝑦𝑥 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) )
42 39 40 41 3syl ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥𝐽 ) → ( 𝑥𝐾 ↔ ∀ 𝑦𝑥 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) )
43 38 42 mpbird ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥𝐽 ) → 𝑥𝐾 )
44 43 ex ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) → ( 𝑥𝐽𝑥𝐾 ) )
45 44 ssrdv ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) → 𝐽𝐾 )
46 10 45 impbida ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐽𝐾 ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) )