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 𝑓 ) ) )