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