Metamath Proof Explorer

Theorem isreg2

Description: A topological space is regular if any closed set is separated from any point not in it by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion isreg2 ⊢J∈TopOn⁡X→J∈Reg↔∀c∈Clsd⁡J∀x∈X¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅

Proof

Step Hyp Ref Expression
1 simp1r ⊢J∈TopOn⁡X∧J∈Reg∧c∈Clsd⁡J∧x∈X∧¬x∈c→J∈Reg
2 simp2l ⊢J∈TopOn⁡X∧J∈Reg∧c∈Clsd⁡J∧x∈X∧¬x∈c→c∈Clsd⁡J
3 simp2r ⊢J∈TopOn⁡X∧J∈Reg∧c∈Clsd⁡J∧x∈X∧¬x∈c→x∈X
4 simp1l ⊢J∈TopOn⁡X∧J∈Reg∧c∈Clsd⁡J∧x∈X∧¬x∈c→J∈TopOn⁡X
5 toponuni ⊢J∈TopOn⁡X→X=⋃J
6 4 5 syl ⊢J∈TopOn⁡X∧J∈Reg∧c∈Clsd⁡J∧x∈X∧¬x∈c→X=⋃J
7 3 6 eleqtrd ⊢J∈TopOn⁡X∧J∈Reg∧c∈Clsd⁡J∧x∈X∧¬x∈c→x∈⋃J
8 simp3 ⊢J∈TopOn⁡X∧J∈Reg∧c∈Clsd⁡J∧x∈X∧¬x∈c→¬x∈c
9 eqid ⊢⋃J=⋃J
10 9 regsep2 ⊢J∈Reg∧c∈Clsd⁡J∧x∈⋃J∧¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅
11 1 2 7 8 10 syl13anc ⊢J∈TopOn⁡X∧J∈Reg∧c∈Clsd⁡J∧x∈X∧¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅
12 11 3expia ⊢J∈TopOn⁡X∧J∈Reg∧c∈Clsd⁡J∧x∈X→¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅
13 12 ralrimivva ⊢J∈TopOn⁡X∧J∈Reg→∀c∈Clsd⁡J∀x∈X¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅
14 topontop ⊢J∈TopOn⁡X→J∈Top
15 14 adantr ⊢J∈TopOn⁡X∧∀c∈Clsd⁡J∀x∈X¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅→J∈Top
16 5 adantr ⊢J∈TopOn⁡X∧y∈J→X=⋃J
17 16 difeq1d ⊢J∈TopOn⁡X∧y∈J→X∖y=⋃J∖y
18 9 opncld ⊢J∈Top∧y∈J→⋃J∖y∈Clsd⁡J
19 14 18 sylan ⊢J∈TopOn⁡X∧y∈J→⋃J∖y∈Clsd⁡J
20 17 19 eqeltrd ⊢J∈TopOn⁡X∧y∈J→X∖y∈Clsd⁡J
21 eleq2 ⊢c=X∖y→x∈c↔x∈X∖y
22 21 notbid ⊢c=X∖y→¬x∈c↔¬x∈X∖y
23 eldif ⊢x∈X∖y↔x∈X∧¬x∈y
24 23 baibr ⊢x∈X→¬x∈y↔x∈X∖y
25 24 con1bid ⊢x∈X→¬x∈X∖y↔x∈y
26 22 25 sylan9bb ⊢c=X∖y∧x∈X→¬x∈c↔x∈y
27 simpl ⊢c=X∖y∧x∈X→c=X∖y
28 27 sseq1d ⊢c=X∖y∧x∈X→c⊆o↔X∖y⊆o
29 28 3anbi1d ⊢c=X∖y∧x∈X→c⊆o∧x∈p∧o∩p=∅↔X∖y⊆o∧x∈p∧o∩p=∅
30 29 2rexbidv ⊢c=X∖y∧x∈X→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅↔∃o∈J∃p∈JX∖y⊆o∧x∈p∧o∩p=∅
31 26 30 imbi12d ⊢c=X∖y∧x∈X→¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅↔x∈y→∃o∈J∃p∈JX∖y⊆o∧x∈p∧o∩p=∅
32 31 ralbidva ⊢c=X∖y→∀x∈X¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅↔∀x∈Xx∈y→∃o∈J∃p∈JX∖y⊆o∧x∈p∧o∩p=∅
33 32 rspcv ⊢X∖y∈Clsd⁡J→∀c∈Clsd⁡J∀x∈X¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅→∀x∈Xx∈y→∃o∈J∃p∈JX∖y⊆o∧x∈p∧o∩p=∅
34 20 33 syl ⊢J∈TopOn⁡X∧y∈J→∀c∈Clsd⁡J∀x∈X¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅→∀x∈Xx∈y→∃o∈J∃p∈JX∖y⊆o∧x∈p∧o∩p=∅
35 ralcom3 ⊢∀x∈Xx∈y→∃o∈J∃p∈JX∖y⊆o∧x∈p∧o∩p=∅↔∀x∈yx∈X→∃o∈J∃p∈JX∖y⊆o∧x∈p∧o∩p=∅
36 toponss ⊢J∈TopOn⁡X∧y∈J→y⊆X
37 36 sselda ⊢J∈TopOn⁡X∧y∈J∧x∈y→x∈X
38 simprr2 ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→x∈p
39 5 ad3antrrr ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→X=⋃J
40 39 difeq1d ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→X∖o=⋃J∖o
41 14 ad3antrrr ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→J∈Top
42 simprll ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→o∈J
43 9 opncld ⊢J∈Top∧o∈J→⋃J∖o∈Clsd⁡J
44 41 42 43 syl2anc ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→⋃J∖o∈Clsd⁡J
45 40 44 eqeltrd ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→X∖o∈Clsd⁡J
46 incom ⊢p∩o=o∩p
47 simprr3 ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→o∩p=∅
48 46 47 eqtrid ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→p∩o=∅
49 simplll ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→J∈TopOn⁡X
50 simprlr ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→p∈J
51 toponss ⊢J∈TopOn⁡X∧p∈J→p⊆X
52 49 50 51 syl2anc ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→p⊆X
53 reldisj ⊢p⊆X→p∩o=∅↔p⊆X∖o
54 52 53 syl ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→p∩o=∅↔p⊆X∖o
55 48 54 mpbid ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→p⊆X∖o
56 9 clsss2 ⊢X∖o∈Clsd⁡J∧p⊆X∖o→cls⁡J⁡p⊆X∖o
57 45 55 56 syl2anc ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→cls⁡J⁡p⊆X∖o
58 simprr1 ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→X∖y⊆o
59 difcom ⊢X∖y⊆o↔X∖o⊆y
60 58 59 sylib ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→X∖o⊆y
61 57 60 sstrd ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→cls⁡J⁡p⊆y
62 38 61 jca ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J∧X∖y⊆o∧x∈p∧o∩p=∅→x∈p∧cls⁡J⁡p⊆y
63 62 expr ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J→X∖y⊆o∧x∈p∧o∩p=∅→x∈p∧cls⁡J⁡p⊆y
64 63 anassrs ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J∧p∈J→X∖y⊆o∧x∈p∧o∩p=∅→x∈p∧cls⁡J⁡p⊆y
65 64 reximdva ⊢J∈TopOn⁡X∧y∈J∧x∈y∧o∈J→∃p∈JX∖y⊆o∧x∈p∧o∩p=∅→∃p∈Jx∈p∧cls⁡J⁡p⊆y
66 65 rexlimdva ⊢J∈TopOn⁡X∧y∈J∧x∈y→∃o∈J∃p∈JX∖y⊆o∧x∈p∧o∩p=∅→∃p∈Jx∈p∧cls⁡J⁡p⊆y
67 37 66 embantd ⊢J∈TopOn⁡X∧y∈J∧x∈y→x∈X→∃o∈J∃p∈JX∖y⊆o∧x∈p∧o∩p=∅→∃p∈Jx∈p∧cls⁡J⁡p⊆y
68 67 ralimdva ⊢J∈TopOn⁡X∧y∈J→∀x∈yx∈X→∃o∈J∃p∈JX∖y⊆o∧x∈p∧o∩p=∅→∀x∈y∃p∈Jx∈p∧cls⁡J⁡p⊆y
69 35 68 biimtrid ⊢J∈TopOn⁡X∧y∈J→∀x∈Xx∈y→∃o∈J∃p∈JX∖y⊆o∧x∈p∧o∩p=∅→∀x∈y∃p∈Jx∈p∧cls⁡J⁡p⊆y
70 34 69 syld ⊢J∈TopOn⁡X∧y∈J→∀c∈Clsd⁡J∀x∈X¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅→∀x∈y∃p∈Jx∈p∧cls⁡J⁡p⊆y
71 70 ralrimdva ⊢J∈TopOn⁡X→∀c∈Clsd⁡J∀x∈X¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅→∀y∈J∀x∈y∃p∈Jx∈p∧cls⁡J⁡p⊆y
72 71 imp ⊢J∈TopOn⁡X∧∀c∈Clsd⁡J∀x∈X¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅→∀y∈J∀x∈y∃p∈Jx∈p∧cls⁡J⁡p⊆y
73 isreg ⊢J∈Reg↔J∈Top∧∀y∈J∀x∈y∃p∈Jx∈p∧cls⁡J⁡p⊆y
74 15 72 73 sylanbrc ⊢J∈TopOn⁡X∧∀c∈Clsd⁡J∀x∈X¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅→J∈Reg
75 13 74 impbida ⊢J∈TopOn⁡X→J∈Reg↔∀c∈Clsd⁡J∀x∈X¬x∈c→∃o∈J∃p∈Jc⊆o∧x∈p∧o∩p=∅