Metamath Proof Explorer

Theorem nrmsep3

Description: In a normal space, given a closed set B inside an open set A , there is an open set x such that B C_ x C_ cls ( x ) C_ A . (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion nrmsep3 ⊢J∈Nrm∧A∈J∧B∈Clsd⁡J∧B⊆A→∃x∈JB⊆x∧cls⁡J⁡x⊆A

Proof

Step Hyp Ref Expression
1 isnrm ⊢J∈Nrm↔J∈Top∧∀y∈J∀z∈Clsd⁡J∩𝒫y∃x∈Jz⊆x∧cls⁡J⁡x⊆y
2 pweq ⊢y=A→𝒫y=𝒫A
3 2 ineq2d ⊢y=A→Clsd⁡J∩𝒫y=Clsd⁡J∩𝒫A
4 sseq2 ⊢y=A→cls⁡J⁡x⊆y↔cls⁡J⁡x⊆A
5 4 anbi2d ⊢y=A→z⊆x∧cls⁡J⁡x⊆y↔z⊆x∧cls⁡J⁡x⊆A
6 5 rexbidv ⊢y=A→∃x∈Jz⊆x∧cls⁡J⁡x⊆y↔∃x∈Jz⊆x∧cls⁡J⁡x⊆A
7 3 6 raleqbidv ⊢y=A→∀z∈Clsd⁡J∩𝒫y∃x∈Jz⊆x∧cls⁡J⁡x⊆y↔∀z∈Clsd⁡J∩𝒫A∃x∈Jz⊆x∧cls⁡J⁡x⊆A
8 7 rspccv ⊢∀y∈J∀z∈Clsd⁡J∩𝒫y∃x∈Jz⊆x∧cls⁡J⁡x⊆y→A∈J→∀z∈Clsd⁡J∩𝒫A∃x∈Jz⊆x∧cls⁡J⁡x⊆A
9 1 8 simplbiim ⊢J∈Nrm→A∈J→∀z∈Clsd⁡J∩𝒫A∃x∈Jz⊆x∧cls⁡J⁡x⊆A
10 elin ⊢B∈Clsd⁡J∩𝒫A↔B∈Clsd⁡J∧B∈𝒫A
11 elpwg ⊢B∈Clsd⁡J→B∈𝒫A↔B⊆A
12 11 pm5.32i ⊢B∈Clsd⁡J∧B∈𝒫A↔B∈Clsd⁡J∧B⊆A
13 10 12 bitri ⊢B∈Clsd⁡J∩𝒫A↔B∈Clsd⁡J∧B⊆A
14 cleq1lem ⊢z=B→z⊆x∧cls⁡J⁡x⊆A↔B⊆x∧cls⁡J⁡x⊆A
15 14 rexbidv ⊢z=B→∃x∈Jz⊆x∧cls⁡J⁡x⊆A↔∃x∈JB⊆x∧cls⁡J⁡x⊆A
16 15 rspccv ⊢∀z∈Clsd⁡J∩𝒫A∃x∈Jz⊆x∧cls⁡J⁡x⊆A→B∈Clsd⁡J∩𝒫A→∃x∈JB⊆x∧cls⁡J⁡x⊆A
17 13 16 biimtrrid ⊢∀z∈Clsd⁡J∩𝒫A∃x∈Jz⊆x∧cls⁡J⁡x⊆A→B∈Clsd⁡J∧B⊆A→∃x∈JB⊆x∧cls⁡J⁡x⊆A
18 9 17 syl6 ⊢J∈Nrm→A∈J→B∈Clsd⁡J∧B⊆A→∃x∈JB⊆x∧cls⁡J⁡x⊆A
19 18 exp4a ⊢J∈Nrm→A∈J→B∈Clsd⁡J→B⊆A→∃x∈JB⊆x∧cls⁡J⁡x⊆A
20 19 3imp2 ⊢J∈Nrm∧A∈J∧B∈Clsd⁡J∧B⊆A→∃x∈JB⊆x∧cls⁡J⁡x⊆A