Metamath Proof Explorer


Theorem isreg

Description: The predicate "is a regular space". In a regular space, any open neighborhood has a closed subneighborhood. Note that some authors require the space to be Hausdorff (which would make it the same as T_3), but we reserve the phrase "regular Hausdorff" for that as many topologists do. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion isreg
|- ( J e. Reg <-> ( J e. Top /\ A. x e. J A. y e. x E. z e. J ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) )

Proof

Step Hyp Ref Expression
1 fveq2
 |-  ( j = J -> ( cls ` j ) = ( cls ` J ) )
2 1 fveq1d
 |-  ( j = J -> ( ( cls ` j ) ` z ) = ( ( cls ` J ) ` z ) )
3 2 sseq1d
 |-  ( j = J -> ( ( ( cls ` j ) ` z ) C_ x <-> ( ( cls ` J ) ` z ) C_ x ) )
4 3 anbi2d
 |-  ( j = J -> ( ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) <-> ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) )
5 4 rexeqbi1dv
 |-  ( j = J -> ( E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) <-> E. z e. J ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) )
6 5 ralbidv
 |-  ( j = J -> ( A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) <-> A. y e. x E. z e. J ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) )
7 6 raleqbi1dv
 |-  ( j = J -> ( A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) <-> A. x e. J A. y e. x E. z e. J ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) )
8 df-reg
 |-  Reg = { j e. Top | A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) }
9 7 8 elrab2
 |-  ( J e. Reg <-> ( J e. Top /\ A. x e. J A. y e. x E. z e. J ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) )