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

Metamath Proof Explorer

Theorem isnrm

Description: The predicate "is a normal space." Much like the case for regular spaces, normal does not imply Hausdorff or even regular. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion isnrm 
|- ( J e. Nrm <-> ( J e. Top /\ A. x e. J A. y e. ( ( Clsd ` J ) i^i ~P x ) E. z e. J ( y C_ z /\ ( ( cls ` J ) ` z ) C_ x ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( j = J -> ( Clsd ` j ) = ( Clsd ` J ) )
2 1 ineq1d 
 |-  ( j = J -> ( ( Clsd ` j ) i^i ~P x ) = ( ( Clsd ` J ) i^i ~P x ) )
3 fveq2 
 |-  ( j = J -> ( cls ` j ) = ( cls ` J ) )
4 3 fveq1d 
 |-  ( j = J -> ( ( cls ` j ) ` z ) = ( ( cls ` J ) ` z ) )
5 4 sseq1d 
 |-  ( j = J -> ( ( ( cls ` j ) ` z ) C_ x <-> ( ( cls ` J ) ` z ) C_ x ) )
6 5 anbi2d 
 |-  ( j = J -> ( ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x ) <-> ( y C_ z /\ ( ( cls ` J ) ` z ) C_ x ) ) )
7 6 rexeqbi1dv 
 |-  ( j = J -> ( E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x ) <-> E. z e. J ( y C_ z /\ ( ( cls ` J ) ` z ) C_ x ) ) )
8 2 7 raleqbidv 
 |-  ( j = J -> ( A. y e. ( ( Clsd ` j ) i^i ~P x ) E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x ) <-> A. y e. ( ( Clsd ` J ) i^i ~P x ) E. z e. J ( y C_ z /\ ( ( cls ` J ) ` z ) C_ x ) ) )
9 8 raleqbi1dv 
 |-  ( j = J -> ( A. x e. j A. y e. ( ( Clsd ` j ) i^i ~P x ) E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x ) <-> A. x e. J A. y e. ( ( Clsd ` J ) i^i ~P x ) E. z e. J ( y C_ z /\ ( ( cls ` J ) ` z ) C_ x ) ) )
10 df-nrm 
 |-  Nrm = { j e. Top | A. x e. j A. y e. ( ( Clsd ` j ) i^i ~P x ) E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x ) }
11 9 10 elrab2 
 |-  ( J e. Nrm <-> ( J e. Top /\ A. x e. J A. y e. ( ( Clsd ` J ) i^i ~P x ) E. z e. J ( y C_ z /\ ( ( cls ` J ) ` z ) C_ x ) ) )