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 
|- ( ( 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 ) )