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 bitrdi
 |-  ( ( ( 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 ) =/= (/) ) ) ) )