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

Metamath Proof Explorer

Theorem isfcf

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

Ref Expression
Assertion isfcf ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) ) )

Proof

Step Hyp Ref Expression
1 fcfval ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) = ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) )
2 1 eleq2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ↔ 𝐴 ∈ ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ) )
3 simp1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
5 filfbas ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
6 id ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → 𝐹 : 𝑌 ⟶ 𝑋 )
7 fmfil ⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝐿 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) )
8 4 5 6 7 syl3an ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) )
9 fclsopn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) ) ) )
10 3 8 9 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( 𝐽 fClus ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) ) ) )
11 simpll1 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
12 11 4 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → 𝑋 ∈ 𝐽 )
13 simpll2 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
14 13 5 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → 𝐿 ∈ ( fBas ‘ 𝑌 ) )
15 simpll3 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → 𝐹 : 𝑌 ⟶ 𝑋 )
16 simpl2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
17 fgfil ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑌 ) → ( 𝑌 filGen 𝐿 ) = 𝐿 )
18 16 17 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝑌 filGen 𝐿 ) = 𝐿 )
19 18 eleq2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝑠 ∈ ( 𝑌 filGen 𝐿 ) ↔ 𝑠 ∈ 𝐿 ) )
20 19 biimpar ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → 𝑠 ∈ ( 𝑌 filGen 𝐿 ) )
21 eqid ⊢ ( 𝑌 filGen 𝐿 ) = ( 𝑌 filGen 𝐿 )
22 21 imaelfm ⊢ ( ( ( 𝑋 ∈ 𝐽 ∧ 𝐿 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑠 ∈ ( 𝑌 filGen 𝐿 ) ) → ( 𝐹 “ 𝑠 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) )
23 12 14 15 20 22 syl31anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → ( 𝐹 “ 𝑠 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) )
24 ineq2 ⊢ ( 𝑥 = ( 𝐹 “ 𝑠 ) → ( 𝑜 ∩ 𝑥 ) = ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) )
25 24 neeq1d ⊢ ( 𝑥 = ( 𝐹 “ 𝑠 ) → ( ( 𝑜 ∩ 𝑥 ) ≠ ∅ ↔ ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
26 25 rspcv ⊢ ( ( 𝐹 “ 𝑠 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) → ( ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ → ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
27 23 26 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑠 ∈ 𝐿 ) → ( ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ → ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
28 27 ralrimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
29 elfm ⊢ ( ( 𝑋 ∈ 𝐽 ∧ 𝐿 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ) ) )
30 4 5 6 29 syl3an ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ) ) )
31 30 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ) ) )
32 31 simplbda ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 )
33 r19.29r ⊢ ( ( ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ∧ ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ∃ 𝑠 ∈ 𝐿 ( ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ∧ ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
34 sslin ⊢ ( ( 𝐹 “ 𝑠 ) ⊆ 𝑥 → ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ⊆ ( 𝑜 ∩ 𝑥 ) )
35 ssn0 ⊢ ( ( ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ⊆ ( 𝑜 ∩ 𝑥 ) ∧ ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ( 𝑜 ∩ 𝑥 ) ≠ ∅ )
36 34 35 sylan ⊢ ( ( ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ∧ ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ( 𝑜 ∩ 𝑥 ) ≠ ∅ )
37 36 rexlimivw ⊢ ( ∃ 𝑠 ∈ 𝐿 ( ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ∧ ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ( 𝑜 ∩ 𝑥 ) ≠ ∅ )
38 33 37 syl ⊢ ( ( ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 ∧ ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) → ( 𝑜 ∩ 𝑥 ) ≠ ∅ )
39 38 ex ⊢ ( ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑥 → ( ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) )
40 32 39 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) ∧ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ) → ( ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) )
41 40 ralrimdva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ → ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) )
42 28 41 impbid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) )
43 42 imbi2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑜 ∈ 𝐽 ) → ( ( 𝐴 ∈ 𝑜 → ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) ↔ ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )
44 43 ralbidva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) )
45 44 anbi2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑥 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐿 ) ( 𝑜 ∩ 𝑥 ) ≠ ∅ ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) ) )
46 2 10 45 3bitrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fClusf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐿 ( 𝑜 ∩ ( 𝐹 “ 𝑠 ) ) ≠ ∅ ) ) ) )