Metamath Proof Explorer

Theorem fclsnei

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

Ref Expression
Assertion fclsnei ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐹 ( 𝑛 ∩ 𝑠 ) ≠ ∅ ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 1 fclselbas ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐴 ∈ ∪ 𝐽 )
3 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
4 3 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → 𝑋 = ∪ 𝐽 )
5 4 eleq2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ 𝑋 ↔ 𝐴 ∈ ∪ 𝐽 ) )
6 2 5 imbitrrid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐴 ∈ 𝑋 ) )
7 fclsneii ⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑠 ∈ 𝐹 ) → ( 𝑛 ∩ 𝑠 ) ≠ ∅ )
8 7 3expb ⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∧ 𝑠 ∈ 𝐹 ) ) → ( 𝑛 ∩ 𝑠 ) ≠ ∅ )
9 8 ralrimivva ⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐹 ( 𝑛 ∩ 𝑠 ) ≠ ∅ )
10 6 9 jca2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐹 ( 𝑛 ∩ 𝑠 ) ≠ ∅ ) ) )
11 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
12 11 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → 𝐽 ∈ Top )
13 simprl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → 𝑜 ∈ 𝐽 )
14 simprr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → 𝐴 ∈ 𝑜 )
15 opnneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) → 𝑜 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
16 12 13 14 15 syl3anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → 𝑜 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
17 ineq1 ⊢ ( 𝑛 = 𝑜 → ( 𝑛 ∩ 𝑠 ) = ( 𝑜 ∩ 𝑠 ) )
18 17 neeq1d ⊢ ( 𝑛 = 𝑜 → ( ( 𝑛 ∩ 𝑠 ) ≠ ∅ ↔ ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
19 18 ralbidv ⊢ ( 𝑛 = 𝑜 → ( ∀ 𝑠 ∈ 𝐹 ( 𝑛 ∩ 𝑠 ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
20 19 rspcv ⊢ ( 𝑜 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐹 ( 𝑛 ∩ 𝑠 ) ≠ ∅ → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
21 16 20 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐹 ( 𝑛 ∩ 𝑠 ) ≠ ∅ → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) )
22 21 expr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝐴 ∈ 𝑜 → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐹 ( 𝑛 ∩ 𝑠 ) ≠ ∅ → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) )
23 22 com23 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐹 ( 𝑛 ∩ 𝑠 ) ≠ ∅ → ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) )
24 23 ralrimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐹 ( 𝑛 ∩ 𝑠 ) ≠ ∅ → ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) )
25 24 imdistanda ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐹 ( 𝑛 ∩ 𝑠 ) ≠ ∅ ) → ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) ) )
26 fclsopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) ) )
27 25 26 sylibrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐹 ( 𝑛 ∩ 𝑠 ) ≠ ∅ ) → 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ) )
28 10 27 impbid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐹 ( 𝑛 ∩ 𝑠 ) ≠ ∅ ) ) )