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 ( ( 𝐽 ∈ Nrm ∧ ( 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐵 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 isnrm ⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝐽 ∀ 𝑧 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑦 ) ∃ 𝑥 ∈ 𝐽 ( 𝑧 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑦 ) ) )
2 pweq ⊢ ( 𝑦 = 𝐴 → 𝒫 𝑦 = 𝒫 𝐴 )
3 2 ineq2d ⊢ ( 𝑦 = 𝐴 → ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑦 ) = ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝐴 ) )
4 sseq2 ⊢ ( 𝑦 = 𝐴 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑦 ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) )
5 4 anbi2d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑧 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑦 ) ↔ ( 𝑧 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) ) )
6 5 rexbidv ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑧 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑧 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) ) )
7 3 6 raleqbidv ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑧 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑦 ) ∃ 𝑥 ∈ 𝐽 ( 𝑧 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑦 ) ↔ ∀ 𝑧 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝐴 ) ∃ 𝑥 ∈ 𝐽 ( 𝑧 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) ) )
8 7 rspccv ⊢ ( ∀ 𝑦 ∈ 𝐽 ∀ 𝑧 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑦 ) ∃ 𝑥 ∈ 𝐽 ( 𝑧 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑦 ) → ( 𝐴 ∈ 𝐽 → ∀ 𝑧 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝐴 ) ∃ 𝑥 ∈ 𝐽 ( 𝑧 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) ) )
9 1 8 simplbiim ⊢ ( 𝐽 ∈ Nrm → ( 𝐴 ∈ 𝐽 → ∀ 𝑧 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝐴 ) ∃ 𝑥 ∈ 𝐽 ( 𝑧 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) ) )
10 elin ⊢ ( 𝐵 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝐴 ) ↔ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ∈ 𝒫 𝐴 ) )
11 elpwg ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ( 𝐵 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
12 11 pm5.32i ⊢ ( ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ∈ 𝒫 𝐴 ) ↔ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) )
13 10 12 bitri ⊢ ( 𝐵 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝐴 ) ↔ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) )
14 cleq1lem ⊢ ( 𝑧 = 𝐵 → ( ( 𝑧 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) ↔ ( 𝐵 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) ) )
15 14 rexbidv ⊢ ( 𝑧 = 𝐵 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑧 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝐵 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) ) )
16 15 rspccv ⊢ ( ∀ 𝑧 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝐴 ) ∃ 𝑥 ∈ 𝐽 ( 𝑧 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) → ( 𝐵 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝐴 ) → ∃ 𝑥 ∈ 𝐽 ( 𝐵 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) ) )
17 13 16 syl5bir ⊢ ( ∀ 𝑧 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝐴 ) ∃ 𝑥 ∈ 𝐽 ( 𝑧 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) → ( ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → ∃ 𝑥 ∈ 𝐽 ( 𝐵 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) ) )
18 9 17 syl6 ⊢ ( 𝐽 ∈ Nrm → ( 𝐴 ∈ 𝐽 → ( ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) → ∃ 𝑥 ∈ 𝐽 ( 𝐵 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) ) ) )
19 18 exp4a ⊢ ( 𝐽 ∈ Nrm → ( 𝐴 ∈ 𝐽 → ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → ( 𝐵 ⊆ 𝐴 → ∃ 𝑥 ∈ 𝐽 ( 𝐵 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) ) ) ) )
20 19 3imp2 ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐵 ⊆ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝐵 ⊆ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝐴 ) )