This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( ( ( ( 𝐽 ∈ ( 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 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) ) ) )