Metamath Proof Explorer

Theorem fbflim2

Description: A condition for a filter base B to converge to a point A . Use neighborhoods instead of open neighborhoods. Compare fbflim . (Contributed by FL, 4-Jul-2011) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis fbflim.3 ⊢ 𝐹 = ( 𝑋 filGen 𝐵 )
Assertion fbflim2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 fbflim.3 ⊢ 𝐹 = ( 𝑋 filGen 𝐵 )
2 1 fbflim ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) ) )
3 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
4 3 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ Top )
5 simpr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
6 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
7 6 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → 𝑋 = ∪ 𝐽 )
8 5 7 eleqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ∪ 𝐽 )
9 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
10 9 isneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ ∪ 𝐽 ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ ( 𝑛 ⊆ ∪ 𝐽 ∧ ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) ) ) )
11 4 8 10 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ ( 𝑛 ⊆ ∪ 𝐽 ∧ ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) ) ) )
12 simpr ⊢ ( ( 𝑛 ⊆ ∪ 𝐽 ∧ ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) ) → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) )
13 11 12 syl6bi ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) ) )
14 r19.29 ⊢ ( ( ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ∧ ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) ) → ∃ 𝑦 ∈ 𝐽 ( ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ∧ ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) ) )
15 pm3.45 ⊢ ( ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) → ( ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) → ( ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) ) )
16 15 imp ⊢ ( ( ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ∧ ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) ) → ( ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) )
17 sstr2 ⊢ ( 𝑥 ⊆ 𝑦 → ( 𝑦 ⊆ 𝑛 → 𝑥 ⊆ 𝑛 ) )
18 17 com12 ⊢ ( 𝑦 ⊆ 𝑛 → ( 𝑥 ⊆ 𝑦 → 𝑥 ⊆ 𝑛 ) )
19 18 reximdv ⊢ ( 𝑦 ⊆ 𝑛 → ( ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 ) )
20 19 impcom ⊢ ( ( ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 )
21 16 20 syl ⊢ ( ( ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ∧ ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) ) → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 )
22 21 rexlimivw ⊢ ( ∃ 𝑦 ∈ 𝐽 ( ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ∧ ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) ) → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 )
23 14 22 syl ⊢ ( ( ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ∧ ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) ) → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 )
24 23 ex ⊢ ( ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) → ( ∃ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑛 ) → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 ) )
25 13 24 syl9 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 ) ) )
26 25 ralrimdv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) → ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 ) )
27 4 adantr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦 ) ) → 𝐽 ∈ Top )
28 simprl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦 ) ) → 𝑦 ∈ 𝐽 )
29 simprr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦 ) ) → 𝐴 ∈ 𝑦 )
30 opnneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦 ) → 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
31 27 28 29 30 syl3anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦 ) ) → 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
32 sseq2 ⊢ ( 𝑛 = 𝑦 → ( 𝑥 ⊆ 𝑛 ↔ 𝑥 ⊆ 𝑦 ) )
33 32 rexbidv ⊢ ( 𝑛 = 𝑦 → ( ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 ↔ ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) )
34 33 rspcv ⊢ ( 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) )
35 31 34 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝐴 ∈ 𝑦 ) ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) )
36 35 expr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝐴 ∈ 𝑦 → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) )
37 36 com23 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝐽 ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 → ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) )
38 37 ralrimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 → ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) )
39 26 38 impbid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 ) )
40 39 pm5.32da ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝐽 ( 𝐴 ∈ 𝑦 → ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑦 ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 ) ) )
41 2 40 bitrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∃ 𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛 ) ) )