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