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 ‘ 𝐽 ) ‘ 𝑥 ) ⊆ 𝑈 ) )