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 ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→A∈JfClusfL⁡F↔A∈X∧∀o∈JA∈o→∀s∈Lo∩Fs≠∅

Proof

Step Hyp Ref Expression
1 fcfval ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→JfClusfL⁡F=JfClusXFilMapF⁡L
2 1 eleq2d ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→A∈JfClusfL⁡F↔A∈JfClusXFilMapF⁡L
3 simp1 ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→J∈TopOn⁡X
4 toponmax ⊢J∈TopOn⁡X→X∈J
5 filfbas ⊢L∈Fil⁡Y→L∈fBas⁡Y
6 id ⊢F:Y⟶X→F:Y⟶X
7 fmfil ⊢X∈J∧L∈fBas⁡Y∧F:Y⟶X→XFilMapF⁡L∈Fil⁡X
8 4 5 6 7 syl3an ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→XFilMapF⁡L∈Fil⁡X
9 fclsopn ⊢J∈TopOn⁡X∧XFilMapF⁡L∈Fil⁡X→A∈JfClusXFilMapF⁡L↔A∈X∧∀o∈JA∈o→∀x∈XFilMapF⁡Lo∩x≠∅
10 3 8 9 syl2anc ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→A∈JfClusXFilMapF⁡L↔A∈X∧∀o∈JA∈o→∀x∈XFilMapF⁡Lo∩x≠∅
11 simpll1 ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J∧s∈L→J∈TopOn⁡X
12 11 4 syl ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J∧s∈L→X∈J
13 simpll2 ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J∧s∈L→L∈Fil⁡Y
14 13 5 syl ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J∧s∈L→L∈fBas⁡Y
15 simpll3 ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J∧s∈L→F:Y⟶X
16 simpl2 ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J→L∈Fil⁡Y
17 fgfil ⊢L∈Fil⁡Y→YfilGenL=L
18 16 17 syl ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J→YfilGenL=L
19 18 eleq2d ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J→s∈YfilGenL↔s∈L
20 19 biimpar ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J∧s∈L→s∈YfilGenL
21 eqid ⊢YfilGenL=YfilGenL
22 21 imaelfm ⊢X∈J∧L∈fBas⁡Y∧F:Y⟶X∧s∈YfilGenL→Fs∈XFilMapF⁡L
23 12 14 15 20 22 syl31anc ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J∧s∈L→Fs∈XFilMapF⁡L
24 ineq2 ⊢x=Fs→o∩x=o∩Fs
25 24 neeq1d ⊢x=Fs→o∩x≠∅↔o∩Fs≠∅
26 25 rspcv ⊢Fs∈XFilMapF⁡L→∀x∈XFilMapF⁡Lo∩x≠∅→o∩Fs≠∅
27 23 26 syl ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J∧s∈L→∀x∈XFilMapF⁡Lo∩x≠∅→o∩Fs≠∅
28 27 ralrimdva ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J→∀x∈XFilMapF⁡Lo∩x≠∅→∀s∈Lo∩Fs≠∅
29 elfm ⊢X∈J∧L∈fBas⁡Y∧F:Y⟶X→x∈XFilMapF⁡L↔x⊆X∧∃s∈LFs⊆x
30 4 5 6 29 syl3an ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→x∈XFilMapF⁡L↔x⊆X∧∃s∈LFs⊆x
31 30 adantr ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J→x∈XFilMapF⁡L↔x⊆X∧∃s∈LFs⊆x
32 31 simplbda ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J∧x∈XFilMapF⁡L→∃s∈LFs⊆x
33 r19.29r ⊢∃s∈LFs⊆x∧∀s∈Lo∩Fs≠∅→∃s∈LFs⊆x∧o∩Fs≠∅
34 sslin ⊢Fs⊆x→o∩Fs⊆o∩x
35 ssn0 ⊢o∩Fs⊆o∩x∧o∩Fs≠∅→o∩x≠∅
36 34 35 sylan ⊢Fs⊆x∧o∩Fs≠∅→o∩x≠∅
37 36 rexlimivw ⊢∃s∈LFs⊆x∧o∩Fs≠∅→o∩x≠∅
38 33 37 syl ⊢∃s∈LFs⊆x∧∀s∈Lo∩Fs≠∅→o∩x≠∅
39 38 ex ⊢∃s∈LFs⊆x→∀s∈Lo∩Fs≠∅→o∩x≠∅
40 32 39 syl ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J∧x∈XFilMapF⁡L→∀s∈Lo∩Fs≠∅→o∩x≠∅
41 40 ralrimdva ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J→∀s∈Lo∩Fs≠∅→∀x∈XFilMapF⁡Lo∩x≠∅
42 28 41 impbid ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J→∀x∈XFilMapF⁡Lo∩x≠∅↔∀s∈Lo∩Fs≠∅
43 42 imbi2d ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X∧o∈J→A∈o→∀x∈XFilMapF⁡Lo∩x≠∅↔A∈o→∀s∈Lo∩Fs≠∅
44 43 ralbidva ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→∀o∈JA∈o→∀x∈XFilMapF⁡Lo∩x≠∅↔∀o∈JA∈o→∀s∈Lo∩Fs≠∅
45 44 anbi2d ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→A∈X∧∀o∈JA∈o→∀x∈XFilMapF⁡Lo∩x≠∅↔A∈X∧∀o∈JA∈o→∀s∈Lo∩Fs≠∅
46 2 10 45 3bitrd ⊢J∈TopOn⁡X∧L∈Fil⁡Y∧F:Y⟶X→A∈JfClusfL⁡F↔A∈X∧∀o∈JA∈o→∀s∈Lo∩Fs≠∅