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

Metamath Proof Explorer

Theorem fclsbas

Description: Cluster points in terms of filter bases. (Contributed by Jeff Hankins, 13-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Hypothesis fclsbas.f ⊢ 𝐹 = ( 𝑋 filGen 𝐵 )
Assertion fclsbas ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) ) )

Proof

Step Hyp Ref Expression
1 fclsbas.f ⊢ 𝐹 = ( 𝑋 filGen 𝐵 )
2 fgcl ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐵 ) ∈ ( Fil ‘ 𝑋 ) )
3 2 adantl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝑋 filGen 𝐵 ) ∈ ( Fil ‘ 𝑋 ) )
4 1 3 eqeltrid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
5 fclsopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) ) ) )
6 4 5 syldan ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) ) ) )
7 ssfg ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → 𝐵 ⊆ ( 𝑋 filGen 𝐵 ) )
8 7 ad3antlr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → 𝐵 ⊆ ( 𝑋 filGen 𝐵 ) )
9 8 1 sseqtrrdi ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → 𝐵 ⊆ 𝐹 )
10 ssralv ⊢ ( 𝐵 ⊆ 𝐹 → ( ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ → ∀ 𝑡 ∈ 𝐵 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) )
11 9 10 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → ( ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ → ∀ 𝑡 ∈ 𝐵 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) )
12 ineq2 ⊢ ( 𝑡 = 𝑠 → ( 𝑜 ∩ 𝑡 ) = ( 𝑜 ∩ 𝑠 ) )
13 12 neeq1d ⊢ ( 𝑡 = 𝑠 → ( ( 𝑜 ∩ 𝑡 ) ≠ ∅ ↔ ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
14 13 cbvralvw ⊢ ( ∀ 𝑡 ∈ 𝐵 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ )
15 11 14 imbitrdi ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → ( ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ → ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
16 1 eleq2i ⊢ ( 𝑡 ∈ 𝐹 ↔ 𝑡 ∈ ( 𝑋 filGen 𝐵 ) )
17 elfg ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐵 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 ) ) )
18 17 ad3antlr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐵 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 ) ) )
19 16 18 bitrid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → ( 𝑡 ∈ 𝐹 ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 ) ) )
20 19 simplbda ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) ∧ 𝑡 ∈ 𝐹 ) → ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 )
21 r19.29r ⊢ ( ( ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 ∧ ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) → ∃ 𝑠 ∈ 𝐵 ( 𝑠 ⊆ 𝑡 ∧ ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
22 sslin ⊢ ( 𝑠 ⊆ 𝑡 → ( 𝑜 ∩ 𝑠 ) ⊆ ( 𝑜 ∩ 𝑡 ) )
23 ssn0 ⊢ ( ( ( 𝑜 ∩ 𝑠 ) ⊆ ( 𝑜 ∩ 𝑡 ) ∧ ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) → ( 𝑜 ∩ 𝑡 ) ≠ ∅ )
24 22 23 sylan ⊢ ( ( 𝑠 ⊆ 𝑡 ∧ ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) → ( 𝑜 ∩ 𝑡 ) ≠ ∅ )
25 24 rexlimivw ⊢ ( ∃ 𝑠 ∈ 𝐵 ( 𝑠 ⊆ 𝑡 ∧ ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) → ( 𝑜 ∩ 𝑡 ) ≠ ∅ )
26 21 25 syl ⊢ ( ( ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 ∧ ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) → ( 𝑜 ∩ 𝑡 ) ≠ ∅ )
27 26 ex ⊢ ( ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 → ( ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ → ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) )
28 20 27 syl ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) ∧ 𝑡 ∈ 𝐹 ) → ( ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ → ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) )
29 28 ralrimdva ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → ( ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ → ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) )
30 15 29 impbid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → ( ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
31 30 anassrs ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝐴 ∈ 𝑜 ) → ( ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
32 31 pm5.74da ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ( 𝐴 ∈ 𝑜 → ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) ↔ ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) )
33 32 ralbidva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) )
34 33 pm5.32da ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑡 ∈ 𝐹 ( 𝑜 ∩ 𝑡 ) ≠ ∅ ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) ) )
35 6 34 bitrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐵 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) ) )