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 ∈ J B ⊆ x ∧ cls ⁡ J ⁡ x ⊆ A

Proof

Step Hyp Ref Expression
1 isnrm ⊢ J ∈ Nrm ↔ J ∈ Top ∧ ∀ y ∈ J ∀ z ∈ Clsd ⁡ J ∩ 𝒫 y ∃ x ∈ J z ⊆ 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 ∈ J z ⊆ x ∧ cls ⁡ J ⁡ x ⊆ y ↔ ∃ x ∈ J z ⊆ x ∧ cls ⁡ J ⁡ x ⊆ A
7 3 6 raleqbidv ⊢ y = A → ∀ z ∈ Clsd ⁡ J ∩ 𝒫 y ∃ x ∈ J z ⊆ x ∧ cls ⁡ J ⁡ x ⊆ y ↔ ∀ z ∈ Clsd ⁡ J ∩ 𝒫 A ∃ x ∈ J z ⊆ x ∧ cls ⁡ J ⁡ x ⊆ A
8 7 rspccv ⊢ ∀ y ∈ J ∀ z ∈ Clsd ⁡ J ∩ 𝒫 y ∃ x ∈ J z ⊆ x ∧ cls ⁡ J ⁡ x ⊆ y → A ∈ J → ∀ z ∈ Clsd ⁡ J ∩ 𝒫 A ∃ x ∈ J z ⊆ x ∧ cls ⁡ J ⁡ x ⊆ A
9 1 8 simplbiim ⊢ J ∈ Nrm → A ∈ J → ∀ z ∈ Clsd ⁡ J ∩ 𝒫 A ∃ x ∈ J z ⊆ 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 ∈ J z ⊆ x ∧ cls ⁡ J ⁡ x ⊆ A ↔ ∃ x ∈ J B ⊆ x ∧ cls ⁡ J ⁡ x ⊆ A
16 15 rspccv ⊢ ∀ z ∈ Clsd ⁡ J ∩ 𝒫 A ∃ x ∈ J z ⊆ x ∧ cls ⁡ J ⁡ x ⊆ A → B ∈ Clsd ⁡ J ∩ 𝒫 A → ∃ x ∈ J B ⊆ x ∧ cls ⁡ J ⁡ x ⊆ A
17 13 16 syl5bir ⊢ ∀ z ∈ Clsd ⁡ J ∩ 𝒫 A ∃ x ∈ J z ⊆ x ∧ cls ⁡ J ⁡ x ⊆ A → B ∈ Clsd ⁡ J ∧ B ⊆ A → ∃ x ∈ J B ⊆ x ∧ cls ⁡ J ⁡ x ⊆ A
18 9 17 syl6 ⊢ J ∈ Nrm → A ∈ J → B ∈ Clsd ⁡ J ∧ B ⊆ A → ∃ x ∈ J B ⊆ x ∧ cls ⁡ J ⁡ x ⊆ A
19 18 exp4a ⊢ J ∈ Nrm → A ∈ J → B ∈ Clsd ⁡ J → B ⊆ A → ∃ x ∈ J B ⊆ x ∧ cls ⁡ J ⁡ x ⊆ A
20 19 3imp2 ⊢ J ∈ Nrm ∧ A ∈ J ∧ B ∈ Clsd ⁡ J ∧ B ⊆ A → ∃ x ∈ J B ⊆ x ∧ cls ⁡ J ⁡ x ⊆ A