This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) → 𝐽 ∈ Nrm )
2 simpr2 ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) → 𝐷 ∈ ( Clsd ‘ 𝐽 ) )
3 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
4 3 cldopn ⊢ ( 𝐷 ∈ ( Clsd ‘ 𝐽 ) → ( ∪ 𝐽 ∖ 𝐷 ) ∈ 𝐽 )
5 2 4 syl ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) → ( ∪ 𝐽 ∖ 𝐷 ) ∈ 𝐽 )
6 simpr1 ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) → 𝐶 ∈ ( Clsd ‘ 𝐽 ) )
7 simpr3 ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) → ( 𝐶 ∩ 𝐷 ) = ∅ )
8 3 cldss ⊢ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) → 𝐶 ⊆ ∪ 𝐽 )
9 reldisj ⊢ ( 𝐶 ⊆ ∪ 𝐽 → ( ( 𝐶 ∩ 𝐷 ) = ∅ ↔ 𝐶 ⊆ ( ∪ 𝐽 ∖ 𝐷 ) ) )
10 6 8 9 3syl ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) → ( ( 𝐶 ∩ 𝐷 ) = ∅ ↔ 𝐶 ⊆ ( ∪ 𝐽 ∖ 𝐷 ) ) )
11 7 10 mpbid ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) → 𝐶 ⊆ ( ∪ 𝐽 ∖ 𝐷 ) )
12 nrmsep3 ⊢ ( ( 𝐽 ∈ Nrm ∧ ( ( ∪ 𝐽 ∖ 𝐷 ) ∈ 𝐽 ∧ 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐶 ⊆ ( ∪ 𝐽 ∖ 𝐷 ) ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ ( ∪ 𝐽 ∖ 𝐷 ) ) )
13 1 5 6 11 12 syl13anc ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ ( ∪ 𝐽 ∖ 𝐷 ) ) )
14 ssdifin0 ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ ( ∪ 𝐽 ∖ 𝐷 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ )
15 14 anim2i ⊢ ( ( 𝐶 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ ( ∪ 𝐽 ∖ 𝐷 ) ) → ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) )
16 15 reximi ⊢ ( ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ ( ∪ 𝐽 ∖ 𝐷 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) )
17 13 16 syl ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) )