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

Metamath Proof Explorer

Theorem ist1

Description: The predicate "is a T_1 space". (Contributed by FL, 18-Jun-2007)

Ref Expression
Hypothesis ist0.1 
|- X = U. J
Assertion ist1 
|- ( J e. Fre <-> ( J e. Top /\ A. a e. X { a } e. ( Clsd ` J ) ) )

Proof

Step Hyp Ref Expression
1 ist0.1 
 |-  X = U. J
2 unieq 
 |-  ( x = J -> U. x = U. J )
3 2 1 eqtr4di 
 |-  ( x = J -> U. x = X )
4 fveq2 
 |-  ( x = J -> ( Clsd ` x ) = ( Clsd ` J ) )
5 4 eleq2d 
 |-  ( x = J -> ( { a } e. ( Clsd ` x ) <-> { a } e. ( Clsd ` J ) ) )
6 3 5 raleqbidv 
 |-  ( x = J -> ( A. a e. U. x { a } e. ( Clsd ` x ) <-> A. a e. X { a } e. ( Clsd ` J ) ) )
7 df-t1 
 |-  Fre = { x e. Top | A. a e. U. x { a } e. ( Clsd ` x ) }
8 6 7 elrab2 
 |-  ( J e. Fre <-> ( J e. Top /\ A. a e. X { a } e. ( Clsd ` J ) ) )