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 ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) )