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 ∈ J C ⊆ 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 ∈ J C ⊆ x ∧ cls ⁡ J ⁡ x ⊆ ⋃ J ∖ D
13 1 5 6 11 12 syl13anc ⊢ J ∈ Nrm ∧ C ∈ Clsd ⁡ J ∧ D ∈ Clsd ⁡ J ∧ C ∩ D = ∅ → ∃ x ∈ J C ⊆ 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 ∈ J C ⊆ x ∧ cls ⁡ J ⁡ x ⊆ ⋃ J ∖ D → ∃ x ∈ J C ⊆ x ∧ cls ⁡ J ⁡ x ∩ D = ∅
17 13 16 syl ⊢ J ∈ Nrm ∧ C ∈ Clsd ⁡ J ∧ D ∈ Clsd ⁡ J ∧ C ∩ D = ∅ → ∃ x ∈ J C ⊆ x ∧ cls ⁡ J ⁡ x ∩ D = ∅