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 TopOn X F Fil X A J fClus F A X o J A o s F o s

Proof

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