Metamath Proof Explorer

Theorem nrmsep2

Description: In a normal space, any two disjoint closed sets have the property that each one is a subset of an open set whose closure is disjoint from the other. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion nrmsep2 ⊢J∈Nrm∧C∈Clsd⁡J∧D∈Clsd⁡J∧C∩D=∅→∃x∈JC⊆x∧cls⁡J⁡x∩D=∅

Proof

Step Hyp Ref Expression
1 simpl ⊢J∈Nrm∧C∈Clsd⁡J∧D∈Clsd⁡J∧C∩D=∅→J∈Nrm
2 simpr2 ⊢J∈Nrm∧C∈Clsd⁡J∧D∈Clsd⁡J∧C∩D=∅→D∈Clsd⁡J
3 eqid ⊢⋃J=⋃J
4 3 cldopn ⊢D∈Clsd⁡J→⋃J∖D∈J
5 2 4 syl ⊢J∈Nrm∧C∈Clsd⁡J∧D∈Clsd⁡J∧C∩D=∅→⋃J∖D∈J
6 simpr1 ⊢J∈Nrm∧C∈Clsd⁡J∧D∈Clsd⁡J∧C∩D=∅→C∈Clsd⁡J
7 simpr3 ⊢J∈Nrm∧C∈Clsd⁡J∧D∈Clsd⁡J∧C∩D=∅→C∩D=∅
8 3 cldss ⊢C∈Clsd⁡J→C⊆⋃J
9 reldisj ⊢C⊆⋃J→C∩D=∅↔C⊆⋃J∖D
10 6 8 9 3syl ⊢J∈Nrm∧C∈Clsd⁡J∧D∈Clsd⁡J∧C∩D=∅→C∩D=∅↔C⊆⋃J∖D
11 7 10 mpbid ⊢J∈Nrm∧C∈Clsd⁡J∧D∈Clsd⁡J∧C∩D=∅→C⊆⋃J∖D
12 nrmsep3 ⊢J∈Nrm∧⋃J∖D∈J∧C∈Clsd⁡J∧C⊆⋃J∖D→∃x∈JC⊆x∧cls⁡J⁡x⊆⋃J∖D
13 1 5 6 11 12 syl13anc ⊢J∈Nrm∧C∈Clsd⁡J∧D∈Clsd⁡J∧C∩D=∅→∃x∈JC⊆x∧cls⁡J⁡x⊆⋃J∖D
14 ssdifin0 ⊢cls⁡J⁡x⊆⋃J∖D→cls⁡J⁡x∩D=∅
15 14 anim2i ⊢C⊆x∧cls⁡J⁡x⊆⋃J∖D→C⊆x∧cls⁡J⁡x∩D=∅
16 15 reximi ⊢∃x∈JC⊆x∧cls⁡J⁡x⊆⋃J∖D→∃x∈JC⊆x∧cls⁡J⁡x∩D=∅
17 13 16 syl ⊢J∈Nrm∧C∈Clsd⁡J∧D∈Clsd⁡J∧C∩D=∅→∃x∈JC⊆x∧cls⁡J⁡x∩D=∅