Metamath Proof Explorer

Theorem fclsbas

Description: Cluster points in terms of filter bases. (Contributed by Jeff Hankins, 13-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Hypothesis fclsbas.f 
|- F = ( X filGen B )
Assertion fclsbas 
|- ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. B ( o i^i s ) =/= (/) ) ) ) )

Proof

Step Hyp Ref Expression
1 fclsbas.f 
 |-  F = ( X filGen B )
2 fgcl 
 |-  ( B e. ( fBas ` X ) -> ( X filGen B ) e. ( Fil ` X ) )
3 2 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( X filGen B ) e. ( Fil ` X ) )
4 1 3 eqeltrid 
 |-  ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) -> F e. ( Fil ` X ) )
5 fclsopn 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. t e. F ( o i^i t ) =/= (/) ) ) ) )
6 4 5 syldan 
 |-  ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. t e. F ( o i^i t ) =/= (/) ) ) ) )
7 ssfg 
 |-  ( B e. ( fBas ` X ) -> B C_ ( X filGen B ) )
8 7 ad3antlr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> B C_ ( X filGen B ) )
9 8 1 sseqtrrdi 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> B C_ F )
10 ssralv 
 |-  ( B C_ F -> ( A. t e. F ( o i^i t ) =/= (/) -> A. t e. B ( o i^i t ) =/= (/) ) )
11 9 10 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> ( A. t e. F ( o i^i t ) =/= (/) -> A. t e. B ( o i^i t ) =/= (/) ) )
12 ineq2 
 |-  ( t = s -> ( o i^i t ) = ( o i^i s ) )
13 12 neeq1d 
 |-  ( t = s -> ( ( o i^i t ) =/= (/) <-> ( o i^i s ) =/= (/) ) )
14 13 cbvralvw 
 |-  ( A. t e. B ( o i^i t ) =/= (/) <-> A. s e. B ( o i^i s ) =/= (/) )
15 11 14 imbitrdi 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> ( A. t e. F ( o i^i t ) =/= (/) -> A. s e. B ( o i^i s ) =/= (/) ) )
16 1 eleq2i 
 |-  ( t e. F <-> t e. ( X filGen B ) )
17 elfg 
 |-  ( B e. ( fBas ` X ) -> ( t e. ( X filGen B ) <-> ( t C_ X /\ E. s e. B s C_ t ) ) )
18 17 ad3antlr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> ( t e. ( X filGen B ) <-> ( t C_ X /\ E. s e. B s C_ t ) ) )
19 16 18 bitrid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> ( t e. F <-> ( t C_ X /\ E. s e. B s C_ t ) ) )
20 19 simplbda 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) /\ t e. F ) -> E. s e. B s C_ t )
21 r19.29r 
 |-  ( ( E. s e. B s C_ t /\ A. s e. B ( o i^i s ) =/= (/) ) -> E. s e. B ( s C_ t /\ ( o i^i s ) =/= (/) ) )
22 sslin 
 |-  ( s C_ t -> ( o i^i s ) C_ ( o i^i t ) )
23 ssn0 
 |-  ( ( ( o i^i s ) C_ ( o i^i t ) /\ ( o i^i s ) =/= (/) ) -> ( o i^i t ) =/= (/) )
24 22 23 sylan 
 |-  ( ( s C_ t /\ ( o i^i s ) =/= (/) ) -> ( o i^i t ) =/= (/) )
25 24 rexlimivw 
 |-  ( E. s e. B ( s C_ t /\ ( o i^i s ) =/= (/) ) -> ( o i^i t ) =/= (/) )
26 21 25 syl 
 |-  ( ( E. s e. B s C_ t /\ A. s e. B ( o i^i s ) =/= (/) ) -> ( o i^i t ) =/= (/) )
27 26 ex 
 |-  ( E. s e. B s C_ t -> ( A. s e. B ( o i^i s ) =/= (/) -> ( o i^i t ) =/= (/) ) )
28 20 27 syl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) /\ t e. F ) -> ( A. s e. B ( o i^i s ) =/= (/) -> ( o i^i t ) =/= (/) ) )
29 28 ralrimdva 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> ( A. s e. B ( o i^i s ) =/= (/) -> A. t e. F ( o i^i t ) =/= (/) ) )
30 15 29 impbid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ ( o e. J /\ A e. o ) ) -> ( A. t e. F ( o i^i t ) =/= (/) <-> A. s e. B ( o i^i s ) =/= (/) ) )
31 30 anassrs 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ o e. J ) /\ A e. o ) -> ( A. t e. F ( o i^i t ) =/= (/) <-> A. s e. B ( o i^i s ) =/= (/) ) )
32 31 pm5.74da 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) /\ o e. J ) -> ( ( A e. o -> A. t e. F ( o i^i t ) =/= (/) ) <-> ( A e. o -> A. s e. B ( o i^i s ) =/= (/) ) ) )
33 32 ralbidva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) /\ A e. X ) -> ( A. o e. J ( A e. o -> A. t e. F ( o i^i t ) =/= (/) ) <-> A. o e. J ( A e. o -> A. s e. B ( o i^i s ) =/= (/) ) ) )
34 33 pm5.32da 
 |-  ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( ( A e. X /\ A. o e. J ( A e. o -> A. t e. F ( o i^i t ) =/= (/) ) ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. B ( o i^i s ) =/= (/) ) ) ) )
35 6 34 bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ B e. ( fBas ` X ) ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. B ( o i^i s ) =/= (/) ) ) ) )