This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 isreg ⊢ ( 𝐽 ∈ Reg ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝐽 ∀ 𝑧 ∈ 𝑦 ∃ 𝑥 ∈ 𝐽 ( 𝑧 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑦 ) ) )
2 sseq2 ⊢ ( 𝑦 = 𝑈 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑦 ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) )
3 2 anbi2d ⊢ ( 𝑦 = 𝑈 → ( ( 𝑧 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑦 ) ↔ ( 𝑧 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) ) )
4 3 rexbidv ⊢ ( 𝑦 = 𝑈 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑧 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑧 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) ) )
5 4 raleqbi1dv ⊢ ( 𝑦 = 𝑈 → ( ∀ 𝑧 ∈ 𝑦 ∃ 𝑥 ∈ 𝐽 ( 𝑧 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑈 ∃ 𝑥 ∈ 𝐽 ( 𝑧 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) ) )
6 5 rspccv ⊢ ( ∀ 𝑦 ∈ 𝐽 ∀ 𝑧 ∈ 𝑦 ∃ 𝑥 ∈ 𝐽 ( 𝑧 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑦 ) → ( 𝑈 ∈ 𝐽 → ∀ 𝑧 ∈ 𝑈 ∃ 𝑥 ∈ 𝐽 ( 𝑧 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) ) )
7 1 6 simplbiim ⊢ ( 𝐽 ∈ Reg → ( 𝑈 ∈ 𝐽 → ∀ 𝑧 ∈ 𝑈 ∃ 𝑥 ∈ 𝐽 ( 𝑧 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) ) )
8 eleq1 ⊢ ( 𝑧 = 𝐴 → ( 𝑧 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 ) )
9 8 anbi1d ⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) ↔ ( 𝐴 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) ) )
10 9 rexbidv ⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑧 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) ) )
11 10 rspccv ⊢ ( ∀ 𝑧 ∈ 𝑈 ∃ 𝑥 ∈ 𝐽 ( 𝑧 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) → ( 𝐴 ∈ 𝑈 → ∃ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) ) )
12 7 11 syl6 ⊢ ( 𝐽 ∈ Reg → ( 𝑈 ∈ 𝐽 → ( 𝐴 ∈ 𝑈 → ∃ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) ) ) )
13 12 3imp ⊢ ( ( 𝐽 ∈ Reg ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈 ) → ∃ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) )