Metamath Proof Explorer

Theorem isnrm2

Description: An alternate characterization of normality. This is the important property in the proof of Urysohn's lemma. (Contributed by Jeff Hankins, 1-Feb-2010) (Proof shortened by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion isnrm2 ⊢ J ∈ Nrm ↔ J ∈ Top ∧ ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅

Proof

Step Hyp Ref Expression
1 nrmtop ⊢ J ∈ Nrm → J ∈ Top
2 nrmsep2 ⊢ J ∈ Nrm ∧ c ∈ Clsd ⁡ J ∧ d ∈ Clsd ⁡ J ∧ c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅
3 2 3exp2 ⊢ J ∈ Nrm → c ∈ Clsd ⁡ J → d ∈ Clsd ⁡ J → c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅
4 3 impd ⊢ J ∈ Nrm → c ∈ Clsd ⁡ J ∧ d ∈ Clsd ⁡ J → c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅
5 4 ralrimivv ⊢ J ∈ Nrm → ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅
6 1 5 jca ⊢ J ∈ Nrm → J ∈ Top ∧ ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅
7 simpl ⊢ J ∈ Top ∧ ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅ → J ∈ Top
8 eqid ⊢ ⋃ J = ⋃ J
9 8 opncld ⊢ J ∈ Top ∧ x ∈ J → ⋃ J ∖ x ∈ Clsd ⁡ J
10 9 adantr ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J → ⋃ J ∖ x ∈ Clsd ⁡ J
11 ineq2 ⊢ d = ⋃ J ∖ x → c ∩ d = c ∩ ⋃ J ∖ x
12 11 eqeq1d ⊢ d = ⋃ J ∖ x → c ∩ d = ∅ ↔ c ∩ ⋃ J ∖ x = ∅
13 ineq2 ⊢ d = ⋃ J ∖ x → cls ⁡ J ⁡ o ∩ d = cls ⁡ J ⁡ o ∩ ⋃ J ∖ x
14 13 eqeq1d ⊢ d = ⋃ J ∖ x → cls ⁡ J ⁡ o ∩ d = ∅ ↔ cls ⁡ J ⁡ o ∩ ⋃ J ∖ x = ∅
15 14 anbi2d ⊢ d = ⋃ J ∖ x → c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅ ↔ c ⊆ o ∧ cls ⁡ J ⁡ o ∩ ⋃ J ∖ x = ∅
16 15 rexbidv ⊢ d = ⋃ J ∖ x → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅ ↔ ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ ⋃ J ∖ x = ∅
17 12 16 imbi12d ⊢ d = ⋃ J ∖ x → c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅ ↔ c ∩ ⋃ J ∖ x = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ ⋃ J ∖ x = ∅
18 17 rspcv ⊢ ⋃ J ∖ x ∈ Clsd ⁡ J → ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅ → c ∩ ⋃ J ∖ x = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ ⋃ J ∖ x = ∅
19 10 18 syl ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J → ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅ → c ∩ ⋃ J ∖ x = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ ⋃ J ∖ x = ∅
20 inssdif0 ⊢ c ∩ ⋃ J ⊆ x ↔ c ∩ ⋃ J ∖ x = ∅
21 8 cldss ⊢ c ∈ Clsd ⁡ J → c ⊆ ⋃ J
22 21 adantl ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J → c ⊆ ⋃ J
23 df-ss ⊢ c ⊆ ⋃ J ↔ c ∩ ⋃ J = c
24 22 23 sylib ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J → c ∩ ⋃ J = c
25 24 sseq1d ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J → c ∩ ⋃ J ⊆ x ↔ c ⊆ x
26 20 25 bitr3id ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J → c ∩ ⋃ J ∖ x = ∅ ↔ c ⊆ x
27 inssdif0 ⊢ cls ⁡ J ⁡ o ∩ ⋃ J ⊆ x ↔ cls ⁡ J ⁡ o ∩ ⋃ J ∖ x = ∅
28 simpll ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J → J ∈ Top
29 elssuni ⊢ o ∈ J → o ⊆ ⋃ J
30 8 clsss3 ⊢ J ∈ Top ∧ o ⊆ ⋃ J → cls ⁡ J ⁡ o ⊆ ⋃ J
31 28 29 30 syl2an ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J ∧ o ∈ J → cls ⁡ J ⁡ o ⊆ ⋃ J
32 df-ss ⊢ cls ⁡ J ⁡ o ⊆ ⋃ J ↔ cls ⁡ J ⁡ o ∩ ⋃ J = cls ⁡ J ⁡ o
33 31 32 sylib ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J ∧ o ∈ J → cls ⁡ J ⁡ o ∩ ⋃ J = cls ⁡ J ⁡ o
34 33 sseq1d ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J ∧ o ∈ J → cls ⁡ J ⁡ o ∩ ⋃ J ⊆ x ↔ cls ⁡ J ⁡ o ⊆ x
35 27 34 bitr3id ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J ∧ o ∈ J → cls ⁡ J ⁡ o ∩ ⋃ J ∖ x = ∅ ↔ cls ⁡ J ⁡ o ⊆ x
36 35 anbi2d ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J ∧ o ∈ J → c ⊆ o ∧ cls ⁡ J ⁡ o ∩ ⋃ J ∖ x = ∅ ↔ c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x
37 36 rexbidva ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ ⋃ J ∖ x = ∅ ↔ ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x
38 26 37 imbi12d ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J → c ∩ ⋃ J ∖ x = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ ⋃ J ∖ x = ∅ ↔ c ⊆ x → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x
39 19 38 sylibd ⊢ J ∈ Top ∧ x ∈ J ∧ c ∈ Clsd ⁡ J → ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅ → c ⊆ x → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x
40 39 ralimdva ⊢ J ∈ Top ∧ x ∈ J → ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅ → ∀ c ∈ Clsd ⁡ J c ⊆ x → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x
41 elin ⊢ c ∈ Clsd ⁡ J ∩ 𝒫 x ↔ c ∈ Clsd ⁡ J ∧ c ∈ 𝒫 x
42 velpw ⊢ c ∈ 𝒫 x ↔ c ⊆ x
43 42 anbi2i ⊢ c ∈ Clsd ⁡ J ∧ c ∈ 𝒫 x ↔ c ∈ Clsd ⁡ J ∧ c ⊆ x
44 41 43 bitri ⊢ c ∈ Clsd ⁡ J ∩ 𝒫 x ↔ c ∈ Clsd ⁡ J ∧ c ⊆ x
45 44 imbi1i ⊢ c ∈ Clsd ⁡ J ∩ 𝒫 x → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x ↔ c ∈ Clsd ⁡ J ∧ c ⊆ x → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x
46 impexp ⊢ c ∈ Clsd ⁡ J ∧ c ⊆ x → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x ↔ c ∈ Clsd ⁡ J → c ⊆ x → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x
47 45 46 bitri ⊢ c ∈ Clsd ⁡ J ∩ 𝒫 x → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x ↔ c ∈ Clsd ⁡ J → c ⊆ x → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x
48 47 ralbii2 ⊢ ∀ c ∈ Clsd ⁡ J ∩ 𝒫 x ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x ↔ ∀ c ∈ Clsd ⁡ J c ⊆ x → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x
49 40 48 syl6ibr ⊢ J ∈ Top ∧ x ∈ J → ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅ → ∀ c ∈ Clsd ⁡ J ∩ 𝒫 x ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x
50 49 ralrimdva ⊢ J ∈ Top → ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅ → ∀ x ∈ J ∀ c ∈ Clsd ⁡ J ∩ 𝒫 x ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x
51 50 imp ⊢ J ∈ Top ∧ ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅ → ∀ x ∈ J ∀ c ∈ Clsd ⁡ J ∩ 𝒫 x ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x
52 isnrm ⊢ J ∈ Nrm ↔ J ∈ Top ∧ ∀ x ∈ J ∀ c ∈ Clsd ⁡ J ∩ 𝒫 x ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ⊆ x
53 7 51 52 sylanbrc ⊢ J ∈ Top ∧ ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅ → J ∈ Nrm
54 6 53 impbii ⊢ J ∈ Nrm ↔ J ∈ Top ∧ ∀ c ∈ Clsd ⁡ J ∀ d ∈ Clsd ⁡ J c ∩ d = ∅ → ∃ o ∈ J c ⊆ o ∧ cls ⁡ J ⁡ o ∩ d = ∅