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 ‘ 𝐽 ) ( ( 𝑐𝑑 ) = ∅ → ∃ 𝑥𝐽𝑦𝐽 ( 𝑐𝑥𝑑𝑦 ∧ ( 𝑥𝑦 ) = ∅ ) ) ) )