Metamath Proof Explorer

Theorem isnrm3

Description: A topological space is normal iff any two disjoint closed sets are separated by open sets. (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion isnrm3 ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) )

Proof

Step Hyp Ref Expression
1 nrmtop ⊢ ( 𝐽 ∈ Nrm → 𝐽 ∈ Top )
2 nrmsep ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑐 ∩ 𝑑 ) = ∅ ) ) → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
3 2 3exp2 ⊢ ( 𝐽 ∈ Nrm → ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑑 ∈ ( Clsd ‘ 𝐽 ) → ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) ) )
4 3 impd ⊢ ( 𝐽 ∈ Nrm → ( ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) )
5 4 ralrimivv ⊢ ( 𝐽 ∈ Nrm → ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )
6 1 5 jca ⊢ ( 𝐽 ∈ Nrm → ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) )
7 simpl ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) → 𝐽 ∈ Top )
8 simpr1 ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑐 ⊆ 𝑥 )
9 simpr2 ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑑 ⊆ 𝑦 )
10 sslin ⊢ ( 𝑑 ⊆ 𝑦 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑦 ) )
11 9 10 syl ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑦 ) )
12 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
13 12 opncld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
14 13 ad4ant13 ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( ∪ 𝐽 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
15 simpr3 ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( 𝑥 ∩ 𝑦 ) = ∅ )
16 simpllr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑥 ∈ 𝐽 )
17 elssuni ⊢ ( 𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽 )
18 reldisj ⊢ ( 𝑥 ⊆ ∪ 𝐽 → ( ( 𝑥 ∩ 𝑦 ) = ∅ ↔ 𝑥 ⊆ ( ∪ 𝐽 ∖ 𝑦 ) ) )
19 16 17 18 3syl ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ ↔ 𝑥 ⊆ ( ∪ 𝐽 ∖ 𝑦 ) ) )
20 15 19 mpbid ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑥 ⊆ ( ∪ 𝐽 ∖ 𝑦 ) )
21 12 clsss2 ⊢ ( ( ( ∪ 𝐽 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ⊆ ( ∪ 𝐽 ∖ 𝑦 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ ( ∪ 𝐽 ∖ 𝑦 ) )
22 ssdifin0 ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ ( ∪ 𝐽 ∖ 𝑦 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑦 ) = ∅ )
23 21 22 syl ⊢ ( ( ( ∪ 𝐽 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ⊆ ( ∪ 𝐽 ∖ 𝑦 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑦 ) = ∅ )
24 14 20 23 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑦 ) = ∅ )
25 sseq0 ⊢ ( ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑦 ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ )
26 11 24 25 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ )
27 8 26 jca ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) )
28 27 rexlimdva2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ( ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) )
29 28 reximdva ⊢ ( 𝐽 ∈ Top → ( ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ∃ 𝑥 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) )
30 29 imim2d ⊢ ( 𝐽 ∈ Top → ( ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) ) )
31 30 ralimdv ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) ) )
32 31 ralimdv ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) ) )
33 32 imp ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) → ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) )
34 isnrm2 ⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) ) )
35 7 33 34 sylanbrc ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) → 𝐽 ∈ Nrm )
36 6 35 impbii ⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) )