# Metamath Proof Explorer

## Theorem regsep2

Description: In a regular space, a closed set is separated by open sets from a point not in it. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis t1sep.1 ${⊢}{X}=\bigcup {J}$
Assertion regsep2 ${⊢}\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\exists {y}\in {J}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {x}\wedge {A}\in {y}\wedge {x}\cap {y}=\varnothing \right)$

### Proof

Step Hyp Ref Expression
1 t1sep.1 ${⊢}{X}=\bigcup {J}$
2 regtop ${⊢}{J}\in \mathrm{Reg}\to {J}\in \mathrm{Top}$
3 2 ad2antrr ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to {J}\in \mathrm{Top}$
4 elssuni ${⊢}{y}\in {J}\to {y}\subseteq \bigcup {J}$
5 4 1 sseqtrrdi ${⊢}{y}\in {J}\to {y}\subseteq {X}$
6 5 ad2antrl ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to {y}\subseteq {X}$
7 1 clscld ${⊢}\left({J}\in \mathrm{Top}\wedge {y}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({y}\right)\in \mathrm{Clsd}\left({J}\right)$
8 3 6 7 syl2anc ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to \mathrm{cls}\left({J}\right)\left({y}\right)\in \mathrm{Clsd}\left({J}\right)$
9 1 cldopn ${⊢}\mathrm{cls}\left({J}\right)\left({y}\right)\in \mathrm{Clsd}\left({J}\right)\to {X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\in {J}$
10 8 9 syl ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to {X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\in {J}$
11 simprrr ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}$
12 1 clsss3 ${⊢}\left({J}\in \mathrm{Top}\wedge {y}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}$
13 3 6 12 syl2anc ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}$
14 simplr1 ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to {C}\in \mathrm{Clsd}\left({J}\right)$
15 1 cldss ${⊢}{C}\in \mathrm{Clsd}\left({J}\right)\to {C}\subseteq {X}$
16 14 15 syl ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to {C}\subseteq {X}$
17 ssconb ${⊢}\left(\mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\wedge {C}\subseteq {X}\right)\to \left(\mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}↔{C}\subseteq {X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)$
18 13 16 17 syl2anc ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to \left(\mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}↔{C}\subseteq {X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)$
19 11 18 mpbid ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to {C}\subseteq {X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)$
20 simprrl ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to {A}\in {y}$
21 1 sscls ${⊢}\left({J}\in \mathrm{Top}\wedge {y}\subseteq {X}\right)\to {y}\subseteq \mathrm{cls}\left({J}\right)\left({y}\right)$
22 3 6 21 syl2anc ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to {y}\subseteq \mathrm{cls}\left({J}\right)\left({y}\right)$
23 sslin ${⊢}{y}\subseteq \mathrm{cls}\left({J}\right)\left({y}\right)\to \left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap {y}\subseteq \left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap \mathrm{cls}\left({J}\right)\left({y}\right)$
24 22 23 syl ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to \left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap {y}\subseteq \left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap \mathrm{cls}\left({J}\right)\left({y}\right)$
25 incom ${⊢}\left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap \mathrm{cls}\left({J}\right)\left({y}\right)=\mathrm{cls}\left({J}\right)\left({y}\right)\cap \left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)$
26 disjdif ${⊢}\mathrm{cls}\left({J}\right)\left({y}\right)\cap \left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)=\varnothing$
27 25 26 eqtri ${⊢}\left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap \mathrm{cls}\left({J}\right)\left({y}\right)=\varnothing$
28 sseq0 ${⊢}\left(\left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap {y}\subseteq \left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap \mathrm{cls}\left({J}\right)\left({y}\right)\wedge \left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap \mathrm{cls}\left({J}\right)\left({y}\right)=\varnothing \right)\to \left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap {y}=\varnothing$
29 24 27 28 sylancl ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to \left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap {y}=\varnothing$
30 sseq2 ${⊢}{x}={X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\to \left({C}\subseteq {x}↔{C}\subseteq {X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)$
31 ineq1 ${⊢}{x}={X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\to {x}\cap {y}=\left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap {y}$
32 31 eqeq1d ${⊢}{x}={X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\to \left({x}\cap {y}=\varnothing ↔\left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap {y}=\varnothing \right)$
33 30 32 3anbi13d ${⊢}{x}={X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\to \left(\left({C}\subseteq {x}\wedge {A}\in {y}\wedge {x}\cap {y}=\varnothing \right)↔\left({C}\subseteq {X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\wedge {A}\in {y}\wedge \left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap {y}=\varnothing \right)\right)$
34 33 rspcev ${⊢}\left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\in {J}\wedge \left({C}\subseteq {X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\wedge {A}\in {y}\wedge \left({X}\setminus \mathrm{cls}\left({J}\right)\left({y}\right)\right)\cap {y}=\varnothing \right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {x}\wedge {A}\in {y}\wedge {x}\cap {y}=\varnothing \right)$
35 10 19 20 29 34 syl13anc ${⊢}\left(\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\wedge \left({y}\in {J}\wedge \left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)\right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {x}\wedge {A}\in {y}\wedge {x}\cap {y}=\varnothing \right)$
36 simpl ${⊢}\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\to {J}\in \mathrm{Reg}$
37 simpr1 ${⊢}\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\to {C}\in \mathrm{Clsd}\left({J}\right)$
38 1 cldopn ${⊢}{C}\in \mathrm{Clsd}\left({J}\right)\to {X}\setminus {C}\in {J}$
39 37 38 syl ${⊢}\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\to {X}\setminus {C}\in {J}$
40 simpr2 ${⊢}\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\to {A}\in {X}$
41 simpr3 ${⊢}\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\to ¬{A}\in {C}$
42 40 41 eldifd ${⊢}\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\to {A}\in \left({X}\setminus {C}\right)$
43 regsep ${⊢}\left({J}\in \mathrm{Reg}\wedge {X}\setminus {C}\in {J}\wedge {A}\in \left({X}\setminus {C}\right)\right)\to \exists {y}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)$
44 36 39 42 43 syl3anc ${⊢}\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\to \exists {y}\in {J}\phantom{\rule{.4em}{0ex}}\left({A}\in {y}\wedge \mathrm{cls}\left({J}\right)\left({y}\right)\subseteq {X}\setminus {C}\right)$
45 35 44 reximddv ${⊢}\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\to \exists {y}\in {J}\phantom{\rule{.4em}{0ex}}\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {x}\wedge {A}\in {y}\wedge {x}\cap {y}=\varnothing \right)$
46 rexcom ${⊢}\exists {y}\in {J}\phantom{\rule{.4em}{0ex}}\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {x}\wedge {A}\in {y}\wedge {x}\cap {y}=\varnothing \right)↔\exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\exists {y}\in {J}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {x}\wedge {A}\in {y}\wedge {x}\cap {y}=\varnothing \right)$
47 45 46 sylib ${⊢}\left({J}\in \mathrm{Reg}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {A}\in {X}\wedge ¬{A}\in {C}\right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\exists {y}\in {J}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {x}\wedge {A}\in {y}\wedge {x}\cap {y}=\varnothing \right)$