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 e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fClusf L ) ` F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) ) ) )

Proof

Step Hyp Ref Expression
1 fcfval 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( J fClusf L ) ` F ) = ( J fClus ( ( X FilMap F ) ` L ) ) )
2 1 eleq2d 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fClusf L ) ` F ) <-> A e. ( J fClus ( ( X FilMap F ) ` L ) ) ) )
3 simp1 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> J e. ( TopOn ` X ) )
4 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
5 filfbas 
 |-  ( L e. ( Fil ` Y ) -> L e. ( fBas ` Y ) )
6 id 
 |-  ( F : Y --> X -> F : Y --> X )
7 fmfil 
 |-  ( ( X e. J /\ L e. ( fBas ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( Fil ` X ) )
8 4 5 6 7 syl3an 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( X FilMap F ) ` L ) e. ( Fil ` X ) )
9 fclsopn 
 |-  ( ( J e. ( TopOn ` X ) /\ ( ( X FilMap F ) ` L ) e. ( Fil ` X ) ) -> ( A e. ( J fClus ( ( X FilMap F ) ` L ) ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. x e. ( ( X FilMap F ) ` L ) ( o i^i x ) =/= (/) ) ) ) )
10 3 8 9 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( J fClus ( ( X FilMap F ) ` L ) ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. x e. ( ( X FilMap F ) ` L ) ( o i^i x ) =/= (/) ) ) ) )
11 simpll1 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) /\ s e. L ) -> J e. ( TopOn ` X ) )
12 11 4 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) /\ s e. L ) -> X e. J )
13 simpll2 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) /\ s e. L ) -> L e. ( Fil ` Y ) )
14 13 5 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) /\ s e. L ) -> L e. ( fBas ` Y ) )
15 simpll3 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) /\ s e. L ) -> F : Y --> X )
16 simpl2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) -> L e. ( Fil ` Y ) )
17 fgfil 
 |-  ( L e. ( Fil ` Y ) -> ( Y filGen L ) = L )
18 16 17 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) -> ( Y filGen L ) = L )
19 18 eleq2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) -> ( s e. ( Y filGen L ) <-> s e. L ) )
20 19 biimpar 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) /\ s e. L ) -> s e. ( Y filGen L ) )
21 eqid 
 |-  ( Y filGen L ) = ( Y filGen L )
22 21 imaelfm 
 |-  ( ( ( X e. J /\ L e. ( fBas ` Y ) /\ F : Y --> X ) /\ s e. ( Y filGen L ) ) -> ( F " s ) e. ( ( X FilMap F ) ` L ) )
23 12 14 15 20 22 syl31anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) /\ s e. L ) -> ( F " s ) e. ( ( X FilMap F ) ` L ) )
24 ineq2 
 |-  ( x = ( F " s ) -> ( o i^i x ) = ( o i^i ( F " s ) ) )
25 24 neeq1d 
 |-  ( x = ( F " s ) -> ( ( o i^i x ) =/= (/) <-> ( o i^i ( F " s ) ) =/= (/) ) )
26 25 rspcv 
 |-  ( ( F " s ) e. ( ( X FilMap F ) ` L ) -> ( A. x e. ( ( X FilMap F ) ` L ) ( o i^i x ) =/= (/) -> ( o i^i ( F " s ) ) =/= (/) ) )
27 23 26 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) /\ s e. L ) -> ( A. x e. ( ( X FilMap F ) ` L ) ( o i^i x ) =/= (/) -> ( o i^i ( F " s ) ) =/= (/) ) )
28 27 ralrimdva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) -> ( A. x e. ( ( X FilMap F ) ` L ) ( o i^i x ) =/= (/) -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) )
29 elfm 
 |-  ( ( X e. J /\ L e. ( fBas ` Y ) /\ F : Y --> X ) -> ( x e. ( ( X FilMap F ) ` L ) <-> ( x C_ X /\ E. s e. L ( F " s ) C_ x ) ) )
30 4 5 6 29 syl3an 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( x e. ( ( X FilMap F ) ` L ) <-> ( x C_ X /\ E. s e. L ( F " s ) C_ x ) ) )
31 30 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) -> ( x e. ( ( X FilMap F ) ` L ) <-> ( x C_ X /\ E. s e. L ( F " s ) C_ x ) ) )
32 31 simplbda 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) /\ x e. ( ( X FilMap F ) ` L ) ) -> E. s e. L ( F " s ) C_ x )
33 r19.29r 
 |-  ( ( E. s e. L ( F " s ) C_ x /\ A. s e. L ( o i^i ( F " s ) ) =/= (/) ) -> E. s e. L ( ( F " s ) C_ x /\ ( o i^i ( F " s ) ) =/= (/) ) )
34 sslin 
 |-  ( ( F " s ) C_ x -> ( o i^i ( F " s ) ) C_ ( o i^i x ) )
35 ssn0 
 |-  ( ( ( o i^i ( F " s ) ) C_ ( o i^i x ) /\ ( o i^i ( F " s ) ) =/= (/) ) -> ( o i^i x ) =/= (/) )
36 34 35 sylan 
 |-  ( ( ( F " s ) C_ x /\ ( o i^i ( F " s ) ) =/= (/) ) -> ( o i^i x ) =/= (/) )
37 36 rexlimivw 
 |-  ( E. s e. L ( ( F " s ) C_ x /\ ( o i^i ( F " s ) ) =/= (/) ) -> ( o i^i x ) =/= (/) )
38 33 37 syl 
 |-  ( ( E. s e. L ( F " s ) C_ x /\ A. s e. L ( o i^i ( F " s ) ) =/= (/) ) -> ( o i^i x ) =/= (/) )
39 38 ex 
 |-  ( E. s e. L ( F " s ) C_ x -> ( A. s e. L ( o i^i ( F " s ) ) =/= (/) -> ( o i^i x ) =/= (/) ) )
40 32 39 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) /\ x e. ( ( X FilMap F ) ` L ) ) -> ( A. s e. L ( o i^i ( F " s ) ) =/= (/) -> ( o i^i x ) =/= (/) ) )
41 40 ralrimdva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) -> ( A. s e. L ( o i^i ( F " s ) ) =/= (/) -> A. x e. ( ( X FilMap F ) ` L ) ( o i^i x ) =/= (/) ) )
42 28 41 impbid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) -> ( A. x e. ( ( X FilMap F ) ` L ) ( o i^i x ) =/= (/) <-> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) )
43 42 imbi2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) /\ o e. J ) -> ( ( A e. o -> A. x e. ( ( X FilMap F ) ` L ) ( o i^i x ) =/= (/) ) <-> ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) ) )
44 43 ralbidva 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A. o e. J ( A e. o -> A. x e. ( ( X FilMap F ) ` L ) ( o i^i x ) =/= (/) ) <-> A. o e. J ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) ) )
45 44 anbi2d 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( ( A e. X /\ A. o e. J ( A e. o -> A. x e. ( ( X FilMap F ) ` L ) ( o i^i x ) =/= (/) ) ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) ) ) )
46 2 10 45 3bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( Fil ` Y ) /\ F : Y --> X ) -> ( A e. ( ( J fClusf L ) ` F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. L ( o i^i ( F " s ) ) =/= (/) ) ) ) )