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

Metamath Proof Explorer

Theorem fcfnei

Description: The property of being a cluster point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 26-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion fcfnei ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )

Proof

Step Hyp Ref Expression
1 isfcf ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) ) )
2 simpll1 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
4 2 3 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐽 ∈ Top )
5 simpr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
6 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
7 6 neii1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑛 ⊆ ∪ 𝐽 )
8 4 5 7 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑛 ⊆ ∪ 𝐽 )
9 6 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑛 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ⊆ 𝑛 )
10 4 8 9 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ⊆ 𝑛 )
11 simplr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐴 ∈ 𝑋 )
12 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
13 2 12 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑋 = ∪ 𝐽 )
14 11 13 eleqtrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐴 ∈ ∪ 𝐽 )
15 14 snssd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → { 𝐴 } ⊆ ∪ 𝐽 )
16 6 neiint ⊢ ( ( 𝐽 ∈ Top ∧ { 𝐴 } ⊆ ∪ 𝐽 ∧ 𝑛 ⊆ ∪ 𝐽 ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ) )
17 4 15 8 16 syl3anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ) )
18 5 17 mpbid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑛 ) )
19 snssg ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ) )
20 11 19 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ↔ { 𝐴 } ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ) )
21 18 20 mpbird ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑛 ) )
22 6 ntropn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑛 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∈ 𝐽 )
23 4 8 22 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∈ 𝐽 )
24 eleq2 ⊢ ( 𝑜 = ( ( int ‘ 𝐽 ) ‘ 𝑛 ) → ( 𝐴 ∈ 𝑜 ↔ 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ) )
25 ineq1 ⊢ ( 𝑜 = ( ( int ‘ 𝐽 ) ‘ 𝑛 ) → ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) = ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∩ ( 𝐹 “ 𝑠 ) ) )
26 25 neeq1d ⊢ ( 𝑜 = ( ( int ‘ 𝐽 ) ‘ 𝑛 ) → ( ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ↔ ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
27 26 ralbidv ⊢ ( 𝑜 = ( ( int ‘ 𝐽 ) ‘ 𝑛 ) → ( ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐿 ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
28 24 27 imbi12d ⊢ ( 𝑜 = ( ( int ‘ 𝐽 ) ‘ 𝑛 ) → ( ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ↔ ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑛 ) → ∀ 𝑠 ∈ 𝐿 ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )
29 28 rspcv ⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∈ 𝐽 → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑛 ) → ∀ 𝑠 ∈ 𝐿 ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )
30 23 29 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ( 𝐴 ∈ ( ( int ‘ 𝐽 ) ‘ 𝑛 ) → ∀ 𝑠 ∈ 𝐿 ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )
31 21 30 mpid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ∀ 𝑠 ∈ 𝐿 ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
32 ssrin ⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ⊆ 𝑛 → ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∩ ( 𝐹 “ 𝑠 ) ) ⊆ ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) )
33 ssn0 ⊢ ( ( ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∩ ( 𝐹 “ 𝑠 ) ) ⊆ ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ∧ ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ )
34 33 ex ⊢ ( ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∩ ( 𝐹 “ 𝑠 ) ) ⊆ ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) → ( ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
35 32 34 syl ⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ⊆ 𝑛 → ( ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
36 35 ralimdv ⊢ ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ⊆ 𝑛 → ( ∀ 𝑠 ∈ 𝐿 ( ( ( int ‘ 𝐽 ) ‘ 𝑛 ) ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
37 10 31 36 sylsyld ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
38 37 ralrimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
39 simpl1 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
40 39 3 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ Top )
41 opnneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) → 𝑜 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
42 41 3expb ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → 𝑜 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
43 40 42 sylan ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → 𝑜 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
44 ineq1 ⊢ ( 𝑛 = 𝑜 → ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) = ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) )
45 44 neeq1d ⊢ ( 𝑛 = 𝑜 → ( ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ↔ ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
46 45 ralbidv ⊢ ( 𝑛 = 𝑜 → ( ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
47 46 rspcv ⊢ ( 𝑜 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
48 43 47 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝐴 ∈ 𝑜 ) ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
49 48 expr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝐴 ∈ 𝑜 → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )
50 49 com23 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )
51 50 ralrimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )
52 38 51 impbid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ↔ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
53 52 pm5.32da ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )
54 1 53 bitrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑛 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ∀ 𝑠 ∈ 𝐿 ( 𝑛 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )