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 snnzg ⊢ ( 𝑦 ∈ 𝑋 → { 𝑦 } ≠ ∅ )
24 21 23 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → { 𝑦 } ≠ ∅ )
25 neifil ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ { 𝑦 } ⊆ 𝑋 ∧ { 𝑦 } ≠ ∅ ) → ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ∈ ( Fil ‘ 𝑋 ) )
26 15 22 24 25 syl3anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ∈ ( Fil ‘ 𝑋 ) )
27 13 14 26 rspcdva ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝐾 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ⊆ ( 𝐽 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) )
28 neiflim ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ ( 𝐾 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) )
29 15 21 28 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ ( 𝐾 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) )
30 27 29 sseldd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) )
31 flimneiss ⊢ ( 𝑦 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ⊆ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) )
32 30 31 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ⊆ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) )
33 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
34 16 33 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝐽 ∈ Top )
35 opnneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
36 34 17 20 35 syl3anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) )
37 32 36 sseldd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) )
38 37 anassrs ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) )
39 38 ralrimiva ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → ∀ 𝑦 ∈ 𝑥 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) )
40 simpllr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
41 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) → 𝐾 ∈ Top )
42 opnnei ⊢ ( 𝐾 ∈ Top → ( 𝑥 ∈ 𝐾 ↔ ∀ 𝑦 ∈ 𝑥 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) )
43 40 41 42 3syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐾 ↔ ∀ 𝑦 ∈ 𝑥 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) )
44 39 43 mpbird ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝐾 )
45 44 ex ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) → ( 𝑥 ∈ 𝐽 → 𝑥 ∈ 𝐾 ) )
46 45 ssrdv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) → 𝐽 ⊆ 𝐾 )
47 10 46 impbida ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐽 ⊆ 𝐾 ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) )