# Metamath Proof Explorer

## Theorem nrmsep

Description: In a normal space, disjoint closed sets are separated by open sets. (Contributed by Jeff Hankins, 1-Feb-2010)

Ref Expression
Assertion nrmsep ${⊢}\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\exists {y}\in {J}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {x}\wedge {D}\subseteq {y}\wedge {x}\cap {y}=\varnothing \right)$

### Proof

Step Hyp Ref Expression
1 nrmtop ${⊢}{J}\in \mathrm{Nrm}\to {J}\in \mathrm{Top}$
2 1 ad2antrr ${⊢}\left(\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\wedge \left({x}\in {J}\wedge \left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)\right)\right)\to {J}\in \mathrm{Top}$
3 elssuni ${⊢}{x}\in {J}\to {x}\subseteq \bigcup {J}$
4 3 ad2antrl ${⊢}\left(\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\wedge \left({x}\in {J}\wedge \left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)\right)\right)\to {x}\subseteq \bigcup {J}$
5 eqid ${⊢}\bigcup {J}=\bigcup {J}$
6 5 clscld ${⊢}\left({J}\in \mathrm{Top}\wedge {x}\subseteq \bigcup {J}\right)\to \mathrm{cls}\left({J}\right)\left({x}\right)\in \mathrm{Clsd}\left({J}\right)$
7 2 4 6 syl2anc ${⊢}\left(\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\wedge \left({x}\in {J}\wedge \left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)\right)\right)\to \mathrm{cls}\left({J}\right)\left({x}\right)\in \mathrm{Clsd}\left({J}\right)$
8 5 cldopn ${⊢}\mathrm{cls}\left({J}\right)\left({x}\right)\in \mathrm{Clsd}\left({J}\right)\to \bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\in {J}$
9 7 8 syl ${⊢}\left(\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\wedge \left({x}\in {J}\wedge \left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)\right)\right)\to \bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\in {J}$
10 simprrl ${⊢}\left(\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\wedge \left({x}\in {J}\wedge \left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)\right)\right)\to {C}\subseteq {x}$
11 incom ${⊢}{D}\cap \mathrm{cls}\left({J}\right)\left({x}\right)=\mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}$
12 simprrr ${⊢}\left(\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\wedge \left({x}\in {J}\wedge \left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)\right)\right)\to \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing$
13 11 12 syl5eq ${⊢}\left(\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\wedge \left({x}\in {J}\wedge \left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)\right)\right)\to {D}\cap \mathrm{cls}\left({J}\right)\left({x}\right)=\varnothing$
14 simplr2 ${⊢}\left(\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\wedge \left({x}\in {J}\wedge \left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)\right)\right)\to {D}\in \mathrm{Clsd}\left({J}\right)$
15 5 cldss ${⊢}{D}\in \mathrm{Clsd}\left({J}\right)\to {D}\subseteq \bigcup {J}$
16 reldisj ${⊢}{D}\subseteq \bigcup {J}\to \left({D}\cap \mathrm{cls}\left({J}\right)\left({x}\right)=\varnothing ↔{D}\subseteq \bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)$
17 14 15 16 3syl ${⊢}\left(\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\wedge \left({x}\in {J}\wedge \left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)\right)\right)\to \left({D}\cap \mathrm{cls}\left({J}\right)\left({x}\right)=\varnothing ↔{D}\subseteq \bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)$
18 13 17 mpbid ${⊢}\left(\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\wedge \left({x}\in {J}\wedge \left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)\right)\right)\to {D}\subseteq \bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)$
19 5 sscls ${⊢}\left({J}\in \mathrm{Top}\wedge {x}\subseteq \bigcup {J}\right)\to {x}\subseteq \mathrm{cls}\left({J}\right)\left({x}\right)$
20 2 4 19 syl2anc ${⊢}\left(\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\wedge \left({x}\in {J}\wedge \left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)\right)\right)\to {x}\subseteq \mathrm{cls}\left({J}\right)\left({x}\right)$
21 20 ssrind ${⊢}\left(\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\wedge \left({x}\in {J}\wedge \left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)\right)\right)\to {x}\cap \left(\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)\subseteq \mathrm{cls}\left({J}\right)\left({x}\right)\cap \left(\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)$
22 disjdif ${⊢}\mathrm{cls}\left({J}\right)\left({x}\right)\cap \left(\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)=\varnothing$
23 sseq0 ${⊢}\left({x}\cap \left(\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)\subseteq \mathrm{cls}\left({J}\right)\left({x}\right)\cap \left(\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap \left(\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)=\varnothing \right)\to {x}\cap \left(\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)=\varnothing$
24 21 22 23 sylancl ${⊢}\left(\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\wedge \left({x}\in {J}\wedge \left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)\right)\right)\to {x}\cap \left(\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)=\varnothing$
25 sseq2 ${⊢}{y}=\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\to \left({D}\subseteq {y}↔{D}\subseteq \bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)$
26 ineq2 ${⊢}{y}=\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\to {x}\cap {y}={x}\cap \left(\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)$
27 26 eqeq1d ${⊢}{y}=\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\to \left({x}\cap {y}=\varnothing ↔{x}\cap \left(\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)=\varnothing \right)$
28 25 27 3anbi23d ${⊢}{y}=\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\to \left(\left({C}\subseteq {x}\wedge {D}\subseteq {y}\wedge {x}\cap {y}=\varnothing \right)↔\left({C}\subseteq {x}\wedge {D}\subseteq \bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\wedge {x}\cap \left(\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)=\varnothing \right)\right)$
29 28 rspcev ${⊢}\left(\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\in {J}\wedge \left({C}\subseteq {x}\wedge {D}\subseteq \bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\wedge {x}\cap \left(\bigcup {J}\setminus \mathrm{cls}\left({J}\right)\left({x}\right)\right)=\varnothing \right)\right)\to \exists {y}\in {J}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {x}\wedge {D}\subseteq {y}\wedge {x}\cap {y}=\varnothing \right)$
30 9 10 18 24 29 syl13anc ${⊢}\left(\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\wedge \left({x}\in {J}\wedge \left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)\right)\right)\to \exists {y}\in {J}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {x}\wedge {D}\subseteq {y}\wedge {x}\cap {y}=\varnothing \right)$
31 nrmsep2 ${⊢}\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {x}\wedge \mathrm{cls}\left({J}\right)\left({x}\right)\cap {D}=\varnothing \right)$
32 30 31 reximddv ${⊢}\left({J}\in \mathrm{Nrm}\wedge \left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {D}\in \mathrm{Clsd}\left({J}\right)\wedge {C}\cap {D}=\varnothing \right)\right)\to \exists {x}\in {J}\phantom{\rule{.4em}{0ex}}\exists {y}\in {J}\phantom{\rule{.4em}{0ex}}\left({C}\subseteq {x}\wedge {D}\subseteq {y}\wedge {x}\cap {y}=\varnothing \right)$