# Metamath Proof Explorer

## Theorem regsep

Description: In a regular space, every neighborhood of a point contains a closed subneighborhood. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion regsep $⊢ J ∈ Reg ∧ U ∈ J ∧ A ∈ U → ∃ x ∈ J A ∈ x ∧ cls ⁡ J ⁡ x ⊆ U$

### Proof

Step Hyp Ref Expression
1 isreg $⊢ J ∈ Reg ↔ J ∈ Top ∧ ∀ y ∈ J ∀ z ∈ y ∃ x ∈ J z ∈ x ∧ cls ⁡ J ⁡ x ⊆ y$
2 sseq2 $⊢ y = U → cls ⁡ J ⁡ x ⊆ y ↔ cls ⁡ J ⁡ x ⊆ U$
3 2 anbi2d $⊢ y = U → z ∈ x ∧ cls ⁡ J ⁡ x ⊆ y ↔ z ∈ x ∧ cls ⁡ J ⁡ x ⊆ U$
4 3 rexbidv $⊢ y = U → ∃ x ∈ J z ∈ x ∧ cls ⁡ J ⁡ x ⊆ y ↔ ∃ x ∈ J z ∈ x ∧ cls ⁡ J ⁡ x ⊆ U$
5 4 raleqbi1dv $⊢ y = U → ∀ z ∈ y ∃ x ∈ J z ∈ x ∧ cls ⁡ J ⁡ x ⊆ y ↔ ∀ z ∈ U ∃ x ∈ J z ∈ x ∧ cls ⁡ J ⁡ x ⊆ U$
6 5 rspccv $⊢ ∀ y ∈ J ∀ z ∈ y ∃ x ∈ J z ∈ x ∧ cls ⁡ J ⁡ x ⊆ y → U ∈ J → ∀ z ∈ U ∃ x ∈ J z ∈ x ∧ cls ⁡ J ⁡ x ⊆ U$
7 1 6 simplbiim $⊢ J ∈ Reg → U ∈ J → ∀ z ∈ U ∃ x ∈ J z ∈ x ∧ cls ⁡ J ⁡ x ⊆ U$
8 eleq1 $⊢ z = A → z ∈ x ↔ A ∈ x$
9 8 anbi1d $⊢ z = A → z ∈ x ∧ cls ⁡ J ⁡ x ⊆ U ↔ A ∈ x ∧ cls ⁡ J ⁡ x ⊆ U$
10 9 rexbidv $⊢ z = A → ∃ x ∈ J z ∈ x ∧ cls ⁡ J ⁡ x ⊆ U ↔ ∃ x ∈ J A ∈ x ∧ cls ⁡ J ⁡ x ⊆ U$
11 10 rspccv $⊢ ∀ z ∈ U ∃ x ∈ J z ∈ x ∧ cls ⁡ J ⁡ x ⊆ U → A ∈ U → ∃ x ∈ J A ∈ x ∧ cls ⁡ J ⁡ x ⊆ U$
12 7 11 syl6 $⊢ J ∈ Reg → U ∈ J → A ∈ U → ∃ x ∈ J A ∈ x ∧ cls ⁡ J ⁡ x ⊆ U$
13 12 3imp $⊢ J ∈ Reg ∧ U ∈ J ∧ A ∈ U → ∃ x ∈ J A ∈ x ∧ cls ⁡ J ⁡ x ⊆ U$