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⁡Jc∩d=∅→∃o∈Jc⊆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∈Jc⊆o∧cls⁡J⁡o∩d=∅
3 2 3exp2 ⊢J∈Nrm→c∈Clsd⁡J→d∈Clsd⁡J→c∩d=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩d=∅
4 3 impd ⊢J∈Nrm→c∈Clsd⁡J∧d∈Clsd⁡J→c∩d=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩d=∅
5 4 ralrimivv ⊢J∈Nrm→∀c∈Clsd⁡J∀d∈Clsd⁡Jc∩d=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩d=∅
6 1 5 jca ⊢J∈Nrm→J∈Top∧∀c∈Clsd⁡J∀d∈Clsd⁡Jc∩d=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩d=∅
7 simpl ⊢J∈Top∧∀c∈Clsd⁡J∀d∈Clsd⁡Jc∩d=∅→∃o∈Jc⊆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∈Jc⊆o∧cls⁡J⁡o∩d=∅↔∃o∈Jc⊆o∧cls⁡J⁡o∩⋃J∖x=∅
17 12 16 imbi12d ⊢d=⋃J∖x→c∩d=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩d=∅↔c∩⋃J∖x=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩⋃J∖x=∅
18 17 rspcv ⊢⋃J∖x∈Clsd⁡J→∀d∈Clsd⁡Jc∩d=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩d=∅→c∩⋃J∖x=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩⋃J∖x=∅
19 10 18 syl ⊢J∈Top∧x∈J∧c∈Clsd⁡J→∀d∈Clsd⁡Jc∩d=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩d=∅→c∩⋃J∖x=∅→∃o∈Jc⊆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∈Jc⊆o∧cls⁡J⁡o∩⋃J∖x=∅↔∃o∈Jc⊆o∧cls⁡J⁡o⊆x
38 26 37 imbi12d ⊢J∈Top∧x∈J∧c∈Clsd⁡J→c∩⋃J∖x=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩⋃J∖x=∅↔c⊆x→∃o∈Jc⊆o∧cls⁡J⁡o⊆x
39 19 38 sylibd ⊢J∈Top∧x∈J∧c∈Clsd⁡J→∀d∈Clsd⁡Jc∩d=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩d=∅→c⊆x→∃o∈Jc⊆o∧cls⁡J⁡o⊆x
40 39 ralimdva ⊢J∈Top∧x∈J→∀c∈Clsd⁡J∀d∈Clsd⁡Jc∩d=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩d=∅→∀c∈Clsd⁡Jc⊆x→∃o∈Jc⊆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∈Jc⊆o∧cls⁡J⁡o⊆x↔c∈Clsd⁡J∧c⊆x→∃o∈Jc⊆o∧cls⁡J⁡o⊆x
46 impexp ⊢c∈Clsd⁡J∧c⊆x→∃o∈Jc⊆o∧cls⁡J⁡o⊆x↔c∈Clsd⁡J→c⊆x→∃o∈Jc⊆o∧cls⁡J⁡o⊆x
47 45 46 bitri ⊢c∈Clsd⁡J∩𝒫x→∃o∈Jc⊆o∧cls⁡J⁡o⊆x↔c∈Clsd⁡J→c⊆x→∃o∈Jc⊆o∧cls⁡J⁡o⊆x
48 47 ralbii2 ⊢∀c∈Clsd⁡J∩𝒫x∃o∈Jc⊆o∧cls⁡J⁡o⊆x↔∀c∈Clsd⁡Jc⊆x→∃o∈Jc⊆o∧cls⁡J⁡o⊆x
49 40 48 imbitrrdi ⊢J∈Top∧x∈J→∀c∈Clsd⁡J∀d∈Clsd⁡Jc∩d=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩d=∅→∀c∈Clsd⁡J∩𝒫x∃o∈Jc⊆o∧cls⁡J⁡o⊆x
50 49 ralrimdva ⊢J∈Top→∀c∈Clsd⁡J∀d∈Clsd⁡Jc∩d=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩d=∅→∀x∈J∀c∈Clsd⁡J∩𝒫x∃o∈Jc⊆o∧cls⁡J⁡o⊆x
51 50 imp ⊢J∈Top∧∀c∈Clsd⁡J∀d∈Clsd⁡Jc∩d=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩d=∅→∀x∈J∀c∈Clsd⁡J∩𝒫x∃o∈Jc⊆o∧cls⁡J⁡o⊆x
52 isnrm ⊢J∈Nrm↔J∈Top∧∀x∈J∀c∈Clsd⁡J∩𝒫x∃o∈Jc⊆o∧cls⁡J⁡o⊆x
53 7 51 52 sylanbrc ⊢J∈Top∧∀c∈Clsd⁡J∀d∈Clsd⁡Jc∩d=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩d=∅→J∈Nrm
54 6 53 impbii ⊢J∈Nrm↔J∈Top∧∀c∈Clsd⁡J∀d∈Clsd⁡Jc∩d=∅→∃o∈Jc⊆o∧cls⁡J⁡o∩d=∅