Metamath Proof Explorer

Theorem flimopn

Description: The condition for being a limit point of a filter still holds if one only considers open neighborhoods. (Contributed by Jeff Hankins, 4-Sep-2009) (Proof shortened by Mario Carneiro, 9-Apr-2015)

Ref Expression
Assertion flimopn ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 elflim ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ) )
2 dfss3 ⊢ ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ↔ ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) 𝑦 ∈ 𝐹 )
3 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
4 3 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ Top )
5 opnneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥 ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
6 5 3expb ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥 ) ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
7 4 6 sylan ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥 ) ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
8 eleq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐹 ↔ 𝑥 ∈ 𝐹 ) )
9 8 rspcv ⊢ ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) 𝑦 ∈ 𝐹 → 𝑥 ∈ 𝐹 ) )
10 7 9 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥 ) ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) 𝑦 ∈ 𝐹 → 𝑥 ∈ 𝐹 ) )
11 10 expr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝐴 ∈ 𝑥 → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) 𝑦 ∈ 𝐹 → 𝑥 ∈ 𝐹 ) ) )
12 11 com23 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) 𝑦 ∈ 𝐹 → ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) ) )
13 12 ralrimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) 𝑦 ∈ 𝐹 → ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) ) )
14 simpr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
15 3 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐽 ∈ Top )
16 simplr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐴 ∈ 𝑋 )
17 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
18 17 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑋 = ∪ 𝐽 )
19 16 18 eleqtrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐴 ∈ ∪ 𝐽 )
20 19 snssd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → { 𝐴 } ⊆ ∪ 𝐽 )
21 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
22 21 neii1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑦 ⊆ ∪ 𝐽 )
23 4 22 sylan ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑦 ⊆ ∪ 𝐽 )
24 21 neiint ⊢ ( ( 𝐽 ∈ Top ∧ { 𝐴 } ⊆ ∪ 𝐽 ∧ 𝑦 ⊆ ∪ 𝐽 ) → ( 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ) )
25 15 20 23 24 syl3anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ) )
26 14 25 mpbid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑦 ) )
27 snssg ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ) )
28 27 ad2antlr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ) )
29 26 28 mpbird ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑦 ) )
30 21 ntropn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ∈ 𝐽 )
31 15 23 30 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ∈ 𝐽 )
32 eleq2 ⊢ ( 𝑥 = ( ( int ‘ 𝐽 ) ‘ 𝑦 ) → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ) )
33 eleq1 ⊢ ( 𝑥 = ( ( int ‘ 𝐽 ) ‘ 𝑦 ) → ( 𝑥 ∈ 𝐹 ↔ ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ∈ 𝐹 ) )
34 32 33 imbi12d ⊢ ( 𝑥 = ( ( int ‘ 𝐽 ) ‘ 𝑦 ) → ( ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) ↔ ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑦 ) → ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ∈ 𝐹 ) ) )
35 34 rspcv ⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ∈ 𝐽 → ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) → ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑦 ) → ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ∈ 𝐹 ) ) )
36 31 35 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) → ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑦 ) → ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ∈ 𝐹 ) ) )
37 29 36 mpid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) → ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ∈ 𝐹 ) )
38 simpllr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
39 21 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ⊆ 𝑦 )
40 15 23 39 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ⊆ 𝑦 )
41 23 18 sseqtrrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑦 ⊆ 𝑋 )
42 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋 ∧ ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ⊆ 𝑦 ) ) → 𝑦 ∈ 𝐹 )
43 42 3exp2 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ∈ 𝐹 → ( 𝑦 ⊆ 𝑋 → ( ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ⊆ 𝑦 → 𝑦 ∈ 𝐹 ) ) ) )
44 43 com24 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ⊆ 𝑦 → ( 𝑦 ⊆ 𝑋 → ( ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ∈ 𝐹 → 𝑦 ∈ 𝐹 ) ) ) )
45 38 40 41 44 syl3c ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( ( ( int ‘ 𝐽 ) ‘ 𝑦 ) ∈ 𝐹 → 𝑦 ∈ 𝐹 ) )
46 37 45 syld ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) → 𝑦 ∈ 𝐹 ) )
47 46 ralrimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) → ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) 𝑦 ∈ 𝐹 ) )
48 13 47 impbid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) 𝑦 ∈ 𝐹 ↔ ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) ) )
49 2 48 syl5bb ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ↔ ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) ) )
50 49 pm5.32da ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( ( 𝐴 ∈ 𝑋 ∧ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ⊆ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) ) ) )
51 1 50 bitrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) ) ) )