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

Proof

Step Hyp Ref Expression
1 nrmtop ⊢ ( 𝐽 ∈ Nrm → 𝐽 ∈ Top )
2 1 ad2antrr ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) ) ) → 𝐽 ∈ Top )
3 elssuni ⊢ ( 𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽 )
4 3 ad2antrl ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) ) ) → 𝑥 ⊆ ∪ 𝐽 )
5 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
6 5 clscld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
7 2 4 6 syl2anc ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
8 5 cldopn ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) → ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ∈ 𝐽 )
9 7 8 syl ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) ) ) → ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ∈ 𝐽 )
10 simprrl ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) ) ) → 𝐶 ⊆ 𝑥 )
11 incom ⊢ ( 𝐷 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 )
12 simprrr ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ )
13 11 12 eqtrid ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) ) ) → ( 𝐷 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) = ∅ )
14 simplr2 ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) ) ) → 𝐷 ∈ ( Clsd ‘ 𝐽 ) )
15 5 cldss ⊢ ( 𝐷 ∈ ( Clsd ‘ 𝐽 ) → 𝐷 ⊆ ∪ 𝐽 )
16 reldisj ⊢ ( 𝐷 ⊆ ∪ 𝐽 → ( ( 𝐷 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) = ∅ ↔ 𝐷 ⊆ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) )
17 14 15 16 3syl ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) ) ) → ( ( 𝐷 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) = ∅ ↔ 𝐷 ⊆ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) )
18 13 17 mpbid ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) ) ) → 𝐷 ⊆ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) )
19 5 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽 ) → 𝑥 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) )
20 2 4 19 syl2anc ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) ) ) → 𝑥 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) )
21 20 ssrind ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) ) ) → ( 𝑥 ∩ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) )
22 disjdif ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) = ∅
23 sseq0 ⊢ ( ( ( 𝑥 ∩ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) = ∅ ) → ( 𝑥 ∩ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) = ∅ )
24 21 22 23 sylancl ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) ) ) → ( 𝑥 ∩ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) = ∅ )
25 sseq2 ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) → ( 𝐷 ⊆ 𝑦 ↔ 𝐷 ⊆ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) )
26 ineq2 ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) → ( 𝑥 ∩ 𝑦 ) = ( 𝑥 ∩ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) )
27 26 eqeq1d ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ( 𝑥 ∩ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) = ∅ ) )
28 25 27 3anbi23d ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) → ( ( 𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ( 𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ∧ ( 𝑥 ∩ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) = ∅ ) ) )
29 28 rspcev ⊢ ( ( ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ∧ ( 𝑥 ∩ ( ∪ 𝐽 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ) ) = ∅ ) ) → ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
30 9 10 18 24 29 syl13anc ⊢ ( ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) ) ) → ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
31 nrmsep2 ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝐷 ) = ∅ ) )
32 30 31 reximddv ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐷 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐶 ∩ 𝐷 ) = ∅ ) ) → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )