Metamath Proof Explorer


Theorem fbflim

Description: A condition for a filter to converge to a point involving one of its bases. (Contributed by Jeff Hankins, 4-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Hypothesis fbflim.3 𝐹 = ( 𝑋 filGen 𝐵 )
Assertion fbflim ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴𝑋 ∧ ∀ 𝑥𝐽 ( 𝐴𝑥 → ∃ 𝑦𝐵 𝑦𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 fbflim.3 𝐹 = ( 𝑋 filGen 𝐵 )
2 fgcl ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐵 ) ∈ ( Fil ‘ 𝑋 ) )
3 1 2 eqeltrid ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
4 flimopn ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴𝑋 ∧ ∀ 𝑥𝐽 ( 𝐴𝑥𝑥𝐹 ) ) ) )
5 3 4 sylan2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴𝑋 ∧ ∀ 𝑥𝐽 ( 𝐴𝑥𝑥𝐹 ) ) ) )
6 toponss ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥𝐽 ) → 𝑥𝑋 )
7 6 ad4ant14 ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴𝑋 ) ∧ 𝑥𝐽 ) → 𝑥𝑋 )
8 1 eleq2i ( 𝑥𝐹𝑥 ∈ ( 𝑋 filGen 𝐵 ) )
9 elfg ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝑋 filGen 𝐵 ) ↔ ( 𝑥𝑋 ∧ ∃ 𝑦𝐵 𝑦𝑥 ) ) )
10 9 ad3antlr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴𝑋 ) ∧ 𝑥𝐽 ) → ( 𝑥 ∈ ( 𝑋 filGen 𝐵 ) ↔ ( 𝑥𝑋 ∧ ∃ 𝑦𝐵 𝑦𝑥 ) ) )
11 8 10 syl5bb ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴𝑋 ) ∧ 𝑥𝐽 ) → ( 𝑥𝐹 ↔ ( 𝑥𝑋 ∧ ∃ 𝑦𝐵 𝑦𝑥 ) ) )
12 7 11 mpbirand ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴𝑋 ) ∧ 𝑥𝐽 ) → ( 𝑥𝐹 ↔ ∃ 𝑦𝐵 𝑦𝑥 ) )
13 12 imbi2d ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴𝑋 ) ∧ 𝑥𝐽 ) → ( ( 𝐴𝑥𝑥𝐹 ) ↔ ( 𝐴𝑥 → ∃ 𝑦𝐵 𝑦𝑥 ) ) )
14 13 ralbidva ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴𝑋 ) → ( ∀ 𝑥𝐽 ( 𝐴𝑥𝑥𝐹 ) ↔ ∀ 𝑥𝐽 ( 𝐴𝑥 → ∃ 𝑦𝐵 𝑦𝑥 ) ) )
15 14 pm5.32da ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝐴𝑋 ∧ ∀ 𝑥𝐽 ( 𝐴𝑥𝑥𝐹 ) ) ↔ ( 𝐴𝑋 ∧ ∀ 𝑥𝐽 ( 𝐴𝑥 → ∃ 𝑦𝐵 𝑦𝑥 ) ) ) )
16 5 15 bitrd ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴𝑋 ∧ ∀ 𝑥𝐽 ( 𝐴𝑥 → ∃ 𝑦𝐵 𝑦𝑥 ) ) ) )