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 e. Reg /\ U e. J /\ A e. U ) -> E. x e. J ( A e. x /\ ( ( cls ` J ) ` x ) C_ U ) )

Proof

Step	Hyp	Ref	Expression
1		isreg	|- ( J e. Reg <-> ( J e. Top /\ A. y e. J A. z e. y E. x e. J ( z e. x /\ ( ( cls ` J ) ` x ) C_ y ) ) )
2		sseq2	|- ( y = U -> ( ( ( cls ` J ) ` x ) C_ y <-> ( ( cls ` J ) ` x ) C_ U ) )
3	2	anbi2d	|- ( y = U -> ( ( z e. x /\ ( ( cls ` J ) ` x ) C_ y ) <-> ( z e. x /\ ( ( cls ` J ) ` x ) C_ U ) ) )
4	3	rexbidv	|- ( y = U -> ( E. x e. J ( z e. x /\ ( ( cls ` J ) ` x ) C_ y ) <-> E. x e. J ( z e. x /\ ( ( cls ` J ) ` x ) C_ U ) ) )
5	4	raleqbi1dv	|- ( y = U -> ( A. z e. y E. x e. J ( z e. x /\ ( ( cls ` J ) ` x ) C_ y ) <-> A. z e. U E. x e. J ( z e. x /\ ( ( cls ` J ) ` x ) C_ U ) ) )
6	5	rspccv	|- ( A. y e. J A. z e. y E. x e. J ( z e. x /\ ( ( cls ` J ) ` x ) C_ y ) -> ( U e. J -> A. z e. U E. x e. J ( z e. x /\ ( ( cls ` J ) ` x ) C_ U ) ) )
7	1 6	simplbiim	|- ( J e. Reg -> ( U e. J -> A. z e. U E. x e. J ( z e. x /\ ( ( cls ` J ) ` x ) C_ U ) ) )
8		eleq1	|- ( z = A -> ( z e. x <-> A e. x ) )
9	8	anbi1d	|- ( z = A -> ( ( z e. x /\ ( ( cls ` J ) ` x ) C_ U ) <-> ( A e. x /\ ( ( cls ` J ) ` x ) C_ U ) ) )
10	9	rexbidv	|- ( z = A -> ( E. x e. J ( z e. x /\ ( ( cls ` J ) ` x ) C_ U ) <-> E. x e. J ( A e. x /\ ( ( cls ` J ) ` x ) C_ U ) ) )
11	10	rspccv	|- ( A. z e. U E. x e. J ( z e. x /\ ( ( cls ` J ) ` x ) C_ U ) -> ( A e. U -> E. x e. J ( A e. x /\ ( ( cls ` J ) ` x ) C_ U ) ) )
12	7 11	syl6	|- ( J e. Reg -> ( U e. J -> ( A e. U -> E. x e. J ( A e. x /\ ( ( cls ` J ) ` x ) C_ U ) ) ) )
13	12	3imp	|- ( ( J e. Reg /\ U e. J /\ A e. U ) -> E. x e. J ( A e. x /\ ( ( cls ` J ) ` x ) C_ U ) )