Metamath Proof Explorer

Theorem fclsopn

Description: Write the cluster point condition in terms of open sets. (Contributed by Jeff Hankins, 10-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion 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. s e. F ( o i^i s ) =/= (/) ) ) ) )

Proof

Step Hyp Ref Expression
1 isfcls2 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) <-> A. s e. F A e. ( ( cls ` J ) ` s ) ) )
2 filn0 
 |-  ( F e. ( Fil ` X ) -> F =/= (/) )
3 2 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> F =/= (/) )
4 r19.2z 
 |-  ( ( F =/= (/) /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) -> E. s e. F A e. ( ( cls ` J ) ` s ) )
5 4 ex 
 |-  ( F =/= (/) -> ( A. s e. F A e. ( ( cls ` J ) ` s ) -> E. s e. F A e. ( ( cls ` J ) ` s ) ) )
6 3 5 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A. s e. F A e. ( ( cls ` J ) ` s ) -> E. s e. F A e. ( ( cls ` J ) ` s ) ) )
7 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
8 7 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ s e. F ) -> J e. Top )
9 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ s e. F ) -> s C_ X )
10 9 adantll 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ s e. F ) -> s C_ X )
11 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
12 11 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ s e. F ) -> X = U. J )
13 10 12 sseqtrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ s e. F ) -> s C_ U. J )
14 eqid 
 |-  U. J = U. J
15 14 clsss3 
 |-  ( ( J e. Top /\ s C_ U. J ) -> ( ( cls ` J ) ` s ) C_ U. J )
16 8 13 15 syl2anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ s e. F ) -> ( ( cls ` J ) ` s ) C_ U. J )
17 16 12 sseqtrrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ s e. F ) -> ( ( cls ` J ) ` s ) C_ X )
18 17 sseld 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ s e. F ) -> ( A e. ( ( cls ` J ) ` s ) -> A e. X ) )
19 18 rexlimdva 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( E. s e. F A e. ( ( cls ` J ) ` s ) -> A e. X ) )
20 6 19 syld 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A. s e. F A e. ( ( cls ` J ) ` s ) -> A e. X ) )
21 20 pm4.71rd 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A. s e. F A e. ( ( cls ` J ) ` s ) <-> ( A e. X /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) ) )
22 7 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ s e. F ) -> J e. Top )
23 13 adantlr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ s e. F ) -> s C_ U. J )
24 simplr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ s e. F ) -> A e. X )
25 11 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ s e. F ) -> X = U. J )
26 24 25 eleqtrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ s e. F ) -> A e. U. J )
27 14 elcls 
 |-  ( ( J e. Top /\ s C_ U. J /\ A e. U. J ) -> ( A e. ( ( cls ` J ) ` s ) <-> A. o e. J ( A e. o -> ( o i^i s ) =/= (/) ) ) )
28 22 23 26 27 syl3anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ s e. F ) -> ( A e. ( ( cls ` J ) ` s ) <-> A. o e. J ( A e. o -> ( o i^i s ) =/= (/) ) ) )
29 28 ralbidva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) -> ( A. s e. F A e. ( ( cls ` J ) ` s ) <-> A. s e. F A. o e. J ( A e. o -> ( o i^i s ) =/= (/) ) ) )
30 ralcom 
 |-  ( A. s e. F A. o e. J ( A e. o -> ( o i^i s ) =/= (/) ) <-> A. o e. J A. s e. F ( A e. o -> ( o i^i s ) =/= (/) ) )
31 r19.21v 
 |-  ( A. s e. F ( A e. o -> ( o i^i s ) =/= (/) ) <-> ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) )
32 31 ralbii 
 |-  ( A. o e. J A. s e. F ( A e. o -> ( o i^i s ) =/= (/) ) <-> A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) )
33 30 32 bitri 
 |-  ( A. s e. F A. o e. J ( A e. o -> ( o i^i s ) =/= (/) ) <-> A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) )
34 29 33 syl6bb 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) -> ( A. s e. F A e. ( ( cls ` J ) ` s ) <-> A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) )
35 34 pm5.32da 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( ( A e. X /\ A. s e. F A e. ( ( cls ` J ) ` s ) ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )
36 1 21 35 3bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fClus F ) <-> ( A e. X /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )