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 syl5ibr ( ( 𝐽 ∈ ( 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 ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠𝐹 ( 𝑛𝑠 ) ≠ ∅ ) ) )